+lemma cpr_cprs_conf: ∀L,T,T1,T2. L ⊢ T ➡* T1 → L ⊢ T ➡ T2 → L ⊢ T1 ⬌* T2.
+#L #T #T1 #T2 #HT1 #HT2
+elim (cprs_strip … HT1 … HT2) /2 width=3 by cpr_cprs_div/
+qed-.
+
+lemma cprs_cpr_conf: ∀L,T,T1,T2. L ⊢ T ➡* T1 → L ⊢ T ➡ T2 → L ⊢ T2 ⬌* T1.
+#L #T #T1 #T2 #HT1 #HT2
+elim (cprs_strip … HT1 … HT2) /2 width=3 by cprs_cpr_div/
+qed-.
+
+lemma cprs_conf: ∀L,T,T1,T2. L ⊢ T ➡* T1 → L ⊢ T ➡* T2 → L ⊢ T1 ⬌* T2.
+#L #T #T1 #T2 #HT1 #HT2
+elim (cprs_conf … HT1 … HT2) /2 width=3/
+qed-.
+