(4steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc
At:
sq
stable
list
all
T:Type, P:(T
Prop), L:T List. (
x:T. SqStable(P(x)))
SqStable(
x
L.P(x))
By:
UnivCD
Generated subgoal:
1
1.
T:
Type
2.
P:
T
Prop
3.
L:
T List
4.
x:T. SqStable(P(x))
SqStable(
x
L.P(x))
About:
(4steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc