Loading module Cryptol
Loading module Cryptol
Loading module check25
[warning] at check25.cry:6:9--6:11
    This binding for tz shadows the existing binding from
    (at check25.cry:3:1--3:3, check25::tz)
[warning] at check25.cry:1:1--8:19:
  Defaulting 1st type parameter
             of expression check25::tx
             at check25.cry:8:11--8:13
  to 4
True