Specify Script_typed_ir.ty
In https://formal-land.gitlab.io/coq-tezos-of-ocaml/docs/proto_alpha/proofs/script_typed_ir add a predicate Valid.ty
of the form:
Module Valid.
Module ty.
Inductive t : Ty.t -> Script_typed_ir.ty -> Prop :=
| Unit_t : t Ty.Unit Script_typed_ir.Unit_t
| ...
taking inspiration from what we already had on the simulations.
Edited by Guillaume Claret