update in ground static_2 basic_2 apps_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / s_transition / fqu.ma

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 ebc264bd7b206bb0d452f85e69dd9911116c5135..2e81b0bc3ca8114c4ffc1472d3efb6106d693f44 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/s_transition/fqu.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/s_transition/fqu.ma
@@ -47,18 +47,18 @@ interpretation
 
 (* Basic properties *********************************************************)
 
-lemma fqu_sort: â\88\80b,I,G,L,s. â\9dªG,L.â\93\98[I],â\8b\86sâ\9d« â¬\82[b] â\9dªG,L,â\8b\86sâ\9d«.
+lemma fqu_sort: â\88\80b,I,G,L,s. â\9d¨G,L.â\93\98[I],â\8b\86sâ\9d© â¬\82[b] â\9d¨G,L,â\8b\86sâ\9d©.
 /2 width=1 by fqu_drop/ qed.
 
-lemma fqu_lref_S: â\88\80b,I,G,L,i. â\9dªG,L.â\93\98[I],#â\86\91iâ\9d« â¬\82[b] â\9dªG,L,#iâ\9d«.
+lemma fqu_lref_S: â\88\80b,I,G,L,i. â\9d¨G,L.â\93\98[I],#â\86\91iâ\9d© â¬\82[b] â\9d¨G,L,#iâ\9d©.
 /2 width=1 by fqu_drop/ qed.
 
-lemma fqu_gref: â\88\80b,I,G,L,l. â\9dªG,L.â\93\98[I],§lâ\9d« â¬\82[b] â\9dªG,L,§lâ\9d«.
+lemma fqu_gref: â\88\80b,I,G,L,l. â\9d¨G,L.â\93\98[I],§lâ\9d© â¬\82[b] â\9d¨G,L,§lâ\9d©.
 /2 width=1 by fqu_drop/ qed.
 
 (* Basic inversion lemmas ***************************************************)
 
-fact fqu_inv_sort1_aux: â\88\80b,G1,G2,L1,L2,T1,T2. â\9dªG1,L1,T1â\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+fact fqu_inv_sort1_aux: â\88\80b,G1,G2,L1,L2,T1,T2. â\9d¨G1,L1,T1â\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
                         ∀s. T1 = ⋆s →
                         ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & T2 = ⋆s.
 #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
@@ -72,11 +72,11 @@ fact fqu_inv_sort1_aux: ∀b,G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂[b] ❪G2,L2,T
 ]
 qed-.
 
-lemma fqu_inv_sort1: â\88\80b,G1,G2,L1,L2,T2,s. â\9dªG1,L1,â\8b\86sâ\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+lemma fqu_inv_sort1: â\88\80b,G1,G2,L1,L2,T2,s. â\9d¨G1,L1,â\8b\86sâ\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
                      ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & T2 = ⋆s.
 /2 width=4 by fqu_inv_sort1_aux/ qed-.
 
-fact fqu_inv_lref1_aux: â\88\80b,G1,G2,L1,L2,T1,T2. â\9dªG1,L1,T1â\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+fact fqu_inv_lref1_aux: â\88\80b,G1,G2,L1,L2,T1,T2. â\9d¨G1,L1,T1â\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
                         ∀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.
@@ -91,12 +91,12 @@ fact fqu_inv_lref1_aux: ∀b,G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂[b] ❪G2,L2,T
 ]
 qed-.
 
-lemma fqu_inv_lref1: â\88\80b,G1,G2,L1,L2,T2,i. â\9dªG1,L1,#iâ\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+lemma fqu_inv_lref1: â\88\80b,G1,G2,L1,L2,T2,i. â\9d¨G1,L1,#iâ\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
                      (∃∃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: â\88\80b,G1,G2,L1,L2,T1,T2. â\9dªG1,L1,T1â\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+fact fqu_inv_gref1_aux: â\88\80b,G1,G2,L1,L2,T1,T2. â\9d¨G1,L1,T1â\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
                         ∀l. T1 = §l →
                         ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & T2 = §l.
 #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
@@ -110,11 +110,11 @@ fact fqu_inv_gref1_aux: ∀b,G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂[b] ❪G2,L2,T
 ]
 qed-.
 
-lemma fqu_inv_gref1: â\88\80b,G1,G2,L1,L2,T2,l. â\9dªG1,L1,§lâ\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+lemma fqu_inv_gref1: â\88\80b,G1,G2,L1,L2,T2,l. â\9d¨G1,L1,§lâ\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
                      ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & T2 = §l.
 /2 width=4 by fqu_inv_gref1_aux/ qed-.
 
-fact fqu_inv_bind1_aux: â\88\80b,G1,G2,L1,L2,T1,T2. â\9dªG1,L1,T1â\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+fact fqu_inv_bind1_aux: â\88\80b,G1,G2,L1,L2,T1,T2. â\9d¨G1,L1,T1â\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
                         ∀p,I,V1,U1. T1 = ⓑ[p,I]V1.U1 →
                         ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
                          | ∧∧ G1 = G2 & L1.ⓑ[I]V1 = L2 & U1 = T2 & b = Ⓣ
