(6steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
At:
decidable
list
all
1
1
1.
T:
Type
2.
P:
T
Prop
3.
L:
T List
4.
x:T. Dec(P(x))
Dec(True)
By:
ProveDecidable
Generated subgoals:
None
About:
(6steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc