open import plfa.part1.Induction using (Bin;from-to-id) renaming (to to toᴮ; from to fromᴮ)

open import plfa.part1.Induction using (Bin;from-to-id) renaming (to to to-bin; from to from-bin)

  { to = toᴮ
  ; from = fromᴮ

  { to = to-bin
  ; from = from-bin