@@ -130,14 +130,14 @@ fact fqu_inv_bind1_aux: ∀b,G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂[b] ❪G2,L2,T
 ]
 qed-.
 
-lemma fqu_inv_bind1: â\88\80b,p,I,G1,G2,L1,L2,V1,U1,T2. â\9dªG1,L1,â\93\91[p,I]V1.U1â\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+lemma fqu_inv_bind1: â\88\80b,p,I,G1,G2,L1,L2,V1,U1,T2. â\9d¨G1,L1,â\93\91[p,I]V1.U1â\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
                      ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
                       | ∧∧ G1 = G2 & L1.ⓑ[I]V1 = L2 & U1 = T2 & b = Ⓣ
                       | ∧∧ 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: â\88\80p,I,G1,G2,L1,L2,V1,U1,T2. â\9dªG1,L1,â\93\91[p,I]V1.U1â\9d« â¬\82 â\9dªG2,L2,T2â\9d« →
+lemma fqu_inv_bind1_true: â\88\80p,I,G1,G2,L1,L2,V1,U1,T2. â\9d¨G1,L1,â\93\91[p,I]V1.U1â\9d© â¬\82 â\9d¨G2,L2,T2â\9d© →
                           ∨∨ ∧∧ 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.
@@ -147,7 +147,7 @@ lemma fqu_inv_bind1_true: ∀p,I,G1,G2,L1,L2,V1,U1,T2. ❪G1,L1,ⓑ[p,I]V1.U1❫
 /3 width=1 by and3_intro, or3_intro1/
 qed-.
 
-fact fqu_inv_flat1_aux: â\88\80b,G1,G2,L1,L2,T1,T2. â\9dªG1,L1,T1â\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+fact fqu_inv_flat1_aux: â\88\80b,G1,G2,L1,L2,T1,T2. â\9d¨G1,L1,T1â\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
                         ∀I,V1,U1. T1 = ⓕ[I]V1.U1 →
                         ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
                          | ∧∧ G1 = G2 & L1 = L2 & U1 = T2
@@ -162,7 +162,7 @@ fact fqu_inv_flat1_aux: ∀b,G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂[b] ❪G2,L2,T
 ]
 qed-.
 
-lemma fqu_inv_flat1: â\88\80b,I,G1,G2,L1,L2,V1,U1,T2. â\9dªG1,L1,â\93\95[I]V1.U1â\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+lemma fqu_inv_flat1: â\88\80b,I,G1,G2,L1,L2,V1,U1,T2. â\9d¨G1,L1,â\93\95[I]V1.U1â\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
                      ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
                       | ∧∧ G1 = G2 & L1 = L2 & U1 = T2
                       | ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & ⇧[1] T2 ≘ ⓕ[I]V1.U1.
@@ -170,31 +170,31 @@ lemma fqu_inv_flat1: ∀b,I,G1,G2,L1,L2,V1,U1,T2. ❪G1,L1,ⓕ[I]V1.U1❫ ⬂[b]
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma fqu_inv_atom1: â\88\80b,I,G1,G2,L2,T2. â\9dªG1,â\8b\86,â\93ª[I]â\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« → ⊥.
+lemma fqu_inv_atom1: â\88\80b,I,G1,G2,L2,T2. â\9d¨G1,â\8b\86,â\93ª[I]â\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© → ⊥.
 #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: â\88\80b,I,G1,G2,K,L2,T2,s. â\9dªG1,K.â\93\98[I],â\8b\86sâ\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+lemma fqu_inv_sort1_bind: â\88\80b,I,G1,G2,K,L2,T2,s. â\9d¨G1,K.â\93\98[I],â\8b\86sâ\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
                           ∧∧ 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: â\88\80b,I,G1,G2,K,L2,V,T2. â\9dªG1,K.â\93\91[I]V,#0â\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+lemma fqu_inv_zero1_pair: â\88\80b,I,G1,G2,K,L2,V,T2. â\9d¨G1,K.â\93\91[I]V,#0â\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
                           ∧∧ 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: â\88\80b,I,G1,G2,K,L2,T2,i. â\9dªG1,K.â\93\98[I],#(â\86\91i)â\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+lemma fqu_inv_lref1_bind: â\88\80b,I,G1,G2,K,L2,T2,i. â\9d¨G1,K.â\93\98[I],#(â\86\91i)â\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
                           ∧∧ 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: â\88\80b,I,G1,G2,K,L2,T2,l. â\9dªG1,K.â\93\98[I],§lâ\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+lemma fqu_inv_gref1_bind: â\88\80b,I,G1,G2,K,L2,T2,l. â\9d¨G1,K.â\93\98[I],§lâ\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
                           ∧∧ 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/