Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

P:. P P = ff


Applied Tactic: GenUnivCD THENA Auto
Generated subgoals:

1. P = ff

2. P