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