namespace http://cds.omdoc.org/urtheories❚

theory LFModulo : ?PLF =
   equality : {A:type} A ⟶ A ⟶ type ❘# 2 = 3 prec -9000❘role Eq❙
❚