proposition: Lemma fp2_thinner : forall f:ab_env-> (a_instr* option ab_env), (forall e e', snd (f e) = Some e' -> compatible e e') -> forall e e' b i1 i' e'', thinner_env e e' -> fp2 e e' b i1 f = found i' (Some e'') -> thinner_env e e''.
proof: Proof. intros f Hf e e' b i1 i' 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 Heq; injection Heq; intros; subst e''. apply fp1_thinner with (f:=f)(3:=Hfp);auto. intros; discriminate. intros; discriminate. intros; discriminate. Qed.
imports: syntax little denot Bool List String ZArith axiom