X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsyntax%2Fvoids.ma;h=854737b4a47c8eeacc3740340ecc3784e66e0fb1;hb=528f8ea107f689d07d060e1d31ba32bf65b4e6ba;hp=766eefd5c2ccfa8c1027b62cfb4b7ded9bffc94e;hpb=dc9c7181b2dc66c8d297f708324dcdeea98bc4d8;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/voids.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/voids.ma
index 766eefd5c..854737b4a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/voids.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/voids.ma
@@ -37,6 +37,49 @@ lemma voids_next: ∀n,L. ⓧ*[n](L.ⓧ) = ⓧ*[⫯n]L.
 #n elim n -n //
 qed.
 
+(* Basic inversion lemmas ***************************************************)
+
+lemma voids_atom_inv: ∀K,n. ⓧ*[n]K = ⋆ → ∧∧ ⋆ = K & 0 = n.
+#K * /2 width=1 by conj/
+#n <voids_succ #H destruct
+qed-.
+
+lemma voids_pair_inv: ∀I,K1,K2,V,n. ⓧ*[n]K1 = K2.ⓑ{I}V →
+                      ∧∧ K2.ⓑ{I}V = K1 & 0 = n.
+#I #K1 #K2 #V * /2 width=1 by conj/
+#n <voids_succ #H destruct
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma voids_inv_atom_sn: ∀n1,K2,n2. ⓧ*[n1]⋆ = ⓧ*[n2]K2 →
+                         ∧∧ ⓧ*[n1-n2]⋆ = K2 & n2 ≤ n1.
+#n1 elim n1 -n1
+[ #K2 <voids_zero * /2 width=1 by conj/
+  #n1 <voids_succ #H destruct
+| #n1 #IH #K2 *
+  [ <voids_zero #H destruct /2 width=1 by conj/
+  | #n2 <voids_succ <voids_succ >minus_S_S #H
+    elim (destruct_lbind_lbind_aux … H) -H #HK #_ (**) (* destruct lemma needed *)
+    elim (IH … HK) -IH -HK #H #Hn destruct /3 width=1 by conj, le_S_S/
+  ]
+]
+qed-.
+
+lemma voids_inv_pair_sn: ∀I,V,n1,K1,K2,n2. ⓧ*[n1]K1.ⓑ{I}V = ⓧ*[n2]K2 →
+                         ∧∧ ⓧ*[n1-n2]K1.ⓑ{I}V = K2 & n2 ≤ n1.
+#I #V #n1 elim n1 -n1
+[ #K1 #K2 <voids_zero * /2 width=1 by conj/
+  #n1 <voids_succ #H destruct
+| #n1 #IH #K1 #K2 *
+  [ <voids_zero #H destruct /2 width=1 by conj/
+  | #n2 <voids_succ <voids_succ >minus_S_S #H
+    elim (destruct_lbind_lbind_aux … H) -H #HK #_ (**) (* destruct lemma needed *)
+    elim (IH … HK) -IH -HK #H #Hn destruct /3 width=1 by conj, le_S_S/
+  ]
+]
+qed-.
+
 (* Main inversion properties ************************************************)
 
 theorem voids_inj: ∀n. injective … (λL. ⓧ*[n]L).