Michelson: translate: comparable_ty vs ty

in first lemma, not able to do induction on type ty, cos it is mutually defined and coq is not able to generate induction principle for it.

created inductive principle with Scheme command

was it good idea? how to apply it?