Commit 2e67e68f authored by Robbert Krebbers's avatar Robbert Krebbers

Make some names more consistent.

parent cef729e8
......@@ -2684,7 +2684,7 @@ Section setoid.
Lemma equiv_Forall2 l k : l k Forall2 () l k.
Proof. split; induction 1; constructor; auto. Qed.
Lemma equiv_lookup l k : l k ( i, l !! i k !! i).
Lemma list_equiv_lookup l k : l k i, l !! i k !! i.
Proof.
rewrite equiv_Forall2, Forall2_lookup.
by setoid_rewrite equiv_option_Forall2.
......
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