Nuprl Theory normalization
(only non hidden objects are presented)
THM
normalization_lemma
G:Sequent
L:Sequent List
s
L.(
s = 0)
(
s
L.|= s
|= G )
(
a:Assignment.
s
L.a |
s
a |
G)
the other theories