proposition: Lemma ALInEta : forall sub v t, LIn (v,t) sub -> (LIn v (ALDom sub)) # (LIn t (ALRange sub)).
proof: Proof. induction sub as [| ? Hind]; introv Hin; auto. allsimpl. dorn Hin; subst; auto;[]. apply IHHind in Hin. repnd. split; right; auto. Qed.
imports: list Omega