P:(T
Prop), L:T List. (x:T. SqStable(P(x))) 
SqStable(x
L.P(x))eq:(TT
), x:T, L:T List. SqStable(x(eq) L)
P P
is mentioned by
| Thm* P:(TProp), L:T List. (x:T. SqStable(P(x))) SqStable(xL.P(x)) | [sq_stable__list_all] |
| Thm* eq:(TT), x:T, L:T List. SqStable(x(eq) L) | [sq_stable__is_member] |
In prior sections: core core 3 jlc fun 1