Level: Lib Thy Top:
Hypotheses:None
Conclusion:
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
)))
Applied Tactic: UnivCD THENA Auto
Generated subgoals:1. v:Var. z = v