proposition: Theorem ax_sem_sound : forall m r i r' g P Q, exec r i r' -> ax_sem m P i Q -> i_a m (r@g) P -> i_a m (r'@g) Q.
proof: Proof. intros; eapply nax_sound; eauto. apply ax_sem_nax; auto. Qed.
imports: syntax little denot Bool List String ZArith