-lemma cprs_strip: ∀L. confluent2 … (cprs L) (cpr L).
-#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: ∀L0,T0,T1. L0 ⊢ T0 ➡* T1 → ∀L1. L0 ⊢ ➡ L1 →
- ∃∃T. L1 ⊢ T1 ➡* T & L1 ⊢ T0 ➡* T.
-#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/
-]
+lemma cprs_strip: ∀G,L. confluent2 … (cprs G L) (cpr G L).
+normalize /4 width=3 by cpr_conf, TC_strip1/ qed-.
+
+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 @(cprs_ind … H) -T1 /2 width=3 by ex2_intro/
+#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
+/4 width=5 by cprs_strap2, cprs_strap1, ex2_intro/