(* Inversion lemmas with sort-irrelevant equivalence for terms **************)
lemma cpm_teqx_inv_lref_sn (h) (n) (G) (L) (i):
- â\88\80X. â\9dªG,Lâ\9d« ⊢ #i ➡[h,n] X → #i ≅ X →
+ â\88\80X. â\9d¨G,Lâ\9d© ⊢ #i ➡[h,n] X → #i ≅ X →
∧∧ X = #i & n = 0.
#h #n #G #L #i #X #H1 #H2
lapply (teqg_inv_lref1 … H2) -H2 #H destruct
qed-.
lemma cpm_teqx_inv_atom_sn (h) (n) (I) (G) (L):
- â\88\80X. â\9dªG,Lâ\9d« ⊢ ⓪[I] ➡[h,n] X → ⓪[I] ≅ X →
+ â\88\80X. â\9d¨G,Lâ\9d© ⊢ ⓪[I] ➡[h,n] X → ⓪[I] ≅ X →
∨∨ ∧∧ X = ⓪[I] & n = 0
| ∃∃s. X = ⋆(⫯[h]s) & I = Sort s & n = 1.
#h #n * #s #G #L #X #H1 #H2