Level: Lib Thy Top: 1
Hypotheses:

  1. a :

  2. b :

Conclusion:

(a b) a = b

Applied Tactic: D 0
Generated subgoals:

1. (a b) a = b

2. (a b) a = b