The Coq mailing list

[Victor Porton <porton AT narod.ru>]

[[[
Require Import sset2.

Class Base {set: Set} := {
}.

Class Relation {set: Set} := {
  relation_is_base :> @Base set;
  mygraph: Set; (*mygraph: set->set->Prop*)
  is_rel: is_graph mygraph;
  is_inside: sub mygraph (product set set)
}.

Definition is_inside2 `{Relation} := sub (domain mygraph) set & sub (range 
mygraph) set.

Lemma TwoInside: is_inside <-> is_inside2.
(*Intended to be proved with corr_propcc*)
]]]

The lemma TwoInside does not compile. I understand the reason it does not 
compile. But what is the correct way to rewrite it so that it will work as it 
is intended? That is I want to state that is_inside and is_inside2 are 
equivalent, provided they are quantified in the right way.

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