+ ∀T2,d,e. L ⊢ T ▶ [d, e] T2 → L ⊢ T1 ➡ T2.
+/3 width=5/ qed.
+
+lemma cpr_tpss_conf: ∀L,T0,T1. L ⊢ T0 ➡ T1 →
+ ∀T2,d,e. L ⊢ T0 ▶* [d, e] T2 →
+ ∃∃T. L ⊢ T1 ▶* [d, e] T & L ⊢ T2 ➡ T.
+#L #T0 #T1 * #U0 #HTU0 #HU0T1 #T2 #d #e #HT02
+elim (tpr_tpss_conf … HTU0 … HT02) -T0 #T0 #HT20 #HUT0
+elim (tpss_conf_eq … HU0T1 … HUT0) -U0 /3 width=5/
+qed-.