"Quot_1" theory
quotient_qinc
type_inj_wf_for_quot
quot_elim
all_quot_elim
dec_iff_ex_bvfun
decidable__quotient_equal