Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

P:. P P = tt

Applied Tactic: GenUnivCD THENA Auto
Generated subgoals:

1. P = tt

2. P