proposition: Lemma fp_none_start : forall e b i i2, fp e b i (abstract_i i) = (i2, None) -> exists e', exists e2, abstract_i i e2 = (i2,None) /\ thinner_env e e' /\ intersect_env true e' b = Some e2.
proof: Proof. intros e b i i2; unfold fp. case_eq (fp2 e e b i (abstract_i i)); [intros i' [l' | ] Hfp2 Heq| intros e' Hfp2]; try(intros; discriminate). injection Heq; intro; subst i'. elim fp2_none_start_found with (1:=Hfp2). intros e' [e2 [Hai [Hth Hinter]]]. exists e'; exists e2; auto. apply thinner_env_refl. case_eq (fp2 e e' b i (abstract_i i)); [intros i' [l'' | ] Hfp2_2 Heq | intros l'' Hfp2_2]; try(intros; discriminate). injection Heq; intro; subst i'. elim fp2_none_start_found with (1:=Hfp2_2). intros l' [e2 [Hai [Hth Hinter]]]. exists l'; exists e2; split; auto. apply fp2_cont_thinner with (f:=abstract_i i)(3:= Hfp2); auto. apply abstract_i_compatible. apply thinner_env_refl. case_eq (fp1 (widen2 e) (widen2 e) b i (abstract_i i)); intros i' [l3 |] Hfp1 Heq; try discriminate. injection Heq; intro; subst i'. elim fp1_none_start with (1:= Hfp1). intros e2 [Hinter Hai]; exists (widen2 e); exists e2; split; auto. split; auto. apply thinner_widen2. Qed.
imports: syntax little denot Bool List String ZArith axiom