X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc%2Fcpxs%2Fcpxs.etc;h=05e7c375dff3e786db123b57f82111c8bbce40ce;hb=18d7afd216aee6c815eac30982d8ad4fa4521070;hp=ada873d816ad1e18da99ed75d40c21108da0808a;hpb=1de84a809c842fbc8a4e0d92b9bc61763c0e6fae;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc
index ada873d81..05e7c375d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc
@@ -1,18 +1,9 @@
-lemma lsubr_cpxs_trans: ∀h,o,G. lsub_trans … (cpxs h o G) lsubr.
-/3 width=5 by lsubr_cpx_trans, LTC_lsub_trans/
-qed-.
 
 lemma cprs_cpxs: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈* T2 → ⦃G, L⦄ ⊢ T1 ⬈*[h] T2.
 #h #o #G #L #T1 #T2 #H @(cprs_ind … H) -T2 /3 width=3 by cpxs_strap1,
 cpr_cpx/
 qed.
 
-lemma cpxs_inv_cnx1: ∀h,o,G,L,T,U. ⦃G, L⦄ ⊢ T ⬈*[h] U → ⦃G, L⦄ ⊢ ⬈[h] 𝐍⦃T⦄ → T = U.
-#h #o #G #L #T #U #H @(cpxs_ind_dx … H) -T //
-#T0 #T #H1T0 #_ #IHT #H2T0
-lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1 by/
-qed-.
-
 lemma cpxs_neq_inv_step_sn: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 = T2 → ⊥) →
                             ∃∃T. ⦃G, L⦄ ⊢ T1 ⬈[h] T & T1 = T → ⊥ & ⦃G, L⦄ ⊢ T ⬈*[h] T2.
 #h #o #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1