{Sequent=}

{Formula=}

sL.((s) = 0)

< hyp,concl > (eqS) L

z(eqF) concl

(hyp)+(concl) = 0

v:Var. z = v

FwdThru Thm* eq:{T=}, L:T List, x:T. x(eq) L (M,N:T List. L = (M @ (x.N))) [-2]
THEN
Repeat (Analyze -1)

1	11. M: Formula List 12. N: Formula List 13. concl = (M @ (z.N)) v:Var. z = v

About: