PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
decid
is
comp
T:Type, f:(T
Prop). (
t:T. Dec(f(t)))
(
g:(T
).
t:T. f(t)
g(t))
By:
UnivCD
Generated subgoal:
1
1.
T:
Type
2.
f:
T
Prop
3.
t:T. Dec(f(t))
g:(T
).
t:T. f(t)
g(t)
About:
Prop
t:T. Dec(f(t))
g:(T
). t:T. f(t) 
g(t) T:Type, f:(TProp). (t:T. Dec(f(t))) 
(g:(T). t:T. f(t) g(t))Propt:T. Dec(f(t)) g:(T). t:T. f(t) g(t)
