Origin
Sections
ClassicalProps(jlc)
Doc
sequent_equality
Nuprl Section: sequent_equality
Selected Objects
THM
discrete__Sequent
Discrete{Sequent}