1 2 3 4 5 6
(* Check Guard in proofs *) Goal nat->nat. fix f 1. intro n; apply f; assumption. Guarded.