X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fs_transition%2Ffqu.ma;h=bff7b2fe9e2561c7f349a58c358153d219d45d58;hp=b834566d303abb0b99470f21aa052d6cf2f3e770;hb=f308429a0fde273605a2330efc63268b4ac36c99;hpb=87f57ddc367303c33e19c83cd8989cd561f3185b

diff --git a/matita/matita/contribs/lambdadelta/static_2/s_transition/fqu.ma b/matita/matita/contribs/lambdadelta/static_2/s_transition/fqu.ma
index b834566d3..bff7b2fe9 100644
--- a/matita/matita/contribs/lambdadelta/static_2/s_transition/fqu.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/s_transition/fqu.ma
@@ -44,18 +44,18 @@ interpretation
 
 (* Basic properties *********************************************************)
 
-lemma fqu_sort: ∀b,I,G,L,s. ⦃G, L.ⓘ{I}, ⋆s⦄ ⊐[b] ⦃G, L, ⋆s⦄.
+lemma fqu_sort: ∀b,I,G,L,s. ⦃G,L.ⓘ{I},⋆s⦄ ⊐[b] ⦃G,L,⋆s⦄.
 /2 width=1 by fqu_drop/ qed.
 
-lemma fqu_lref_S: ∀b,I,G,L,i. ⦃G, L.ⓘ{I}, #↑i⦄ ⊐[b] ⦃G, L, #i⦄.
+lemma fqu_lref_S: ∀b,I,G,L,i. ⦃G,L.ⓘ{I},#↑i⦄ ⊐[b] ⦃G,L,#i⦄.
 /2 width=1 by fqu_drop/ qed.
 
-lemma fqu_gref: ∀b,I,G,L,l. ⦃G, L.ⓘ{I}, §l⦄ ⊐[b] ⦃G, L, §l⦄.
+lemma fqu_gref: ∀b,I,G,L,l. ⦃G,L.ⓘ{I},§l⦄ ⊐[b] ⦃G,L,§l⦄.
 /2 width=1 by fqu_drop/ qed.
 
 (* Basic inversion lemmas ***************************************************)
 
-fact fqu_inv_sort1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+fact fqu_inv_sort1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⊐[b] ⦃G2,L2,T2⦄ →
                         ∀s. T1 = ⋆s →
                         ∃∃J. G1 = G2 & L1 = L2.ⓘ{J} & T2 = ⋆s.
 #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
@@ -69,11 +69,11 @@ fact fqu_inv_sort1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L
 ]
 qed-.
 
-lemma fqu_inv_sort1: ∀b,G1,G2,L1,L2,T2,s. ⦃G1, L1, ⋆s⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+lemma fqu_inv_sort1: ∀b,G1,G2,L1,L2,T2,s. ⦃G1,L1,⋆s⦄ ⊐[b] ⦃G2,L2,T2⦄ →
                      ∃∃J. G1 = G2 & L1 = L2.ⓘ{J} & T2 = ⋆s.
 /2 width=4 by fqu_inv_sort1_aux/ qed-.
 
-fact fqu_inv_lref1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+fact fqu_inv_lref1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⊐[b] ⦃G2,L2,T2⦄ →
                         ∀i. T1 = #i →
                         (∃∃J,V. G1 = G2 & L1 = L2.ⓑ{J}V & T2 = V & i = 0) ∨
                         ∃∃J,j. G1 = G2 & L1 = L2.ⓘ{J} & T2 = #j & i = ↑j.
@@ -88,12 +88,12 @@ fact fqu_inv_lref1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L
 ]
 qed-.
 
-lemma fqu_inv_lref1: ∀b,G1,G2,L1,L2,T2,i. ⦃G1, L1, #i⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+lemma fqu_inv_lref1: ∀b,G1,G2,L1,L2,T2,i. ⦃G1,L1,#i⦄ ⊐[b] ⦃G2,L2,T2⦄ →
                      (∃∃J,V. G1 = G2 & L1 = L2.ⓑ{J}V & T2 = V & i = 0) ∨
                      ∃∃J,j. G1 = G2 & L1 = L2.ⓘ{J} & T2 = #j & i = ↑j.
 /2 width=4 by fqu_inv_lref1_aux/ qed-.
 
