proposition: Theorem vcg_sound : forall ps i A g r1 r2, valid_l ps (vcg i A) -> exec r1 (un_annot i) r2 -> i_a ps (r1@g) (pc i A) -> i_a ps (r2@g) A.
proof: Proof. intros; eapply ax_sem_sound; eauto. apply vcg_ax; auto. Qed.
imports: syntax little denot Bool List String ZArith