Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Formula 
Applied Tactic: RWH (AllC [UnfoldC `formula_rank`;
letrec_unrollC;
FoldC `formula_rank`]) 0
Generated subgoals:1. (
f.case f:
x
0;
p ( p + 1);
p
q (( p + q) + 1);
p
q (( p + q) + 1);
p
q (( p + q) + 1);) Formula