proposition: Lemma abstract_i_pre_condition : forall i e p, pc (fst (abstract_i i e)) p = (to_a e).
proof: Proof. induction i; intros e p; simpl; auto. assert (IHi1' := IHi1 e); destruct (abstract_i i1 e) as [i'1 [e' |]]; simpl in IHi1' |- *; auto. assert (IHi2' := IHi2 e'); destruct (abstract_i i2 e') as [i'2 [e''|]]; simpl; auto. simpl; destruct (intersect_env true e b); simpl; auto. destruct (fp e b i (abstract_i i)) as [i' [l' | ]]; simpl; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom