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

open import plfa.part1.Induction using (Bin)

  { to = plfa.part1.Induction.to
  ; from = plfa.part1.Induction.from
  ; from∘to = plfa.part1.Induction.from-to-id

  { to = toᴮ
  ; from = fromᴮ
  ; from∘to = from-to-id