1 2 3 4 5
(* -*- mode: coq; coq-prog-args: ("-quick") -*- *) Goal True. abstract exact I. Timeout 1 Defined.