There is also a Dedukti[1][2] project that can load the logic from many different systems, including Coq[3]. [1] https://deducteam.github.io/ https://deducteam

There is also a Dedukti[1][2] project that can load the logic from many different systems, including Coq[3]. [1] https://deducteam.github.io/ https://deducteam.github.io/ [2] https://github.com/Deducteam/ https://github.com/Deducteam/ [3] https://github.com/Deducteam/CoqInE https://github.com/Deducteam/CoqInE