(* Properties concerning stratified native validity *************************)
lemma lsubsv_snv_trans: ∀h,g,G,L2,T. ⦃G, L2⦄ ⊢ T ¡[h, g] →
- ∀L1. G ⊢ L1 ¡⫃[h, g] L2 → ⦃G, L1⦄ ⊢ T ¡[h, g].
+ ∀L1. G ⊢ L1 ⫃¡[h, g] L2 → ⦃G, L1⦄ ⊢ T ¡[h, g].
#h #g #G #L2 #T #H elim H -G -L2 -T //
[ #I #G #L2 #K2 #V #i #HLK2 #_ #IHV #L1 #HL12
elim (lsubsv_drop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1