def π : List (Fin 3) → List (Fin 2)

Equations

• π [] = []
• π (hd :: tl) = if h : hd < 2 then ⟨↑hd, h⟩ :: π tl else π tl