proposition: Lemma intersect_env_false_i_a : forall e b g, i_a Ab.m g (to_a e) -> ~i_a Ab.m g (a_b b) -> i_a Ab.m g (to_a' (intersect_env false e b)).
proof: Proof. intros e b g; destruct (intersect_case b) as [s1 e2 Heq Hint | e1 s2 Heq Hexc Hint | e1 e2 Heq Hexc1 Hexc2 Hint]; intros He Hb; assert (Hint' := Hint false e); clear Hint. case_eq (Ab.add_test_constraint_right false (ab_lookup e s1) (ab_eval (ab_lookup e) e2)). unfold to_a'. intros v Hadd; rewrite Hadd in Hint'; rewrite Hint'; apply i_a_update; auto. i_a_to_to_p. apply Ab.add_test_constraint_right_false_sound with (1:=Hadd) (v2:=(ab_eval (ab_lookup e) e2))(x2 := af' g e2). to_p_to_i_a. apply ab_lookup_i_a; auto. to_p_to_i_a. apply ab_eval_i_a; auto. rewrite Heq in Hb; exact Hb. intros Hadd. elim Hb; rewrite Heq. apply Ab.add_test_constraint_right_false_none with (1:=Hadd) (x1 := af' g (avar s1))(x2:= af' g e2). to_p_to_i_a. apply ab_lookup_i_a; auto. to_p_to_i_a. apply ab_eval_i_a; auto. case_eq (Ab.add_test_constraint_left false (ab_eval (ab_lookup e) e1) (ab_lookup e s2)). intros v Hadd; rewrite Hadd in Hint'; rewrite Hint'; simpl. apply i_a_update; auto. i_a_to_to_p. apply Ab.add_test_constraint_left_false_sound with (1:=Hadd) (v1:=(ab_eval (ab_lookup e) e1))(x1:= af' g e1). to_p_to_i_a. apply ab_eval_i_a; auto. to_p_to_i_a. apply ab_lookup_i_a; auto. rewrite Heq in Hb; exact Hb. intros Hadd. elim Hb; rewrite Heq. simpl. apply Ab.add_test_constraint_left_false_none with (1:=Hadd) (v1:= ab_eval (ab_lookup e) e1) (v2 := ab_lookup e s2). to_p_to_i_a. apply ab_eval_i_a; auto. to_p_to_i_a. apply ab_lookup_i_a; auto. rewrite Hint'; simpl; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom