proposition: Theorem sillyfun_false : forall (n : nat), (sillyfun n = false) : Type.
proof: Proof. MProof. intros n. unfold sillyfun. destruct (beq_nat n 3). - simpl. reflexivity. - simpl. destruct (beq_nat _ _). + reflexivity. + reflexivity. Qed.