Theorem: PFin2.toFin2_ofFin2 (Qpf/MathlibPort/Fin2.lean)

State before:
n : ℕ
i : PFin2 n
⊢ ofFin2 (toFin2 i) = i
Tactic:
induction i <;> simp [ofFin2, toFin2, *]
State after:
no goals