-fact fqu_inv_gref1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+fact fqu_inv_gref1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⊐[b] ⦃G2,L2,T2⦄ →
                         ∀l. T1 = §l →
                         ∃∃J. G1 = G2 & L1 = L2.ⓘ{J} & T2 = §l.
 #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
@@ -107,11 +107,11 @@ fact fqu_inv_gref1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L
 ]
 qed-.
 
-lemma fqu_inv_gref1: ∀b,G1,G2,L1,L2,T2,l. ⦃G1, L1, §l⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+lemma fqu_inv_gref1: ∀b,G1,G2,L1,L2,T2,l. ⦃G1,L1,§l⦄ ⊐[b] ⦃G2,L2,T2⦄ →
                      ∃∃J. G1 = G2 & L1 = L2.ⓘ{J} & T2 = §l.
 /2 width=4 by fqu_inv_gref1_aux/ qed-.
 
-fact fqu_inv_bind1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+fact fqu_inv_bind1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⊐[b] ⦃G2,L2,T2⦄ →
                         ∀p,I,V1,U1. T1 = ⓑ{p,I}V1.U1 →
                         ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
                          | ∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & U1 = T2
@@ -127,14 +127,14 @@ fact fqu_inv_bind1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L
 ]
 qed-.
 
-lemma fqu_inv_bind1: ∀b,p,I,G1,G2,L1,L2,V1,U1,T2. ⦃G1, L1, ⓑ{p,I}V1.U1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+lemma fqu_inv_bind1: ∀b,p,I,G1,G2,L1,L2,V1,U1,T2. ⦃G1,L1,ⓑ{p,I}V1.U1⦄ ⊐[b] ⦃G2,L2,T2⦄ →
                      ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
                       | ∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & U1 = T2
                       | ∧∧ G1 = G2 & L1.ⓧ = L2 & U1 = T2 & b = Ⓕ
                       | ∃∃J. G1 = G2 & L1 = L2.ⓘ{J} & ⬆*[1] T2 ≘ ⓑ{p,I}V1.U1.
 /2 width=4 by fqu_inv_bind1_aux/ qed-.
 
-lemma fqu_inv_bind1_true: ∀p,I,G1,G2,L1,L2,V1,U1,T2. ⦃G1, L1, ⓑ{p,I}V1.U1⦄ ⊐ ⦃G2, L2, T2⦄ →
+lemma fqu_inv_bind1_true: ∀p,I,G1,G2,L1,L2,V1,U1,T2. ⦃G1,L1,ⓑ{p,I}V1.U1⦄ ⊐ ⦃G2,L2,T2⦄ →
                           ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
                            | ∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & U1 = T2
                            | ∃∃J. G1 = G2 & L1 = L2.ⓘ{J} & ⬆*[1] T2 ≘ ⓑ{p,I}V1.U1.
@@ -143,7 +143,7 @@ lemma fqu_inv_bind1_true: ∀p,I,G1,G2,L1,L2,V1,U1,T2. ⦃G1, L1, ⓑ{p,I}V1.U1
 * #_ #_ #_ #H destruct
 qed-.
 
-fact fqu_inv_flat1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+fact fqu_inv_flat1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⊐[b] ⦃G2,L2,T2⦄ →
                         ∀I,V1,U1. T1 = ⓕ{I}V1.U1 →
                         ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
                          | ∧∧ G1 = G2 & L1 = L2 & U1 = T2
@@ -158,7 +158,7 @@ fact fqu_inv_flat1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L
 ]
 qed-.
 
-lemma fqu_inv_flat1: ∀b,I,G1,G2,L1,L2,V1,U1,T2. ⦃G1, L1, ⓕ{I}V1.U1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+lemma fqu_inv_flat1: ∀b,I,G1,G2,L1,L2,V1,U1,T2. ⦃G1,L1,ⓕ{I}V1.U1⦄ ⊐[b] ⦃G2,L2,T2⦄ →
                      ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
                       | ∧∧ G1 = G2 & L1 = L2 & U1 = T2
                       | ∃∃J. G1 = G2 & L1 = L2.ⓘ{J} & ⬆*[1] T2 ≘ ⓕ{I}V1.U1.
