proposition: Lemma fp1_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 i3 l', thinner_env e e' -> fp1 e e' b i1 f = (i3, Some l') -> thinner_env e l'.
proof: Proof. intros f Hf e e' b i1 i3 l' Hte'; unfold fp1. assert (Hce' : compatible e e') by (apply thinner_compatible; auto). case_eq (intersect_env true e' b); [intros l'0 Hie | idtac]. assert (Hcl'0 : compatible e' l'0) by (apply compatible_intersect_env with true b; auto). case_eq (f l'0); intros i' [l'' | ] Hf'. assert (Hcl'' : compatible l'0 l'') by (apply Hf; rewrite Hf'; auto). intros Heq; injection Heq; intros; subst l'. apply thinner_join_env_left. apply compatible_trans with e'; auto. apply compatible_trans with l'0; auto. apply compatible_join_env_left; auto. intros; discriminate. intros Hi Heq; injection Heq; intros; subst l'; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom