⊗-distrib-⊕ : ∀ A B C → A ⊗ (B ⊕ C) ≣ (A ⊗ B) ⊕ (A ⊗ C)
⊗-distrib-⊕  A B _ = &R
  (⊸R (⊗L [] (⊕L [ A ]
    (⊕R₁ (⊗R init init))
    (⊕R₂ (⊗R init init))
  )))
  (⊸R (⊕L []
    (⊗L [] (⊗R init (⊕R₁ init)))
    (⊗L [] (⊗R init (⊕R₂ init)))
  ))