A verifier for the Metamath Zero proof language.
strict provable sort FF;
term termF1 (p: FF): FF; 
term termF2 (p: FF): FF;