]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
update in ground_2 and basic_2 ...
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / cpy.ma
index 66852c667b6f4fcd0e76cc26387070320b41b420..cf29f1cc2ba48a5501fd2962faaf89ff07544fa0 100644 (file)
@@ -41,7 +41,7 @@ lemma lsuby_cpy_trans: ∀G,d,e. lsub_trans … (cpy d e G) (lsuby d e).
 #G #d #e #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2 -d -e
 [ //
 | #I #G #L1 #K1 #V #W #i #d #e #Hdi #Hide #HLK1 #HVW #L2 #HL12
-  elim (lsuby_fwd_ldrop2_be … HL12 … HLK1) -HL12 -HLK1 /2 width=5 by cpy_subst/
+  elim (lsuby_ldrop_trans_be … HL12 … HLK1) -HL12 -HLK1 /2 width=5 by cpy_subst/
 | /4 width=1 by lsuby_succ, cpy_bind/
 | /3 width=1 by cpy_flat/
 ]
@@ -83,6 +83,7 @@ lemma cpy_weak: ∀G,L,T1,T2,d1,e1. ⦃G, L⦄ ⊢ T1 ▶[d1, e1] T2 →
 ]
 qed-.
 
+(* Note: lemma 1250 *)
 lemma cpy_weak_top: ∀G,L,T1,T2,d,e.
                     ⦃G, L⦄ ⊢ T1 ▶[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶[d, |L| - d] T2.
 #G #L #T1 #T2 #d #e #H elim H -G -L -T1 -T2 -d -e //