Commit 09dc9e0d authored by Ralf Jung's avatar Ralf Jung

more consistent lemma names

parent 536c3662
...@@ -913,11 +913,11 @@ Section find. ...@@ -913,11 +913,11 @@ Section find.
Proof. Proof.
induction l as [|x l IH]; [done|]. simpl. induction l as [|x l IH]; [done|]. simpl.
case_decide; [done|]. case_decide; [done|].
change (list_fmap B A f l) with (f <$> l). (* FIXME it simplified too much *) change (list_fmap B A f l) with (f <$> l). (* induction didn't re-fold *)
rewrite IH. by destruct (list_find (P f) l). rewrite IH. by destruct (list_find (P f) l).
Qed. Qed.
Lemma list_find_proper (Q : A Prop) `{ x, Decision (Q x)} l : Lemma list_find_ext (Q : A Prop) `{ x, Decision (Q x)} l :
( x, P x Q x) ( x, P x Q x)
list_find P l = list_find Q l. list_find P l = list_find Q l.
Proof. Proof.
......
Markdown is supported
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