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