/3 width=3 by cprs_CTC, lex_co/ qed.
(* Inversion lemmas with contextual transitive closure **********************)
lemma lprs_inv_CTC (h) (G):
/3 width=3 by cprs_CTC, lex_co/ qed.
(* Inversion lemmas with contextual transitive closure **********************)
lemma lprs_inv_CTC (h) (G):