PrintForm Definitions finite sets Sections AutomataTheory Doc

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

y:. f(x) y
By: Witness true
Generated subgoal:

15. f(x)
true

About:
existsboolapplyassertbtrueuniversefunctionprop