proposition: Lemma tr_rev_correct : forall X, @tr_rev X = @rev X.
proof: Proof. Admitted. Theorem evenb_double : forall k, evenb (double k) = true. MProof. intros k. elim k &> [i: ~~| \k' IHk']. - T.reflexivity. - simpl. apply IHk'. Qed.