namespace http://cds.omdoc.org/urtheories❚ theory LFModulo : ?PLF = equality : {A:type} A ⟶ A ⟶ type ❘# 2 = 3 prec -9000❘role Eq❙ ❚