(3steps)
PrintForm
Definitions
core
3
jlc
Sections
Support(jlc)
Doc
At:
decidable
spread
1
1.
T:
Type
2.
U:
Type
3.
P:
T
U
Prop
4.
x:T, y:U. Dec(P(x,y))
5.
p:
T
U
Dec(p/l,r. P(l,r))
By:
Analyze 5
THEN
Reduce 0
Generated subgoal:
1
5.
p1:
T
6.
p2:
U
Dec(P(p1,p2))
About:
(3steps)
PrintForm
Definitions
core
3
jlc
Sections
Support(jlc)
Doc
Dec(P(p1,p2))
UProp
x:T, y:U. Dec(P(x,y))
U
Dec(p/l,r. P(l,r))
Dec(P(p1,p2))
