proposition: Lemma nax_ax_sem : forall m P i Q, nax m P i Q -> ax_sem m P i Q.
proof: Proof. induction 1. apply ax5 with Q Q; unfold valid in *; simpl in *; eauto. apply ax5 with (a_subst P' x e) P'; simpl in *; eauto. apply ax5 with P' R'; simpl in *; eauto. apply ax5 with P' (a_conj (a_not (a_b b)) P'); simpl in *; eauto. Qed.
imports: syntax little denot Bool List String ZArith