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