proposition: Lemma intersect_env_true_none : forall l b, intersect_env true l b = None -> forall g, i_a Ab.m g (to_a l) -> ~bf' g b.
proof: Proof. intros l b; destruct (intersect_case b) as [x e Hb Hi | e x Hb _ Hi | e1 e2 Hb H1 H2 Hi]. rewrite Hi. case_eq (Ab.add_test_constraint_right true (ab_lookup l x) (ab_eval (ab_lookup l) e)). intros v Hadd Habs; discriminate Habs. intros Hadd _ g Hl. rewrite Hb. simpl; apply Ab.add_test_constraint_right_true_none with (1:=Hadd). to_p_to_i_a. apply ab_lookup_i_a; auto. to_p_to_i_a. apply ab_eval_i_a; auto. rewrite Hi. case_eq (Ab.add_test_constraint_left true (ab_eval (ab_lookup l) e) (ab_lookup l x)). intros v Hadd Habs; discriminate Habs. intros Hadd _ g Hl. rewrite Hb. simpl; apply Ab.add_test_constraint_left_true_none with (1:=Hadd). to_p_to_i_a. apply ab_eval_i_a; auto. to_p_to_i_a. apply ab_lookup_i_a; auto. rewrite Hi; intros; discriminate. Qed.
imports: syntax little denot Bool List String ZArith axiom