proposition: Lemma ALKeepFirstLinApp: forall sub v vs vss t, LIn (v,t) (ALKeepFirst sub (vs)) -> LIn (v,t) (ALKeepFirst sub (vs++ vss)).
proof: Proof. introv X. apply ALKeepFirstLin in X. apply ALKeepFirstLin. exrepnd; dands; auto. apply in_app_iff. cpx. Qed.
imports: list Omega