PrintForm Definitions finite sets Sections AutomataTheory Doc

At: set function

S,T:Type, R:(STProp). (s:S. Dec(t:T. R(s,t))) (f:({s:S| t:T. R(s,t) }T). s:{s:S| t:T. R(s,t) }. R(s,f(s)))
By: UnivCD
Generated subgoal:

11. S: Type
2. T: Type
3. R: STProp
4. s:S. Dec(t:T. R(s,t))
f:({s:S| t:T. R(s,t) }T). s:{s:S| t:T. R(s,t) }. R(s,f(s))

About:
alluniversefunctionpropimpliesexistsapplyset