a Minimal Extensible Proof Kernel, for trusted proofs in the style of Metamath and Ghilbert