The Coq mailing list

[Georgi Guninski <guninski AT guninski.com>]

how a client should check a Coq proof for cheating?

please excuse my dumbness, i am new to Coq.

i am trying to convince a client a bit counterintuitive proof is valid.

it is my understanding there must be no axioms (coqchk -o) and in coqtop 
"Print lemma_X." should print after ":" the statement of the .v source file.

should the client do other checks in the example below?

should i take any action to improve the example? (if it happens valid/invalid 
i suppose i can change it a lot...):

(* coqtop is not fiddled by me, no east european plugins. coqchk -o passed 
genuinely and showed no axioms.).

fuck_m$>coqtop
Welcome to Coq 8.2pl1 (February 2010)
Coq < Require Import fib10.
Coq < Print c1.
c1 = SOME_STUF ending in ')\n'
  : True -> forall x : Prop, True -> x

Coq < Lemma l1: True -> forall x : Prop, True -> x.
l1 < apply c1.
Proof completed.

thank you for your time.

(please reply to list with your counter-cheating ideas).