A simple proof by elimination
Prove the following theorem, using only the following tactics :
intros
,
assumption
,
elim
,
simpl
, and
reflexivity
.
Theorem plus_n_O : forall n, n+0 =n.
Solution
Look at
this file