fact: Fixpoint ALRangeRel (R : Value -> Value-> [univ]) (subl subr : AssocList) : [univ] := match (subl, subr) with | ([],[]) => True | ((vl,tl) :: sl , (vr,tr) :: sr) => (vl=vr # R tl tr # ALRangeRel R sl sr) | ( _ , _) => False end.
imports: list Omega