--

check and.intro
check or.elim
check eq
check eq.rec
