intro; reflexivity.
qed.
-theorem trivial: \forall n. S (myplus n n) = (S n) + n.
- unfold myplus.
+theorem trivial: \forall n. S (myplus n n) = myplus (S n) n.
+ unfold myplus in \vdash \forall _.(? ? ? %).
intro.
+ unfold myplus.
rewrite > lem.
reflexivity.
qed.
\ No newline at end of file