module braun where open import Data.Sum using (_⊎_; inj₁; inj₂; map₂; [_,_]) open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong; cong₂) open import Data.Empty using (⊥; ⊥-elim) open import Relation.Nullary using (¬_) open import Data.Nat.Binary using (ℕᵇ; zero; 1ᵇ; 1+[2_]; 2[1+_]; suc; pred; _+_) open import Data.Nat.Binary using (_<_; 0