(* Inversion lemmas with sort-irrelevant equivalence for terms **************)
lemma cpm_teqx_inv_lref_sn (h) (n) (G) (L) (i):
(* Inversion lemmas with sort-irrelevant equivalence for terms **************)
lemma cpm_teqx_inv_lref_sn (h) (n) (G) (L) (i):