theorem X: \forall x:nat. let myplus \def plus x in myplus (S O) = S x.
intros. simplify. change in \vdash (? ? (% ?) ?) with (plus x).
rewrite > plus_comm. reflexivity. qed.
theorem X: \forall x:nat. let myplus \def plus x in myplus (S O) = S x.
intros. simplify. change in \vdash (? ? (% ?) ?) with (plus x).
rewrite > plus_comm. reflexivity. qed.