Level: Lib Thy Top: 1 2
Hypotheses:

  1. a :

  2. b :

Conclusion:

(a b) a = b

Applied Tactic: D 0 THENW Auto
Generated subgoals:

1. a b