PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
finite
decidable
subset
T:Type, B:(T
Prop). Fin(T) & (
t:T. Dec(B(t)))
Fin({t:T| B(t) })
By:
GenRepD
Generated subgoal:
1
1.
T:
Type
2.
B:
T
Prop
3.
Fin(T)
4.
t:T. Dec(B(t))
Fin({t:T| B(t) })
About:
Prop
t:T. Dec(B(t))
Fin({t:T| B(t) }) T:Type, B:(TProp). Fin(T) & (t:T. Dec(B(t))) 
Fin({t:T| B(t) })Propt:T. Dec(B(t)) Fin({t:T| B(t) })
