- lambda_delta: subject reduction for nativa type assignment begins ...

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / equivalence / cpcs_cprs.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma
index 1fb994c7194c424c87e43a92b458ac6af6a3a29b..7394858efe4b089cd987a9f4d383bb62e49235db 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma
@@ -24,11 +24,17 @@ lemma cpcs_cprs_dx: ∀L,T1,T2. L ⊢ T1 ➡* T2 → L ⊢ T1 ⬌* T2.
 #L #T1 #T2 #H @(cprs_ind … H) -T2 /width=1/ /3 width=3/
 qed.
 
+lemma cpcs_tpr_dx: ∀L,T1,T2. T1 ➡ T2 → L ⊢ T1 ⬌* T2.
+/3 width=1/ qed.
+
 (* Basic_1: was: pc3_pr3_x *)
 lemma cpcs_cprs_sn: ∀L,T1,T2. L ⊢ T2 ➡* T1 → L ⊢ T1 ⬌* T2.
 #L #T1 #T2 #H @(cprs_ind_dx … H) -T2 /width=1/ /3 width=3/
 qed.
 
+lemma cpcs_tpr_sn: ∀L,T1,T2. T2 ➡ T1 → L ⊢ T1 ⬌* T2.
+/3 width=1/ qed.
+
 lemma cpcs_cprs_strap1: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T ➡* T2 → L ⊢ T1 ⬌* T2.
 #L #T1 #T #HT1 #T2 #H @(cprs_ind … H) -T2 /width=1/ /2 width=3/
 qed.