- the relation for pointwise extensions now takes a binder as argument

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / fquq_alt.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_alt.ma
index 033959bea950c686a63bb39769a447d4693f836b..c1048857c53a3526f7f2b5d5a427074932651738 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_alt.ma
@@ -30,7 +30,7 @@ lemma fquqa_refl: tri_reflexive … fquqa.
 // qed.
 
 lemma fquqa_drop: ∀G,L,K,T,U,e.
-                  â\87©[e] L â\89¡ K â\86\92 â\87§[0, e] T â\89¡ U â\86\92 â¦\83G, L, Uâ¦\84 â\8a\83â\8a\83⸮ ⦃G, K, T⦄.
+                  â\87©[e] L â\89¡ K â\86\92 â\87§[0, e] T â\89¡ U â\86\92 â¦\83G, L, Uâ¦\84 â\8a\90â\8a\90⸮ ⦃G, K, T⦄.
 #G #L #K #T #U #e #HLK #HTU elim (eq_or_gt e)
 /3 width=5 by fqu_drop_lt, or_introl/ #H destruct
 >(ldrop_inv_O2 … HLK) -L >(lift_inv_O2 … HTU) -T //
@@ -38,22 +38,22 @@ qed.
 
 (* Main properties **********************************************************)
 
-theorem fquq_fquqa: â\88\80G1,G2,L1,L2,T1,T2. â¦\83G1, L1, T1â¦\84 â\8a\83⸮ â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 â\8a\83â\8a\83⸮ ⦃G2, L2, T2⦄.
+theorem fquq_fquqa: â\88\80G1,G2,L1,L2,T1,T2. â¦\83G1, L1, T1â¦\84 â\8a\90⸮ â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 â\8a\90â\8a\90⸮ ⦃G2, L2, T2⦄.
 #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
 /2 width=3 by fquqa_drop, fqu_lref_O, fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, or_introl/
 qed.
 
 (* Main inversion properties ************************************************)
 
-theorem fquqa_inv_fquq: â\88\80G1,G2,L1,L2,T1,T2. â¦\83G1, L1, T1â¦\84 â\8a\83â\8a\83⸮ â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 â\8a\83⸮ ⦃G2, L2, T2⦄.
+theorem fquqa_inv_fquq: â\88\80G1,G2,L1,L2,T1,T2. â¦\83G1, L1, T1â¦\84 â\8a\90â\8a\90⸮ â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 â\8a\90⸮ ⦃G2, L2, T2⦄.
 #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H /2 width=1 by fqu_fquq/
 * #H1 #H2 #H3 destruct //
 qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma fquq_inv_gen: â\88\80G1,G2,L1,L2,T1,T2. â¦\83G1, L1, T1â¦\84 â\8a\83⸮ ⦃G2, L2, T2⦄ →
-                    â¦\83G1, L1, T1â¦\84 â\8a\83 ⦃G2, L2, T2⦄ ∨ (∧∧ G1 = G2 & L1 = L2 & T1 = T2).
+lemma fquq_inv_gen: â\88\80G1,G2,L1,L2,T1,T2. â¦\83G1, L1, T1â¦\84 â\8a\90⸮ ⦃G2, L2, T2⦄ →
+                    â¦\83G1, L1, T1â¦\84 â\8a\90 ⦃G2, L2, T2⦄ ∨ (∧∧ G1 = G2 & L1 = L2 & T1 = T2).
 #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fquq_fquqa … H) -H [| * ]
 /2 width=1 by or_introl/
 qed-.