Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
P:T
.
L:T List. (
x:T. SqStable(P[x]))
SqStable(
x
L.P[x])
Applied Tactic:
UnivCD THENA Auto
Generated subgoals:
1
. SqStable(
x
L.P[x])
T:
. P:T 
. L:T List. (x:T. SqStable(P[x])) 
SqStable(x
L.P[x])xL.P[x])