== (letrec formula_rank f = case f:
x
0;
p (formula_rank(p)+1);p
q (formula_rank(p)+formula_rank(q)+1);p
q (formula_rank(p)+formula_rank(q)+1);p
q (formula_rank(p)+formula_rank(q)+1); )
is not mentioned in this or prior sections.
Try larger context:
ClassicalProps(jlc)