PrintForm Definitions finite sets Sections AutomataTheory Doc

At: set function 1 1
1. S: Type
2. T: Type
3. R: STProp
4. s:S. Dec(t:T. R(s,t))

x:{s:S| t:T. R(s,t) }. y:T. R(x,y)
By:
Analyze 0
THEN
Analyze 5
THEN
Unhide
Generated subgoals:

None

About:
allsetexistsapplyuniversefunctionprop