I think @Profquail explained everything so well. So I only have to add some pieces of information about Kei. Kei rewriting rules are used to transform (well-typed) data into other (well-typed) data basically (in that case to avoid non-confluent system Kei allows only static symbols transformations), thus it enables Kei creates others logic systems. This matters because of two points. First, proofs construed in a different proof assistant can be export to Kei. Second, I have the expressiveness to lead with others type inference rules, although without the needless of learning a new language.
~I really need a welcome doc to peoples who aren't familiarized with those kinds of topics.
