fix compiler proofs for changed location of convert_t_def
more opening of the new inferPropsTheory