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

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