proposition: Lemma fp2_compatible : forall f e l1 b i1 i2 l2, (forall l l', snd (f l) = Some l' -> compatible l l') -> fp2 e l1 b i1 f = found i2 (Some l2) -> compatible e l1 -> compatible e l2.
proof: Proof. intros f e l1 b i1 i2 l2 Hf; unfold fp2. case_eq (fp1 e l1 b i1 f); intros a_i [l' | ] Hfp1. case_eq (fp1 e l' b i1 f); intros a_i' [l'' | ] Hfp1'. destruct (stable l' l''). intros Heq Hcel1; injection Heq; do 2 intro; subst l2. apply fp1_compatible with (3:= Hfp1); auto. intros; discriminate. intros; discriminate. intros; discriminate. Qed.
imports: syntax little denot Bool List String ZArith axiom