1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground/notation/relations/ringeq_3.ma".
16 include "ground/lib/list.ma".
18 (* EXTENSIONAL EQUIVALENCE FOR LISTS ****************************************)
20 rec definition list_eq A (l1,l2:list A) on l1 ≝
30 | list_cons a2 l2 ⇒ a1 = a2 ∧ list_eq A l1 l2
35 "extensional equivalence (lists)"
36 'RingEq A l1 l2 = (list_eq A l1 l2).
38 (* Basic constructions ******************************************************)
40 lemma list_eq_refl (A):
41 reflexive … (list_eq A).
42 #A #l elim l -l /2 width=1 by conj/
45 (* Main constructions *******************************************************)
47 theorem eq_list_eq (A) (l1) (l2):
51 (* Main inversions **********************************************************)
53 theorem list_eq_inv_eq (A) (l1) (l2):
55 #A #l1 elim l1 -l1 [| #a1 #l1 #IH ] *
59 | #a2 #l2 * #Ha #Hl /3 width=1 by eq_f2/