Level: Lib Thy Top: 1 1
Hypotheses:

  1. a :

  2. b :

Conclusion:

(a b) a = b

Applied Tactic: D 0 THENW Auto THEN InstLemma `iff_imp_equal_bool` [a;b] THEN Auto
Generated subgoals:

None