PrintForm Definitions finite sets Sections AutomataTheory Doc

At: decid is comp 1 1 1
1. T: Type
2. f: TProp
3. t:T. Dec(f(t))
4. x: T

y:. f(x) y
By: Witness3 x
Generated subgoal:

13. x: T
4. Dec(f(x))
y:. f(x) y

About:
existsboolapplyassertuniversefunctionpropall