Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
P:
.
n:
. (
k:{n...}. P k
(
i:
k. P i))
(
m:
. P m)
(
m:
n. P m)
Applied Tactic:
UnivCD THENW Auto THEN D 3 THEN D 4
Generated subgoals:
1
.
m:
n. P m
P:
. n:. (k:{n...}. P k 
(
i:k. P i)) 
(m:. P m) (m:n. P m)m:n. P m