update in ground_2, static_2, basic_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / s_computation / fqup_drops.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/s_computation/fqup_drops.ma b/matita/matita/contribs/lambdadelta/static_2/s_computation/fqup_drops.ma
index c21d46c6026be363201aa91140a85b6e272829f8..2b5173d75bfbb82709e3a043b1a5ad92347252e9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/s_computation/fqup_drops.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/s_computation/fqup_drops.ma
@@ -19,21 +19,21 @@ include "static_2/s_computation/fqup.ma".
 
 (* Properties with generic slicing for local environments *******************)
 
-lemma fqup_drops_succ: â\88\80b,G,K,T,i,L,U. â¬\87*[â\86\91i] L â\89\98 K â\86\92 â¬\86*[↑i] T ≘ U →
-                       â¦\83G,L,Uâ¦\84 â¬\82+[b] â¦\83G,K,Tâ¦\84.
+lemma fqup_drops_succ: â\88\80b,G,K,T,i,L,U. â\87©[â\86\91i] L â\89\98 K â\86\92 â\87§[↑i] T ≘ U →
+                       â\9dªG,L,Uâ\9d« â¬\82+[b] â\9dªG,K,Tâ\9d«.
 #b #G #K #T #i elim i -i
 [ #L #U #HLK #HTU elim (drops_inv_succ … HLK) -HLK
   #I #Y #HY #H destruct <(drops_fwd_isid … HY) -K //
   /3 width=2 by fqu_fqup, fqu_drop/
 | #l #IH #L #U #HLK #HTU elim (drops_inv_succ … HLK) -HLK
   #I #Y #HY #H destruct
-  elim (lifts_split_trans â\80¦ HTU â\80¦ (ð\9d\90\94â\9d´â\86\91lâ\9dµ) (ð\9d\90\94â\9d´1â\9dµ)) -HTU
+  elim (lifts_split_trans â\80¦ HTU â\80¦ (ð\9d\90\94â\9d¨â\86\91lâ\9d©) (ð\9d\90\94â\9d¨1â\9d©)) -HTU
   /4 width=5 by fqup_strap2, fqu_drop/
 ]
 qed.
 
-lemma fqup_drops_strap1: â\88\80b,G1,G2,L1,K1,K2,T1,T2,U1,i. â¬\87*[i] L1 â\89\98 K1 â\86\92 â¬\86*[i] T1 ≘ U1 →
-                         â¦\83G1,K1,T1â¦\84 â¬\82[b] â¦\83G2,K2,T2â¦\84 â\86\92 â¦\83G1,L1,U1â¦\84 â¬\82+[b] â¦\83G2,K2,T2â¦\84.
+lemma fqup_drops_strap1: â\88\80b,G1,G2,L1,K1,K2,T1,T2,U1,i. â\87©[i] L1 â\89\98 K1 â\86\92 â\87§[i] T1 ≘ U1 →
+                         â\9dªG1,K1,T1â\9d« â¬\82[b] â\9dªG2,K2,T2â\9d« â\86\92 â\9dªG1,L1,U1â\9d« â¬\82+[b] â\9dªG2,K2,T2â\9d«.
 #b #G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 *
 [ #HLK1 #HTU1 #HT12
   >(drops_fwd_isid … HLK1) -L1 //
@@ -42,5 +42,5 @@ lemma fqup_drops_strap1: ∀b,G1,G2,L1,K1,K2,T1,T2,U1,i. ⬇*[i] L1 ≘ K1 → 
 ]
 qed-.
 
-lemma fqup_lref: â\88\80b,I,G,L,K,V,i. â¬\87*[i] L â\89\98 K.â\93\91{I}V â\86\92 â¦\83G,L,#iâ¦\84 â¬\82+[b] â¦\83G,K,Vâ¦\84.
+lemma fqup_lref: â\88\80b,I,G,L,K,V,i. â\87©[i] L â\89\98 K.â\93\91[I]V â\86\92 â\9dªG,L,#iâ\9d« â¬\82+[b] â\9dªG,K,Vâ\9d«.
 /2 width=6 by fqup_drops_strap1/ qed.