proposition: Theorem sillyfun_false : forall (n : nat), (sillyfun n = false) : Type.
proof: Proof. MProof. intros n. unfold sillyfun. variabilize (Nat.eqb n 3) as t3. destruct t3. simpl. reflexivity. simpl. variabilize (Nat.eqb _ _) as t5. destruct t5 &> reflexivity. Qed.
imports: Mtac2(Mtac2 CompoundTactics) Strings.String Arith