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?
Edited by Guillaume Claret