(7steps)
PrintForm
Definitions
core
3
jlc
Sections
Support(jlc)
Doc
At:
not
not
rw
T:Type, P:(T
Prop). (
x:T. Dec(P(x)))
(
x:T.
P(x)
P(x))
By:
UnivCD
Generated subgoal:
1
1.
T:
Type
2.
P:
T
Prop
3.
x:T. Dec(P(x))
4.
x:
T
P(x)
P(x)
About:
(7steps)
PrintForm
Definitions
core
3
jlc
Sections
Support(jlc)
Doc
Prop
x:T. Dec(P(x))
P(x) 
P(x)
T:Type, P:(TProp). (x:T. Dec(P(x))) 
(x:T. P(x) P(x))
Propx:T. Dec(P(x)) P(x) P(x)
