agda_bug

test.agda

module test where

module QBree (A : Set) where

  data Bree : Set where
    _∪_ : Bree → Bree → Bree

  data S : Bree → Bree → Set where
    assoc   : (x y z : Bree) → S (x ∪ (y ∪ z)) ((x ∪ y) ∪ z)

module _ W Q where

  module WMB = QBree W
  module QMB = QBree Q

  l12 : (a b : WMB.Bree) → WMB.S a b → Set
  l12 a b r = {!!}