+/4 width=3 by lprs_inv_CTC, lprs_CTC, lpr_cprs_trans, lex_CTC_step_dx/ qed-.
+
+lemma lprs_strip (h) (G): confluent2 … (lprs h G) (lpr h G).
+#h #G #L0 #L1 #HL01 #L2 #HL02
+elim (TC_strip1 … L1 ?? HL02) -HL02
+[ /3 width=3 by lprs_TC, ex2_intro/ | skip
+| /2 width=1 by lprs_inv_TC/
+| /2 width=3 by lpr_conf/
+]
+qed-.