update in basic_2 and ground_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu.ma b/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu.ma
index 0f5feb7fc88c4739f3f83d303138aa8500a120d7..85ddd67c76ce265aaf40ea9e0f971a1fbae6dd84 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu.ma
@@ -31,7 +31,7 @@ inductive fqu (b:bool): tri_relation genv lenv term ≝
 | fqu_bind_dx: ∀p,I,G,L,V,T. 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   : â\88\80I,G,L,T,U. â¬\86*[1] T â\89¡ U → fqu b G (L.ⓘ{I}) U G L T
+| fqu_drop   : â\88\80I,G,L,T,U. â¬\86*[1] T â\89\98 U → fqu b G (L.ⓘ{I}) U G L T
 .
 
 interpretation
@@ -116,7 +116,7 @@ fact fqu_inv_bind1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L
                         ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
                          | ∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & U1 = T2
                          | ∧∧ G1 = G2 & L1.ⓧ = L2 & U1 = T2 & b = Ⓕ
-                         | â\88\83â\88\83J. G1 = G2 & L1 = L2.â\93\98{J} & â¬\86*[1] T2 â\89¡ ⓑ{p,I}V1.U1.
+                         | â\88\83â\88\83J. G1 = G2 & L1 = L2.â\93\98{J} & â¬\86*[1] T2 â\89\98 ⓑ{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/
@@ -131,13 +131,13 @@ lemma fqu_inv_bind1: ∀b,p,I,G1,G2,L1,L2,V1,U1,T2. ⦃G1, L1, ⓑ{p,I}V1.U1⦄
                      ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
                       | ∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & U1 = T2
                       | ∧∧ G1 = G2 & L1.ⓧ = L2 & U1 = T2 & b = Ⓕ
-                      | â\88\83â\88\83J. G1 = G2 & L1 = L2.â\93\98{J} & â¬\86*[1] T2 â\89¡ ⓑ{p,I}V1.U1.
+                      | â\88\83â\88\83J. G1 = G2 & L1 = L2.â\93\98{J} & â¬\86*[1] T2 â\89\98 ⓑ{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⦄ →
                           ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
                            | ∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & U1 = T2
-                           | â\88\83â\88\83J. G1 = G2 & L1 = L2.â\93\98{J} & â¬\86*[1] T2 â\89¡ ⓑ{p,I}V1.U1.
+                           | â\88\83â\88\83J. G1 = G2 & L1 = L2.â\93\98{J} & â¬\86*[1] T2 â\89\98 ⓑ{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_intro1, or3_intro2/
 * #_ #_ #_ #H destruct
@@ -147,7 +147,7 @@ fact fqu_inv_flat1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L
                         ∀I,V1,U1. T1 = ⓕ{I}V1.U1 →
                         ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
                          | ∧∧ G1 = G2 & L1 = L2 & U1 = T2
-                         | â\88\83â\88\83J. G1 = G2 & L1 = L2.â\93\98{J} & â¬\86*[1] T2 â\89¡ ⓕ{I}V1.U1.
+                         | â\88\83â\88\83J. G1 = G2 & L1 = L2.â\93\98{J} & â¬\86*[1] T2 â\89\98 ⓕ{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/
@@ -161,7 +161,7 @@ qed-.
 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
-                      | â\88\83â\88\83J. G1 = G2 & L1 = L2.â\93\98{J} & â¬\86*[1] T2 â\89¡ ⓕ{I}V1.U1.
+                      | â\88\83â\88\83J. G1 = G2 & L1 = L2.â\93\98{J} & â¬\86*[1] T2 â\89\98 ⓕ{I}V1.U1.
 /2 width=4 by fqu_inv_flat1_aux/ qed-.
 
 (* Advanced inversion lemmas ************************************************)