proposition: Lemma disjointlforall : forall {G : CFGV} {vc : VarSym G} (lswap : list (Swapping vc)), disjoint (flat_map (@ALDom _ _) lswap) (flat_map (@ALRange _ _) lswap) -> lForall (fun x => disjoint (ALDom x) (ALRange x)) lswap.
proof: Proof. induction lswap; cpx; introv Hdis. allsimpl. repeat (disjoint_reasoning); cpx. Qed.
imports: SubstAux AlphaEqProps