proposition: Lemma rangeFreeVarsKeepFirstAppImplies: forall sub va vb x, LIn x (rangeFreeVars (ALKeepFirst (DeqVtype vc) sub (va++vb))) -> (LIn x (rangeFreeVars (ALKeepFirst (DeqVtype vc) sub (va ))) [+] LIn x (rangeFreeVars (ALKeepFirst (DeqVtype vc) sub (vb )))).
proof: Proof. introv Hin. rw lin_flat_map in Hin. exrepnd. rw in_map_iff in Hin1. exrepnd. apply ALKeepFirstAppLin in Hin1. dorn Hin1;[left | right]; rw lin_flat_map; eexists; dands; eauto; rw in_map_iff; eexists; dands; eauto. Qed.
imports: Term AssociationList