Thm* Discrete{Sequent} discrete__Sequent
In prior sections: discrete jlc list 3 jlc var jlc formula equality
x,y:T. Dec(x = y)