proposition: Lemma fp_abstract_i_body_accept : forall e b i1 i2 i3 l' l'', fp e b i1 (abstract_i i2) = (i3, Some l') -> intersect_env true l' b = Some l'' -> exists l''', abstract_i i2 l'' = (i3, Some l''').
proof: Proof. intros e b i1 i2 i3 l' l''. unfold fp. case_eq (fp2 e e b i1 (abstract_i i2)); [intros a_i l1 Hfp2 | intros l1 Hfp2]. intros Heq Hi; injection Heq; do 2 intro; subst l1 a_i. apply fp2_abstract_i_body_accept with (1:= Hfp2); auto. case_eq (fp2 e l1 b i1 (abstract_i i2));[intros a_i2 l2 Hfp2' | intros l2 Hfp2']. intros Heq Hi; injection Heq; do 2 intro; subst l2 a_i2. apply fp2_abstract_i_body_accept with (1:= Hfp2'); auto. case_eq (fp1 (widen2 e)(widen2 e) b i1 (abstract_i i2)). intros a_i [l3 | ] Hfp1 Heq Hi. injection Heq; do 2 intro; subst a_i l'. apply fp1_abstract_i_body_accept with (1:= Hfp1); auto. discriminate. Qed.
imports: syntax little denot Bool List String ZArith axiom