X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv_cpme.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv_cpme.ma;h=a9091b059071c8c6c2216e1d87ff3d0969b7b0d7;hb=cacd7323994f7621286dbfd93bbf4c50acfbe918;hp=be0443bca6b90a7c39ee7cb6ea80ec2745b1be67;hpb=f76594123e375bd7852c9421fe260a7bec693a92;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpme.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpme.ma
index be0443bca..a9091b059 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpme.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpme.ma
@@ -35,3 +35,13 @@ elim (cnv_cpms_conf … HT0 … HT01 … HT02) -T0 <minus_n_n #T0 #HT10 #HT20
 lapply (cprs_inv_cnr_sn … HT20 HT2) -HT20 #H destruct
 /2 width=1 by conj/
 qed-.
+
+(* Main properties with evaluation for t-bound rt-transition on terms *****)
+
+theorem cnv_cpme_mono (a) (h) (n) (G) (L):
+        ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∀T1. ⦃G,L⦄ ⊢ T ➡*[h,n] 𝐍⦃T1⦄ →
+        ∀T2. ⦃G,L⦄ ⊢ T ➡*[h,n] 𝐍⦃T2⦄ → T1 = T2.
+#a #h #n #G #L #T0 #HT0 #T1 * #HT01 #HT1 #T2 * #HT02 #HT2
+elim (cnv_cpms_conf … HT0 … HT01 … HT02) -T0 <minus_n_n #T0 #HT10 #HT20
+/3 width=7 by cprs_inv_cnr_sn, canc_dx_eq/
+qed-.