The Coq mailing list

[Victor Porton <porton AT narod.ru>]

[[[[
Variable s: Set.
Variable mygraph: Set.

Variable sub: Set->Set->Prop.
Variable product: Set->Set->Set.
Variable is_graph: Set->Prop.
Variable domain: Set->Set.
Variable range: Set->Set.

Axiom corr_propcc: forall s t g,
  sub g (product s t) = (is_graph g /\ sub (domain g) s /\ sub (range g) t).

Lemma TwoInside: sub mygraph (product s s) = (is_graph mygraph /\ sub (domain 
mygraph) s /\ sub (range mygraph) s).
(*
Proof.
  specialize corr_propcc.
  eauto.
Qed.
*)
proof.
  have thesis using specialize corr_propcc.
end proof. Qed.
]]]]

It does not work. When I uncomment the Proof...Qed and comment declarative 
proof, it works.

It does not work with declarative proofs. Please help me to rewrite it in 
declarative proof style.

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