(* Nicer error messages. Instead of being asked to prove `False`,
    you are asked to prove `error (hopefully useful message)`.
*)

Module Type error_spec.
    Parameter error : forall {T : Type}, T -> Prop.
    Axiom error_elim : forall {msgType} {msg : msgType} {T}, error msg -> T.
End error_spec.

Module Export error : error_spec.
    Definition error {T} (msg : T) := False.
    Definition error_elim {msgType} (msg : msgType) T : error msg -> T := False_rect T.
End error.