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

import meta http://cds.omdoc.org/mmt❚

theory Dedukti =
   include ?PLF❙
   rewriteType: type ⟶ type ⟶ type❘ # 1 ---> 2❘ role Eq❙
   rewriteTerm: {a: type} a ⟶ a ⟶ type ❘ # 1 --> 2❘ role Eq❙
❚