(datatype KAT
    (par KAT KAT)
)
(function AConst () KAT)
(let A (AConst))

(rewrite (par p p) p)
(rule ((= r (par q r)) (= q (par q r))) ((union r q)))

; tests
(let q (par A A))
(run 10)