proposition: Lemma ALRangeRelSameDom : forall R (subl subr : AssocList), ALRangeRel R subl subr -> ALDom subl = ALDom subr.
proof: Proof. induction subl as [| (kl,vl) subl Hind]; introv Hal; destruct subr as [| (kr,vr) subr]; allsimpl; repnd; dands; cpx. f_equal; cpx. Qed.
imports: list Omega