The Coq mailing list

["Terrell, Jeffrey" <jeffrey.terrell AT kcl.ac.uk>]

Hi,

How could Spec be made to return the proposition

forall x : X, D x /\ L x?

Clearly, the way I've defined it is nonsense. However, I don't know how to 
exploit the fact that parameters d and l are both dependent on parameter X.

Inductive Data : Set -> Type :=
   Build_Data : forall X : Set, (X -> Prop) -> Data X.

Inductive Link : Set -> Type :=
   Build_Link : forall X : Set, (X -> Prop) -> Link X.

Definition Spec (X : Set) (d : Data X) (l : Link X) : Prop :=
   match d with Build_Data X D => 
      match l with Build_Link X L =>
         forall x : X, D x /\ L x
      end
   end.

Many thanks.

Regards,
Jeff.
---
Jeffrey Terrell
Department of Informatics
King's College, London