proposition: Lemma mark_sound : forall i g, i_lc Ab.m g (vcg (mark i) false_assert).
proof: Proof. intros i g; induction i; simpl; auto. rewrite mark_pc; apply app_i_lc; auto. rewrite mark_pc; rewrite f_p_lookup; rewrite false_top; intuition. Qed.
imports: syntax little denot Bool List String ZArith axiom