proposition: Theorem vcg_ax : forall m i A, valid_l m (vcg i A) -> ax_sem m (pc i A) (un_annot i) A.
proof: Proof. unfold valid_l; intros m i; induction i; intros A Hc; simpl. simpl in *; apply ax5 with (pc i A) A. intros g; elim (Hc g); auto. apply IHi; intros g; elim (Hc g); auto. red; simpl; auto. apply ax1. apply ax2. simpl in *; apply ax3 with (pc i2 A). apply IHi1; intros g; apply i_lc_app_r with (1:= Hc g). apply IHi2; intros g; apply i_lc_app_l with (1:= Hc g). simpl in *; apply ax5 with a (a_conj (a_not (a_b b)) a). red; simpl; auto. apply ax4. apply ax5 with (pc i a) a. intros g; simpl; generalize (Hc g); intuition. apply IHi; intros g; simpl; generalize (Hc g); intuition. red; simpl; auto. intros g; simpl; generalize (Hc g); intuition. Qed.
imports: syntax little denot Bool List String ZArith