(* Basic_1: was: pc3_pr3_conf *)
lemma cpcs_cprs_conf: ∀L,T1,T. L ⊢ T ➡* T1 → ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2.
#L #T1 #T #H #T2 #HT2 @(cprs_ind … H) -T1 /width=1/ /2 width=3/
qed.
(* Basic_1: was: pc3_pr3_conf *)
lemma cpcs_cprs_conf: ∀L,T1,T. L ⊢ T ➡* T1 → ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2.
#L #T1 #T #H #T2 #HT2 @(cprs_ind … H) -T1 /width=1/ /2 width=3/
qed.