The Nest
Explore
0
A verifier for the Metamath Zero proof language. 
strict provable sort DD;
term termD1 (p: DD): DD; 
term termD2 (p: DD): DD;