update in ground_2, static_2, basic_2, apps_2, alpha_1

[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 a496d528c66d662b94b0cd86ef20bf12ebb018b7..91502888453e422587d3fafd54feb860fba322ea 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/s_transition/fqu.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/s_transition/fqu.ma
@@ -29,12 +29,12 @@ include "static_2/relocation/lifts.ma".
          frees_fqus_drops requires fqu_drop restricted on atoms
 *)
 inductive fqu (b:bool): tri_relation genv lenv term ≝
-| fqu_lref_O : ∀I,G,L,V. fqu b G (L.ⓑ{I}V) (#0) G L V
-| fqu_pair_sn: ∀I,G,L,V,T. fqu b G L (②{I}V.T) G L V
-| fqu_bind_dx: ∀p,I,G,L,V,T. b = Ⓣ → fqu b G L (ⓑ{p,I}V.T) G (L.ⓑ{I}V) T
-| fqu_clear  : ∀p,I,G,L,V,T. b = Ⓕ → fqu b G L (ⓑ{p,I}V.T) G (L.ⓧ) T
-| fqu_flat_dx: ∀I,G,L,V,T. fqu b G L (ⓕ{I}V.T) G L T
-| fqu_drop   : ∀I,G,L,T,U. ⇧*[1] T ≘ U → fqu b G (L.ⓘ{I}) U G L T
+| fqu_lref_O : ∀I,G,L,V. fqu b G (L.ⓑ[I]V) (#0) G L V
+| fqu_pair_sn: ∀I,G,L,V,T. fqu b G L (②[I]V.T) G L V
+| fqu_bind_dx: ∀p,I,G,L,V,T. b = Ⓣ → fqu b G L (ⓑ[p,I]V.T) G (L.ⓑ[I]V) T
+| fqu_clear  : ∀p,I,G,L,V,T. b = Ⓕ → fqu b G L (ⓑ[p,I]V.T) G (L.ⓧ) T
+| fqu_flat_dx: ∀I,G,L,V,T. fqu b G L (ⓕ[I]V.T) G L T
+| fqu_drop   : ∀I,G,L,T,U. ⇧*[1] T ≘ U → fqu b G (L.ⓘ[I]) U G L T
 .
 
 interpretation
@@ -47,20 +47,20 @@ interpretation
 
 (* Basic properties *********************************************************)
 
-lemma fqu_sort: â\88\80b,I,G,L,s. â¦\83G,L.â\93\98{I},â\8b\86sâ¦\84 â¬\82[b] â¦\83G,L,â\8b\86sâ¦\84.
+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. â¦\83G,L.â\93\98{I},#â\86\91iâ¦\84 â¬\82[b] â¦\83G,L,#iâ¦\84.
+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. â¦\83G,L.â\93\98{I},§lâ¦\84 â¬\82[b] â¦\83G,L,§lâ¦\84.
+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. â¦\83G1,L1,T1â¦\84 â¬\82[b] â¦\83G2,L2,T2â¦\84 →
+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.
+                        ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & T2 = ⋆s.
 #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
 [ #I #G #L #T #s #H destruct
 | #I #G #L #V #T #s #H destruct
@@ -72,14 +72,14 @@ 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. â¦\83G1,L1,â\8b\86sâ¦\84 â¬\82[b] â¦\83G2,L2,T2â¦\84 →
-                     ∃∃J. G1 = G2 & L1 = L2.ⓘ{J} & T2 = ⋆s.
+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. â¦\83G1,L1,T1â¦\84 â¬\82[b] â¦\83G2,L2,T2â¦\84 →
+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.
+                        (∃∃J,V. G1 = G2 & L1 = L2.ⓑ[J]V & T2 = V & i = 0) ∨
+                        ∃∃J,j. G1 = G2 & L1 = L2.ⓘ[J] & T2 = #j & i = ↑j.
 #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
 [ #I #G #L #T #i #H destruct /3 width=4 by ex4_2_intro, or_introl/
 | #I #G #L #V #T #i #H destruct
@@ -91,14 +91,14 @@ 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. â¦\83G1,L1,#iâ¦\84 â¬\82[b] â¦\83G2,L2,T2â¦\84 →
-                     (∃∃J,V. G1 = G2 & L1 = L2.ⓑ{J}V & T2 = V & i = 0) ∨
-                     ∃∃J,j. G1 = G2 & L1 = L2.ⓘ{J} & T2 = #j & i = ↑j.
+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. â¦\83G1,L1,T1â¦\84 â¬\82[b] â¦\83G2,L2,T2â¦\84 →
+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.
+                        ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & T2 = §l.
 #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
 [ #I #G #L #T #l #H destruct
 | #I #G #L #V #T #l #H destruct
@@ -110,16 +110,16 @@ 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. â¦\83G1,L1,§lâ¦\84 â¬\82[b] â¦\83G2,L2,T2â¦\84 →
-                     ∃∃J. G1 = G2 & L1 = L2.ⓘ{J} & T2 = §l.
+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. â¦\83G1,L1,T1â¦\84 â¬\82[b] â¦\83G2,L2,T2â¦\84 →
-                        ∀p,I,V1,U1. T1 = ⓑ{p,I}V1.U1 →
+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 = Ⓣ
+                         | ∧∧ 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.
+                         | ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & ⇧*[1] T2 ≘ ⓑ[p,I]V1.U1.
 #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
 [ #I #G #L #T #q #J #V0 #U0 #H destruct
 | #I #G #L #V #T #q #J #V0 #U0 #H destruct /3 width=1 by and3_intro, or4_intro0/
@@ -130,28 +130,28 @@ 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. â¦\83G1,L1,â\93\91{p,I}V1.U1â¦\84 â¬\82[b] â¦\83G2,L2,T2â¦\84 →
+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.ⓑ[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.
+                      | ∃∃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. â¦\83G1,L1,â\93\91{p,I}V1.U1â¦\84 â¬\82 â¦\83G2,L2,T2â¦\84 →
+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.
+                           | ∧∧ G1 = G2 & L1.ⓑ[I]V1 = L2 & U1 = T2
+                           | ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & ⇧*[1] T2 ≘ ⓑ[p,I]V1.U1.
 #p #I #G1 #G2 #L1 #L2 #V1 #U1 #T2 #H elim (fqu_inv_bind1 … H) -H
 /3 width=1 by or3_intro0, or3_intro2/
 * #HG #HL #HU #H destruct
 /3 width=1 by and3_intro, or3_intro1/
 qed-.
 
-fact fqu_inv_flat1_aux: â\88\80b,G1,G2,L1,L2,T1,T2. â¦\83G1,L1,T1â¦\84 â¬\82[b] â¦\83G2,L2,T2â¦\84 →
-                        ∀I,V1,U1. T1 = ⓕ{I}V1.U1 →
+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
-                         | ∃∃J. G1 = G2 & L1 = L2.ⓘ{J} & ⇧*[1] T2 ≘ ⓕ{I}V1.U1.
+                         | ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & ⇧*[1] T2 ≘ ⓕ[I]V1.U1.
 #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
 [ #I #G #L #T #J #V0 #U0 #H destruct
 | #I #G #L #V #T #J #V0 #U0 #H destruct /3 width=1 by and3_intro, or3_intro0/
@@ -162,39 +162,39 @@ 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. â¦\83G1,L1,â\93\95{I}V1.U1â¦\84 â¬\82[b] â¦\83G2,L2,T2â¦\84 →
+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.
+                      | ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & ⇧*[1] T2 ≘ ⓕ[I]V1.U1.
 /2 width=4 by fqu_inv_flat1_aux/ qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma fqu_inv_atom1: â\88\80b,I,G1,G2,L2,T2. â¦\83G1,â\8b\86,â\93ª{I}â¦\84 â¬\82[b] â¦\83G2,L2,T2â¦\84 → ⊥.
+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. â¦\83G1,K.â\93\98{I},â\8b\86sâ¦\84 â¬\82[b] â¦\83G2,L2,T2â¦\84 →
+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. â¦\83G1,K.â\93\91{I}V,#0â¦\84 â¬\82[b] â¦\83G2,L2,T2â¦\84 →
+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. â¦\83G1,K.â\93\98{I},#(â\86\91i)â¦\84 â¬\82[b] â¦\83G2,L2,T2â¦\84 →
+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. â¦\83G1,K.â\93\98{I},§lâ¦\84 â¬\82[b] â¦\83G2,L2,T2â¦\84 →
+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/