Require Import Tactics.
Require Import Pointer AndersenModel AndersenSound AndersenIter.
Lemma incl_intersect2 : forall s1 t1 s2 t2,
AllocSet.incl s1 s2 = true
-> AllocSet.incl t1 t2 = true
-> AllocSet.incl (AllocSet.intersect s1 t1)
(AllocSet.intersect s2 t2) = true.
Definition andersen : mustNotAlias_procedure.