-#G #L @TC_strip1 /2 width=3 by cpr_conf/ qed-. (**) (* auto /3 width=3/ does not work because a δ-expansion gets in the way *)
-
-lemma cprs_lpr_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 → ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 →
- ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T.
-#G #L0 #T0 #T1 #H elim H -T1
-[ #T1 #HT01 #L1 #HL01
- elim (lpr_cpr_conf_dx … HT01 … HL01) -L0 /3 width=3/
-| #T #T1 #_ #HT1 #IHT0 #L1 #HL01
- elim (IHT0 … HL01) #T2 #HT2 #HT02
- elim (lpr_cpr_conf_dx … HT1 … HL01) -L0 #T3 #HT3 #HT13
- elim (cprs_strip … HT2 … HT3) -T #T #HT2 #HT3
- lapply (cprs_strap2 … HT13 … HT3) -T3
- lapply (cprs_strap1 … HT02 … HT2) -T2 /2 width=3/
-]
+normalize /4 width=3 by cpr_conf, TC_strip1/ qed-.
+
+lemma cprs_llpr_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 → ∀L1. ⦃G, L0⦄ ⊢ ➡[T0, 0] L1 →
+ ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T.
+#G #L0 #T0 #T1 #H @(cprs_ind_dx … T0 H) -T0 /2 width=3 by ex2_intro/
+#T0 #T #HT0 #_ #IHT1 #L1 #HL01
+elim (IHT1 … L1) /2 by llpr_cpr_conf/ -IHT1 #T2 #HT12 #HT2
+elim (llpr_cpr_conf_dx … HT0 … HL01) -L0 #T3 #HT03 #HT3
+elim (cprs_strip … HT2 … HT3) -T
+/4 width=5 by cprs_strap2, cprs_strap1, ex2_intro/