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