639 verify Token (Part I)
Issue 639 : Internal errors, Token.v, admitted definitions.
with skeleton of a proof for transfer_n_is_valid,
trying to keep MR's small, maybe this intermediate step can be merged.
Edited by Natasha Klaus
Issue 639 : Internal errors, Token.v, admitted definitions.
with skeleton of a proof for transfer_n_is_valid,
trying to keep MR's small, maybe this intermediate step can be merged.