@@ -166,31 +166,31 @@ lemma fqu_inv_flat1: ∀b,I,G1,G2,L1,L2,V1,U1,T2. ⦃G1, L1, ⓕ{I}V1.U1⦄ ⊐[
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma fqu_inv_atom1: ∀b,I,G1,G2,L2,T2. ⦃G1, ⋆, ⓪{I}⦄ ⊐[b] ⦃G2, L2, T2⦄ → ⊥.
+lemma fqu_inv_atom1: ∀b,I,G1,G2,L2,T2. ⦃G1,⋆,⓪{I}⦄ ⊐[b] ⦃G2,L2,T2⦄ → ⊥.
 #b * #x #G1 #G2 #L2 #T2 #H
 [ elim (fqu_inv_sort1 … H) | elim (fqu_inv_lref1 … H) * | elim (fqu_inv_gref1 … H) ] -H
 #I [2: #V |3: #i ] #_ #H destruct
 qed-.
 
-lemma fqu_inv_sort1_bind: ∀b,I,G1,G2,K,L2,T2,s. ⦃G1, K.ⓘ{I}, ⋆s⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+lemma fqu_inv_sort1_bind: ∀b,I,G1,G2,K,L2,T2,s. ⦃G1,K.ⓘ{I},⋆s⦄ ⊐[b] ⦃G2,L2,T2⦄ →
                           ∧∧ G1 = G2 & L2 = K & T2 = ⋆s.
 #b #I #G1 #G2 #K #L2 #T2 #s #H elim (fqu_inv_sort1 … H) -H
 #Z #X #H1 #H2 destruct /2 width=1 by and3_intro/
 qed-.
 
-lemma fqu_inv_zero1_pair: ∀b,I,G1,G2,K,L2,V,T2. ⦃G1, K.ⓑ{I}V, #0⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+lemma fqu_inv_zero1_pair: ∀b,I,G1,G2,K,L2,V,T2. ⦃G1,K.ⓑ{I}V,#0⦄ ⊐[b] ⦃G2,L2,T2⦄ →
                           ∧∧ G1 = G2 & L2 = K & T2 = V.
 #b #I #G1 #G2 #K #L2 #V #T2 #H elim (fqu_inv_lref1 … H) -H *
 #Z #X #H1 #H2 #H3 #H4 destruct /2 width=1 by and3_intro/
 qed-.
 
-lemma fqu_inv_lref1_bind: ∀b,I,G1,G2,K,L2,T2,i. ⦃G1, K.ⓘ{I}, #(↑i)⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+lemma fqu_inv_lref1_bind: ∀b,I,G1,G2,K,L2,T2,i. ⦃G1,K.ⓘ{I},#(↑i)⦄ ⊐[b] ⦃G2,L2,T2⦄ →
                           ∧∧ G1 = G2 & L2 = K & T2 = #i.
 #b #I #G1 #G2 #K #L2 #T2 #i #H elim (fqu_inv_lref1 … H) -H *
 #Z #X #H1 #H2 #H3 #H4 destruct /2 width=1 by and3_intro/
 qed-.
 
-lemma fqu_inv_gref1_bind: ∀b,I,G1,G2,K,L2,T2,l. ⦃G1, K.ⓘ{I}, §l⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+lemma fqu_inv_gref1_bind: ∀b,I,G1,G2,K,L2,T2,l. ⦃G1,K.ⓘ{I},§l⦄ ⊐[b] ⦃G2,L2,T2⦄ →
                           ∧∧ G1 = G2 & L2 = K & T2 = §l.
 #b #I #G1 #G2 #K #L2 #T2 #l #H elim (fqu_inv_gref1 … H) -H
 #Z #H1 #H2 #H3 destruct /2 width=1 by and3_intro/