The Coq mailing list

[Victor Porton <porton AT narod.ru>]

The following is an example of a proof which uses GAIA ( 
http://www-sop.inria.fr/apics/gaia/tralics/bset1.xml ;).

Coq says

Warning: Insufficient justification.

What I miss to make the justification sufficient? I am a beginner in writing 
Coq proofs but want to learn.

[[[[
Require Import sset2.

Variable s: Set.
Variable mygraph: Set.

Lemma TwoInside: sub mygraph (product s s) = is_graph mygraph & sub (domain 
mygraph) s & sub (range mygraph) s.
proof.
  have thesis by corr_propcc.
end proof. Qed.
]]]]

-- 
Victor Porton - http://portonvictor.org