(* Forward lemmas on lenv refinement for atomic arity assignment ************)
-lemma lsubsv_fwd_lsuba: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 → L1 ⁝⊑ L2.
-#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+lemma lsubsv_fwd_lsuba: ∀h,g,G,L1,L2. G ⊢ L1 ¡⊑[h, g] L2 → G ⊢ L1 ⁝⊑ L2.
+#h #g #G #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
#L1 #L2 #W #V #W1 #V2 #l #HV #HW #_ #_ #_ #IHL12 -W1 -V2
elim (snv_fwd_aaa … HV) -HV #A #HV
elim (snv_fwd_aaa … HW) -HW #B #HW