proposition: Lemma intersect_env_false_accept : forall l l', thinner_env l l' -> forall b l1, intersect_env false l b = Some l1 -> exists l1', intersect_env false l' b = Some l1' /\ thinner_env l1 l1'.
proof: Proof. intros l l' H b l1. destruct (intersect_case b) as [x e Hb Hi | e x Hb Hn Hi | a1 a2 Hb Hn1 Hn2 Hi]. rewrite (Hi false l); rewrite (Hi false l'); clear Hi. case_eq (Ab.add_test_constraint_right false (ab_lookup l x) (ab_eval (ab_lookup l) e)). intros v Hadd. intros H'; injection H'; intros Hupdate; clear H'. case_eq (Ab.add_test_constraint_right false (ab_lookup l' x) (ab_eval (ab_lookup l') e)). intros v' Hadd'. exists (ab_update l' x v'). split; auto. subst l1. apply thinner_update; auto. apply Ab.add_test_constraint_right_monotonic with (1:= Hadd)(2:=Hadd'). apply thinner_lookup; auto. apply thinner_eval; auto. intros Hnone. elim Ab.add_test_constraint_right_monotonic_none with (1:=Hadd)(v1':=ab_lookup l' x)(v2':= ab_eval (ab_lookup l') e). apply thinner_lookup; auto. apply thinner_eval; auto. auto. intros; discriminate. rewrite (Hi false l); rewrite (Hi false l'); clear Hi. case_eq (Ab.add_test_constraint_left false (ab_eval (ab_lookup l) e) (ab_lookup l x)). intros v Hadd. intros H'; injection H'; intros Heq; clear H'. case_eq (Ab.add_test_constraint_left false (ab_eval (ab_lookup l') e) (ab_lookup l' x)). intros v' Hadd'. exists (ab_update l' x v'); split; auto. subst l1. apply thinner_update; auto. apply Ab.add_test_constraint_left_monotonic with (1:=Hadd)(2:=Hadd'). apply thinner_eval; auto. apply thinner_lookup; auto. intros Hnone. elim Ab.add_test_constraint_left_monotonic_none with (1:=Hadd)(v1':= ab_eval (ab_lookup l') e)(v2':=ab_lookup l' x); auto. apply thinner_eval; auto. apply thinner_lookup; auto. intros; discriminate. rewrite Hi; intros Heq'; injection Heq'; intros Heq; clear Heq'. subst l1. rewrite Hi. exists l'; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom