proposition: Fact silly_fact_2_FAILED : forall m, bar m + 1 = bar (m + 1) + 1.
proof: Proof. MProof. intros m. simpl. Abort. Fact silly_fact_2 : forall m, bar m + 1 = bar (m + 1) + 1. MProof. intros m. destruct m. - simpl. reflexivity. - simpl. reflexivity. Qed.