PrintForm Definitions decidability Sections ClassicalProps(jlc) Doc

At: zero rank valid or falsifiable 1 1 2 1 1 1 1 1
1. L: Sequent List
2. eqS: {Sequent=}
3. eqF: {Formula=}
4. sL.((s) = 0)
5. sL.(disjoint(eqF;s.H;s.C))
6. z: Sequent
7. z(eqS) L
8. disjoint(eqF;z.H;z.C)

|= z
By:
FwdThru Thm* eq:{T=}, L,M:T List. disjoint(eq;L;M) (x:T. x(eq) L & x(eq) M) [-1]
THEN
Repeat (Analyze -1)
Generated subgoal:

19. x: Formula
10. x(eqF) z.H
11. x(eqF) z.C
|= z

About:
listequalintapplynatural_numberassert