proposition: Lemma rangeFreeVarsKeepFirstAppL: forall sub va vb x, LIn x (rangeFreeVars (ALKeepFirst (DeqVtype vc) sub va)) -> LIn x (rangeFreeVars (ALKeepFirst (DeqVtype vc) sub (va ++ vb))).
proof: Proof. introv Hin. rw lin_flat_map in Hin. exrepnd. rw in_map_iff in Hin1. exrepnd. apply ALKeepFirstLin in Hin1. exrepnd. rw lin_flat_map. eexists; dands; eauto. rw in_map_iff; eexists; dands; eauto;[]. allsimpl; apply ALKeepFirstLin. dands; allrw in_app_iff; cpx. Qed.
imports: Term AssociationList