Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

A:. P:A . (x:A. P x (P x)) ((x:A. (P x)) (x:A. (P x))) (x:A. P x) (x:A. P x)

Applied Tactic: UnivCD THENW Auto
Generated subgoals:

1. (x:A. P x) (x:A. P x)