2. eqS: {Sequent=
}3. eqF: {Formula=
}4.
s
L.(
(s) = 0)5. hyp: Formula List
6. concl: Formula List
7. < hyp,concl > (
eqS) L8. z: Formula
9. z(
eqF) hyp 
z(eqF) concl
v:Var. z = 
v
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)))| 1 | 1. L: Sequent List 2. eqS: {Sequent= }3. eqF: {Formula= }4. sL.((s) = 0)5. hyp: Formula List 6. concl: Formula List 7. < hyp,concl > ( eqS) L8. z: Formula 9. z( eqF) hyp z(eqF) concl v:Var. z = v |
About:
 |  |  |  |  |  |
 |  |  |  |  |