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

State before:
α β : Type
a : α
b : β
⊢ myProd.first (myProd.mk a b) = a
Tactic:
rfl
State after:
no goals