Skip to content
Snippets Groups Projects
Commit be8dfddb authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Use wf_projected instead of well_founded_lt_compat

parent 64bedf4c
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/fin_collections.v
+ 1
− 1
View file @ be8dfddb
......@@ -145,7 +145,7 @@ Proof.
Qed.
Lemma collection_wf : wf (strict (@subseteq C _)).
Proof. apply well_founded_lt_compat with size, subset_size. Qed.
Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed.
Lemma collection_ind (P : C → Prop) :
Proper ((≡) ==> iff) P →
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment