proposition: Lemma tr_rev_correct : forall X, @tr_rev X = @rev X.
proof: Proof. Admitted. Theorem evenb_double : forall k, evenb (double k) = true. Proof. intros k. induction k as [|k' IHk']. - reflexivity. - simpl. apply IHk'. Qed.
imports: Tactics