(* *)
(**************************************************************************)
-include "ground/notation/functions/circledE_1.ma".
+include "ground/notation/functions/circled_element_e_1.ma".
include "ground/notation/functions/oplusright_3.ma".
include "ground/lib/relations.ma".
(* LISTS ********************************************************************)
-inductive list (A:Type[0]) : Type[0] :=
- | nil : list A
- | cons: A → list A → list A.
+inductive list (A:Type[0]): Type[0] :=
+| list_empty: list A
+| list_lcons: A → list A → list A
+.
-interpretation "nil (list)" 'CircledE A = (nil A).
+interpretation
+ "empty (lists)"
+ 'CircledElementE A = (list_empty A).
-interpretation "cons (list)" 'OPlusRight A hd tl = (cons A hd tl).
+interpretation
+ "left cons (lists)"
+ 'OPlusRight A hd tl = (list_lcons A hd tl).
-rec definition all A (R:predicate A) (l:list A) on l ≝
- match l with
- [ nil ⇒ ⊤
- | cons hd tl ⇒ ∧∧ R hd & all A R tl
- ].
+rec definition list_all A (R:predicate A) (l:list A) on l ≝ match l with
+[ list_empty ⇒ ⊤
+| list_lcons hd tl ⇒ ∧∧ R hd & list_all A R tl
+].
+
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_list_lcons_bi (A) (a1) (a2) (l1) (l2):
+ a1⨮l1 = a2⨮{A}l2 →
+ ∧∧ a1 = a2 & l1 = l2.
+#A #a1 #a2 #l1 #l2 #H0 destruct
+/2 width=1 by conj/
+qed-.