L:Sequent List, eqS:{Sequent=
}, eqF:{Formula=}.
s
L.(
(s) = 0) 
(hyp,concl:Formula List.
< hyp,concl > (eqS) L
(z:Formula. z(eqF) hyp 
z(eqF) concl (
v:Var. z = 
v
)))
zero_rank_all_vars
eq) L
== (letrec is_member x eq L = (Case of L
nil 
false
h.t if eq(x,h) true else is_member(x,eq,t) fi) )
(x
,eq
,L)
Thm* L:Sequent List, eqS:{Sequent=}, eqF:{Formula=}.
sL.((s) = 0)
(hyp,concl:Formula List.
< hyp,concl > (eqS) L
(z:Formula. z(eqF) hyp z(eqF) concl (v:Var. z = v)))
zero_rank_all_vars
In prior sections: list 3 jlc