proposition: Lemma fp2_abstract_i_body_imp_invariant : forall e e' b i1 i3 i4 l' l'' l''' f, (forall l l', snd (f l) = Some l' -> compatible l l') -> compatible e e' -> fp2 e e' b i1 f = found i3 (Some l') -> intersect_env true l' b = Some l'' -> f l'' = (i4, Some l''') -> thinner_env l''' l'.
proof: Proof. intros e e' b i1 i3 i4 l' l'' l''' f Hf Hcee'. unfold fp2. case_eq (fp1 e e' b i1 f); intros i' [l1 | ] Hfp1. case_eq (fp1 e l1 b i1 f); intros a_i [l2 | ] Hfp1'. case_eq (stable l1 l2); intros Hst. assert (Hcel1 : compatible e l1). apply fp1_compatible with (3:= Hfp1); auto. assert (Hcel2 : compatible e l2). apply fp1_compatible with (3:= Hfp1'); auto. assert (Hl1l2 : l1 = l2). apply compatible_stable_eq; auto. apply compatible_trans with e; auto. apply compatible_sym; auto. intros Heq; injection Heq; do 2 intro; subst i3 l' l1. intros Hi Hai. apply fp1_abstract_i_body_imp_invariant with (3:=Hi)(4:=Hai)(5:=Hfp1');auto. intros; discriminate. intros; discriminate. intros; discriminate. Qed.
imports: syntax little denot Bool List String ZArith axiom