Nuprl - Pf zero_rank_valid_or_falsifiable 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)

a:Assignment. sL.a | s

By: Using [`T',Sequent;`eq',eqS;`P',(s. disjoint(eqF;s.H;s.C));`L',L] (FwdThru Thm* eq:{T=}, P:(TProp), L:T List. (x:T. x(eq) L & P(x)) yL.P(y) [-1])

Generated subgoal:

1 6. x:Sequent. x(eqS) L & disjoint(eqF;x.H;x.C)
a:Assignment. sL.a | s

About: