:p arhs
intro x
intros
trivial
qed
:q