proposition: Lemma fp1_none_precondition : forall e e' b i i' a e'', fp1 e e' b i (abstract_i i) = (i', None) -> intersect_env true e' b = Some e'' -> pc i' a = to_a e''.
proof: Proof. intros e e' b i i' a e''; unfold fp1. destruct (intersect_env true e' b). case_eq (abstract_i i a0); intros i1 [l | ]; try (intros; discriminate). intros Hai Heq; injection Heq; intro; subst i1. intros Heq'; injection Heq'; intro; subst a0. assert (Hai' : fst (abstract_i i e'') = i') by (rewrite Hai; auto). rewrite <- Hai'. apply abstract_i_pre_condition. intros; discriminate. Qed.
imports: syntax little denot Bool List String ZArith axiom