proposition: Lemma fp1_abstract_i_body_accept: forall f e l b i1 i' l' l'', fp1 e l b i1 f = (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 fp1. destruct (intersect_env true l b) as [l1 | ]. case_eq (f l1); intros a_i [l2 | ] Hf. intros Heq Hi; injection Heq; do 2 intro; subst l' i'. injection Hi; intro; subst l''; exists l2; auto. intros; discriminate. intros; discriminate. Qed.
imports: syntax little denot Bool List String ZArith axiom