These proofs, originally developed in Matita , has been expressed in a formulation of the Calculus of Inductive Constructions in Dedukti, it has then been translated to a formulation of Simple type theory in Dedukti, and exported to Open theory , Coq , Matita , Lean , and PVS .