proposition: Lemma compatible_intersect_env : forall neg l b l', intersect_env neg l b = Some l' -> compatible l l'.
proof: Proof. intros neg l b; destruct (intersect_case b) as [x e Hb Hi | e x Hb _ Hi | e1 e2 Hb H1 H2 Hi]. intros l'; rewrite Hi. destruct (Ab.add_test_constraint_right neg (ab_lookup l x) (ab_eval (ab_lookup l) e)) as [v | ]. intros Heq; injection Heq; intro; subst l'; apply compatible_update. intros; discriminate. intros l'; rewrite Hi. destruct (Ab.add_test_constraint_left neg (ab_eval (ab_lookup l) e) (ab_lookup l x)) as [ v | ]. intros Heq; injection Heq; intro; subst l'; apply compatible_update. intros; discriminate. intros l'; rewrite Hi; intros Heq; injection Heq; intros; subst. apply compatible_refl. Qed.
imports: syntax little denot Bool List String ZArith axiom