+(* Basic_1: uses: ty3_sred_wcpr0_pr0 *)
+lemma nta_cpr_conf_lpr (a) (h) (G):
+ ∀L1,T1,U. ⦃G,L1⦄ ⊢ T1 :[a,h] U → ∀T2. ⦃G,L1⦄ ⊢ T1 ➡[h] T2 →
+ ∀L2. ⦃G,L1⦄ ⊢ ➡[h] L2 → ⦃G,L2⦄ ⊢ T2 :[a,h] U.
+#a #h #G #L1 #T1 #U #H #T2 #HT12 #L2 #HL12
+/3 width=6 by cnv_cpm_trans_lpr, cpm_cast/
+qed-.
+
+(* Basic_1: uses: ty3_sred_pr2 ty3_sred_pr0 *)
+lemma nta_cpr_conf (a) (h) (G) (L):
+ ∀T1,U. ⦃G,L⦄ ⊢ T1 :[a,h] U →
+ ∀T2. ⦃G,L⦄ ⊢ T1 ➡[h] T2 → ⦃G,L⦄ ⊢ T2 :[a,h] U.
+#a #h #G #L #T1 #U #H #T2 #HT12
+/3 width=6 by cnv_cpm_trans, cpm_cast/
+qed-.
+
+(* Note: this is the preservation property *)
+(* Basic_1: uses: ty3_sred_pr3 ty3_sred_pr1 *)
+lemma nta_cprs_conf (a) (h) (G) (L):
+ ∀T1,U. ⦃G,L⦄ ⊢ T1 :[a,h] U →
+ ∀T2. ⦃G,L⦄ ⊢ T1 ➡*[h] T2 → ⦃G,L⦄ ⊢ T2 :[a,h] U.
+#a #h #G #L #T1 #U #H #T2 #HT12
+/3 width=6 by cnv_cpms_trans, cpms_cast/
+qed-.
+
+(* Basic_1: uses: ty3_cred_pr2 *)
+lemma nta_lpr_conf (a) (h) (G):
+ ∀L1,T,U. ⦃G,L1⦄ ⊢ T :[a,h] U →
+ ∀L2. ⦃G,L1⦄ ⊢ ➡[h] L2 → ⦃G,L2⦄ ⊢ T :[a,h] U.
+#a #h #G #L1 #T #U #HTU #L2 #HL12
+/2 width=3 by cnv_lpr_trans/
+qed-.
+
+(* Basic_1: uses: ty3_cred_pr3 *)
+lemma nta_lprs_conf (a) (h) (G):
+ ∀L1,T,U. ⦃G,L1⦄ ⊢ T :[a,h] U →
+ ∀L2. ⦃G,L1⦄ ⊢ ➡*[h] L2 → ⦃G,L2⦄ ⊢ T :[a,h] U.
+#a #h #G #L1 #T #U #HTU #L2 #HL12
+/2 width=3 by cnv_lprs_trans/
+qed-.
+