proposition: Lemma fp1_none_start : forall e e' b i i2, fp1 e e' b i (abstract_i i) = (i2, None) -> exists e2, intersect_env true e' b = Some e2 /\ abstract_i i e2 = (i2,None).
proof: Proof. intros e e' b i i2; unfold fp1. case_eq (intersect_env true e' b); [intros e2 Heq | intros; discriminate]. exists e2; destruct (abstract_i i e2) as [i' [l' | ]]; try(intros; discriminate); auto. Qed.
imports: syntax little denot Bool List String ZArith axiom