A verifier for the Metamath Zero proof language.
strict provable sort EE;
term termE1 (p: EE): EE; 
term termE2 (p: EE): EE;