rec definition list_eq A (l1,l2:list A) on l1 ≝
match l1 with
-[ list_nil ⇒
+[ list_empty ⇒
match l2 with
- [ list_nil ⇒ ⊤
- | list_cons _ _ ⇒ ⊥
+ [ list_empty ⇒ ⊤
+ | list_lcons _ _ ⇒ ⊥
]
-| list_cons a1 l1 ⇒
+| list_lcons a1 l1 ⇒
match l2 with
- [ list_nil ⇒ ⊥
- | list_cons a2 l2 ⇒ a1 = a2 ∧ list_eq A l1 l2
+ [ list_empty ⇒ ⊥
+ | list_lcons a2 l2 ⇒ a1 = a2 ∧ list_eq A l1 l2
]
].
(* Basic constructions ******************************************************)
-lemma list_eq_refl (A): reflexive … (list_eq A).
+lemma list_eq_refl (A):
+ reflexive … (list_eq A).
#A #l elim l -l /2 width=1 by conj/
qed.
(* Main constructions *******************************************************)
-theorem eq_list_eq (A,l1,l2): l1 = l2 → l1 ≗{A} l2.
+theorem eq_list_eq (A) (l1) (l2):
+ l1 = l2 → l1 ≗{A} l2.
// qed.
(* Main inversions **********************************************************)
-theorem list_eq_inv_eq (A,l1,l2): l1 ≗{A} l2 → l1 = l2.
+theorem list_eq_inv_eq (A) (l1) (l2):
+ l1 ≗{A} l2 → l1 = l2.
#A #l1 elim l1 -l1 [| #a1 #l1 #IH ] *
[ //
| #a2 #l2 #H elim H