🚀 go-pugleaf

	Say I have defined a schema S, which contains both variables
and predicates. 

	-- S -----------------
	|
	| variables
	|
	|-------
	|
	| predicates
	|
	|_____________________

	In another schema T say, I have a set X of type \power S. 

	-- T -----------------
	|
	| X: P S
	|
	|-------
	|
	| predicates
	|
	|_____________________

There is also a property I wish any S to hold. Let this property
be P. So I have a schema P which includes S and defines the property

	-- P -----------------
	|
	| S
	| variables
	|
	|-------
	|
	| predicates
	|
	|_____________________
	

	Now how do I say that each x in X in the schema T has property P?
Intuition tells me that it should be something like:

	-- T -----------------
	|
	| X: P S
	|
	|-------
	|
	| predicates
	|
	| forall x in X @ P
	|
	|_____________________


	But what is the link with x and the schema P?

All suggestions/help gratefully received.

-- 
Bill Ferreira (bill@uk.ac.warwick.dcs)
Dept. of Computer Science,
University of Warwick,
Coventry CV4 7AL, ENGLAND.