S:Sequent. |= S 
(
a:Assignment. a |
S)
propositional_decidability
(Formula List)
Thm* S:Sequent. |= S (a:Assignment. a | S)
propositional_decidability
Thm* S:Sequent. |= S (a:Assignment. a | S) prop_decide
Thm* L:Sequent List.
s
L.(
(s) = 0) 
sL.|= s (a:Assignment. sL.a | s)
zero_rank_valid_or_falsifiable
Thm* 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
)))
zero_rank_all_vars
In prior sections: sequent sequent equality sequent rank sequent satisfaction sequent falsification sequent sat lemmas full sequent assignment sequent valid normalization