def Bool.ofFin2 : Fin 2 → Bool
  | ⟨0, _⟩   => false
  | ⟨1, _⟩   => true