-lemma snv_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ U ¡[h, g] → ∀K,s,d,e. ⇩[s, d, e] L ≡ K →
- â\88\80T. â\87§[d, e] T â\89¡ U â\86\92 â¦\83G, Kâ¦\84 â\8a¢ T ¡[h, g].
-#h #g #G #L #U #H elim H -G -L -U
-[ #G #L #k #K #s #d #e #_ #X #H
- >(lift_inv_sort2 … H) -X -L -d -e //
-| #I #G #L #L0 #W #i #HL0 #_ #IHW #K #s #d #e #HLK #X #H
- elim (lift_inv_lref2 … H) * #Hid #H destruct
- [ elim (drop_conf_le … HLK … HL0) -L /2 width=2 by lt_to_le/ #X #HK0 #H
- elim (drop_inv_skip1 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hid #K0 #V #HLK0 #HVW #H destruct
+lemma snv_inv_lift: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ U ¡[h, o] → ∀K,b,l,k. ⬇[b, l, k] L ≡ K →
+ â\88\80T. â¬\86[l, k] T â\89¡ U â\86\92 â¦\83G, Kâ¦\84 â\8a¢ T ¡[h, o].
+#h #o #G #L #U #H elim H -G -L -U
+[ #G #L #s #K #b #l #k #_ #X #H
+ >(lift_inv_sort2 … H) -X -L -l -k //
+| #I #G #L #L0 #W #i #HL0 #_ #IHW #K #b #l #k #HLK #X #H
+ elim (lift_inv_lref2 … H) * #Hil #H destruct
+ [ elim (drop_conf_le … HLK … HL0) -L /2 width=2 by ylt_fwd_le/ #X #HK0 #H
+ elim (drop_inv_skip1 … H) -H /2 width=1 by ylt_to_minus/ -Hil #K0 #V #HLK0 #HVW #H destruct