update in delayed_updating and ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / lib / list.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list.ma b/matita/matita/contribs/lambdadelta/ground/lib/list.ma
index 21a0f75602d53d5962585ffb0a7ac69d5480b7e3..a486fd39ae1fbf2cdcf0096331b5a7759358368b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/list.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-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".
 
@@ -25,7 +25,7 @@ inductive list (A:Type[0]): Type[0] :=
 
 interpretation
   "empty (lists)"
-  'CircledE A = (list_empty A).
+  'CircledElementE A = (list_empty A).
 
 interpretation
   "left cons (lists)"
@@ -35,3 +35,12 @@ 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-.