Level: Lib Thy Top: 1
Hypotheses:

  1. A :

  2. P : A

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

Conclusion:

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

Applied Tactic: D 3 THENW Auto
Generated subgoals:

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