PrintForm Definitions finite sets Sections AutomataTheory Doc

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

x:T. y:. f(x) y
By: Analyze 0
Generated subgoal:

14. x: T
y:. f(x) y

About:
allexistsboolapplyassertuniversefunctionprop