still more additions and corrections for the article

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / cnv_cpme.ma

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 be0443bca6b90a7c39ee7cb6ea80ec2745b1be67..a9091b059071c8c6c2216e1d87ff3d0969b7b0d7 100644 (file)
--- 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-.