Theorem: LoVe.BackwardProofs.η_example (LoVe/Lectures/LoVe03_BackwardProofs_Demo.lean)

State before:
α β : Type
f : α → β
⊢ (fun x => f x) = f
Tactic:
rfl
State after:
no goals