still more additions and corrections for the article

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / lsubv.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma
index 17a22da58e20b23bf0b9057e9dfb6f2463e21de2..fdf2ad8033ec615caa435de249a95edb70926a3c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma
@@ -30,7 +30,8 @@ interpretation
 
 (* Basic inversion lemmas ***************************************************)
 
-fact lsubv_inv_atom_sn_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → L1 = ⋆ → L2 = ⋆.
+fact lsubv_inv_atom_sn_aux (a) (h) (G):
+     ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → L1 = ⋆ → L2 = ⋆.
 #a #h #G #L1 #L2 * -L1 -L2
 [ //
 | #I #L1 #L2 #_ #H destruct
@@ -39,15 +40,15 @@ fact lsubv_inv_atom_sn_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → L1 =
 qed-.
 
 (* Basic_2A1: uses: lsubsv_inv_atom1 *)
-lemma lsubv_inv_atom_sn (a) (h) (G): ∀L2. G ⊢ ⋆ ⫃![a,h] L2 → L2 = ⋆.
+lemma lsubv_inv_atom_sn (a) (h) (G):
+      ∀L2. G ⊢ ⋆ ⫃![a,h] L2 → L2 = ⋆.
 /2 width=6 by lsubv_inv_atom_sn_aux/ qed-.
 
 fact lsubv_inv_bind_sn_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 →
-                           ∀I,K1. L1 = K1.ⓘ{I} →
-                           ∨∨ ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & L2 = K2.ⓘ{I}
-                            | ∃∃K2,W,V. ⦃G,K1⦄ ⊢ ⓝW.V ![a,h] &
-                                        G ⊢ K1 ⫃![a,h] K2 &
-                                        I = BPair Abbr (ⓝW.V) & L2 = K2.ⓛW.
+     ∀I,K1. L1 = K1.ⓘ{I} →
+     ∨∨ ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & L2 = K2.ⓘ{I}
+      | ∃∃K2,W,V. ⦃G,K1⦄ ⊢ ⓝW.V ![a,h] & G ⊢ K1 ⫃![a,h] K2
+                & I = BPair Abbr (ⓝW.V) & L2 = K2.ⓛW.
 #a #h #G #L1 #L2 * -L1 -L2
 [ #J #K1 #H destruct
 | #I #L1 #L2 #HL12 #J #K1 #H destruct /3 width=3 by ex2_intro, or_introl/
@@ -56,14 +57,15 @@ fact lsubv_inv_bind_sn_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 →
 qed-.
 
 (* Basic_2A1: uses: lsubsv_inv_pair1 *)
-lemma lsubv_inv_bind_sn (a) (h) (G): ∀I,K1,L2. G ⊢ K1.ⓘ{I} ⫃![a,h] L2 →
-                        ∨∨ ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & L2 = K2.ⓘ{I}
-                         | ∃∃K2,W,V. ⦃G,K1⦄ ⊢ ⓝW.V ![a,h] &
-                                     G ⊢ K1 ⫃![a,h] K2 &
-                                     I = BPair Abbr (ⓝW.V) & L2 = K2.ⓛW.
+lemma lsubv_inv_bind_sn (a) (h) (G):
+      ∀I,K1,L2. G ⊢ K1.ⓘ{I} ⫃![a,h] L2 →
+      ∨∨ ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & L2 = K2.ⓘ{I}
+       | ∃∃K2,W,V. ⦃G,K1⦄ ⊢ ⓝW.V ![a,h] & G ⊢ K1 ⫃![a,h] K2
+                 & I = BPair Abbr (ⓝW.V) & L2 = K2.ⓛW.
 /2 width=3 by lsubv_inv_bind_sn_aux/ qed-.
 
-fact lsubv_inv_atom_dx_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → L2 = ⋆ → L1 = ⋆.
+fact lsubv_inv_atom_dx_aux (a) (h) (G):
+     ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → L2 = ⋆ → L1 = ⋆.
 #a #h #G #L1 #L2 * -L1 -L2
 [ //
 | #I #L1 #L2 #_ #H destruct
@@ -72,14 +74,16 @@ fact lsubv_inv_atom_dx_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → L2 =
 qed-.
 
 (* Basic_2A1: uses: lsubsv_inv_atom2 *)
-lemma lsubv_inv_atom2 (a) (h) (G): ∀L1. G ⊢ L1 ⫃![a,h] ⋆ → L1 = ⋆.
+lemma lsubv_inv_atom2 (a) (h) (G):
+      ∀L1. G ⊢ L1 ⫃![a,h] ⋆ → L1 = ⋆.
 /2 width=6 by lsubv_inv_atom_dx_aux/ qed-.
 
-fact lsubv_inv_bind_dx_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 →
-                           ∀I,K2. L2 = K2.ⓘ{I} →
-                           ∨∨ ∃∃K1. G ⊢ K1 ⫃![a,h] K2 & L1 = K1.ⓘ{I}
-                            | ∃∃K1,W,V. ⦃G,K1⦄ ⊢ ⓝW.V ![a,h] &
-                                        G ⊢ K1 ⫃![a,h] K2 & I = BPair Abst W & L1 = K1.ⓓⓝW.V.
+fact lsubv_inv_bind_dx_aux (a) (h) (G):
+     ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 →
+     ∀I,K2. L2 = K2.ⓘ{I} →
+     ∨∨ ∃∃K1. G ⊢ K1 ⫃![a,h] K2 & L1 = K1.ⓘ{I}
+      | ∃∃K1,W,V. ⦃G,K1⦄ ⊢ ⓝW.V ![a,h] &
+                  G ⊢ K1 ⫃![a,h] K2 & I = BPair Abst W & L1 = K1.ⓓⓝW.V.
 #a #h #G #L1 #L2 * -L1 -L2
 [ #J #K2 #H destruct
 | #I #L1 #L2 #HL12 #J #K2 #H destruct /3 width=3 by ex2_intro, or_introl/
@@ -88,16 +92,18 @@ fact lsubv_inv_bind_dx_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 →
 qed-.
 
 (* Basic_2A1: uses: lsubsv_inv_pair2 *)
-lemma lsubv_inv_bind_dx (a) (h) (G): ∀I,L1,K2. G ⊢ L1 ⫃![a,h] K2.ⓘ{I} →
-                        ∨∨ ∃∃K1. G ⊢ K1 ⫃![a,h] K2 & L1 = K1.ⓘ{I}
-                         | ∃∃K1,W,V. ⦃G,K1⦄ ⊢ ⓝW.V ![a,h] &
-                                     G ⊢ K1 ⫃![a,h] K2 & I = BPair Abst W & L1 = K1.ⓓⓝW.V.
+lemma lsubv_inv_bind_dx (a) (h) (G):
+      ∀I,L1,K2. G ⊢ L1 ⫃![a,h] K2.ⓘ{I} →
+      ∨∨ ∃∃K1. G ⊢ K1 ⫃![a,h] K2 & L1 = K1.ⓘ{I}
+       | ∃∃K1,W,V. ⦃G,K1⦄ ⊢ ⓝW.V ![a,h] &
+                   G ⊢ K1 ⫃![a,h] K2 & I = BPair Abst W & L1 = K1.ⓓⓝW.V.
 /2 width=3 by lsubv_inv_bind_dx_aux/ qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma lsubv_inv_abst_sn (a) (h) (G): ∀K1,L2,W. G ⊢ K1.ⓛW ⫃![a,h] L2 →
-                        ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & L2 = K2.ⓛW.
+lemma lsubv_inv_abst_sn (a) (h) (G):
+      ∀K1,L2,W. G ⊢ K1.ⓛW ⫃![a,h] L2 →
+      ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & L2 = K2.ⓛW.
 #a #h #G #K1 #L2 #W #H
 elim (lsubv_inv_bind_sn … H) -H // *
 #K2 #XW #XV #_ #_ #H1 #H2 destruct