(* Inversion lemmas with sort-irrelevant equivalence for terms **************)
-lemma cpm_teqx_inv_lref_sn (n) (h) (G) (L) (i):
- ∀X. ❪G,L❫ ⊢ #i ➡[n,h] X → #i ≛ X →
+lemma cpm_teqx_inv_lref_sn (h) (n) (G) (L) (i):
+ ∀X. ❪G,L❫ ⊢ #i ➡[h,n] X → #i ≛ X →
∧∧ X = #i & n = 0.
-#n #h #G #L #i #X #H1 #H2
+#h #n #G #L #i #X #H1 #H2
lapply (teqx_inv_lref1 … H2) -H2 #H destruct
elim (cpm_inv_lref1_drops … H1) -H1 // * [| #m ]
#K #V1 #V2 #_ #_ #H -V1
elim (lifts_inv_lref2_uni_lt … H) -H //
qed-.
-lemma cpm_teqx_inv_atom_sn (n) (h) (I) (G) (L):
- ∀X. ❪G,L❫ ⊢ ⓪[I] ➡[n,h] X → ⓪[I] ≛ X →
+lemma cpm_teqx_inv_atom_sn (h) (n) (I) (G) (L):
+ ∀X. ❪G,L❫ ⊢ ⓪[I] ➡[h,n] X → ⓪[I] ≛ X →
∨∨ ∧∧ X = ⓪[I] & n = 0
| ∃∃s. X = ⋆(⫯[h]s) & I = Sort s & n = 1.
-#n #h * #s #G #L #X #H1 #H2
+#h #n * #s #G #L #X #H1 #H2
[ elim (cpm_inv_sort1 … H1) -H1
cases n -n [| #n ] #H #Hn destruct -H2
[ /3 width=1 by or_introl, conj/