X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc_2A1%2Fappend%2Fcpys2.etc;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc_2A1%2Fappend%2Fcpys2.etc;h=22f74d0a8e7eba070ee539a0c4a89f5c735a1c55;hb=09b4420070d6a71990e16211e499b51dbb0742cb;hp=0000000000000000000000000000000000000000;hpb=bba53a83579540bc3925d47d679e2aad22e85755;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/append/cpys2.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/append/cpys2.etc
new file mode 100644
index 000000000..22f74d0a8
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/append/cpys2.etc
@@ -0,0 +1,14 @@
+lemma cpys_append: ∀G,d,e. l_appendable_sn … (cpys d e G).
+#G #d #e #K #T1 #T2 #H @(cpys_ind … H) -T2
+/3 width=3 by cpys_strap1, cpy_append/
+qed-.
+
+lemma cpys_fwd_shift1: ∀G,L,L1,T1,T,d,e. ⦃G, L⦄ ⊢ L1 @@ T1 ▶*[d, e] T →
+                       ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
+#G #L #L1 #T1 #T #d #e #H @(cpys_ind … H) -T
+[ /2 width=4 by ex2_2_intro/
+| #T #X #_ #HX * #L0 #T0 #HL10 #H destruct
+  elim (cpy_fwd_shift1 … HX) -HX #L2 #T2 #HL02 #H destruct
+  /2 width=4 by ex2_2_intro/
+]
+qed-.