最近Coqが流行してるので、ボクも流れに乗ってみました。今回、ボクが証明したかったのは、2回reverseすると元に戻るという性質です。 Theorem RevReflect : forall {A : Type} {xs : list A}, reverse (reverse xs) = xs. そののために、appendを定義したり…