proposition: Lemma ALKeepFirstAppLin: forall lv1 lv2 sub v u, LIn (v,u) (ALKeepFirst sub (lv1++lv2)) -> LIn (v,u) (ALKeepFirst sub lv1) [+] LIn (v,u) (ALKeepFirst sub lv2).
proof: Proof. introv Hin. apply ALKeepFirstLin in Hin. repnd. apply in_app_iff in Hin. dorn Hin;[left|right]; apply ALKeepFirstLin;sp. Qed.
imports: list Omega