proposition: Lemma fp2_cont_thinner : forall f, (forall e e', snd (f e) = Some e' -> compatible e e') -> forall e e' b i1 e'', thinner_env e e' -> fp2 e e' b i1 f = cont e'' -> thinner_env e e''.
proof: Proof. intros f Hf e e' b i1 e'' Hte'. unfold fp2. case_eq (fp1 e e' b i1 f); intros i'0 [l' | ] Hfp. case_eq (fp1 e l' b i1 f); intros i'1 [l'' | ] Hfp'. case (stable l' l''). simpl. intros; discriminate. intros Heq; injection Heq; intros; subst e''. apply thinner_env_trans with l'. apply fp1_thinner with (3:= Hfp); auto. apply thinner_widen. intros; discriminate. intros; discriminate. Qed.
imports: syntax little denot Bool List String ZArith axiom