Def
== (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); )
Thm*
hyp,concl:Formula List.

f
hyp.(
(f) > 0) 

f
concl.(
(f) > 0) 
( < hyp,concl > ) = 0
not_list_exists_rank_gt_0_rank_0