proposition: Lemma fp_thinner : forall f, (forall e e', snd (f e) = Some e' -> compatible e e') -> forall e b i1 i3 l', fp e b i1 f = (i3,Some l') -> thinner_env e l'.
proof: Proof. intros f Hf e b i1 i3 l'. unfold fp. case_eq (fp2 e e b i1 f); [intros i' [l'0 |] Hfp Heq | intros l'0 Hfp]; simpl. injection Heq; intros; subst l'. apply fp2_thinner with (f:=f) (3:=Hfp); auto. apply thinner_env_refl. discriminate. case_eq (fp2 e l'0 b i1 f); [intros i'1 [l'1|] Hfp' Heq | intros l'1 Hfp']; simpl. injection Heq; intros; subst l'1. apply fp2_thinner with (f:=f)(3:= Hfp'); auto. apply fp2_cont_thinner with (f:=f)(3:= Hfp); auto. apply thinner_env_refl. discriminate. intros Hfp''. apply thinner_env_trans with (widen2 e). apply thinner_widen2. case_eq (fp1 (widen2 e)(widen2 e) b i1 f); intros a_i [l | ] Hfp1. rewrite Hfp1 in Hfp''; injection Hfp''; do 2 intro; subst a_i l'. apply thinner_env_refl. rewrite Hfp1 in Hfp''; discriminate. Qed.
imports: syntax little denot Bool List String ZArith axiom