Draft: Natasha comparable ty vs ty
TASK : Michelson: translate: comparable_ty vs ty
created 2 lemmas, need to prove them. Please check if lemmas correct.
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 automatically.
we must ask for mutual principles as we need them, using the Scheme command, maybe this solution is not correct? I can not move forward with it, can not apply newly-defined induction principle.