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

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