let int_canon = fun _ -> norm [delta; zeta; iota]; int_semiring ()
let int_canon =
fun _ ->
  norm [delta; zeta; iota];
  int_semiring ()
Vale.Curve25519.FastHybrid_helpers.fsti.checked
Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Curve25519.Fast_defs.fst.checked prims.fst.checked FStar.Tactics.CanonCommSemiring.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Calc.fsti.checked
Vale.Curve25519.FastHybrid_helpers.fsti
FStar.Tactics.CanonCommSemiring.int_semiring Prims.unit FStar.Tactics.V1.Builtins.norm Prims.Cons FStar.Pervasives.norm_step FStar.Pervasives.delta FStar.Pervasives.zeta FStar.Pervasives.iota Prims.Nil
module Vale.Curve25519.FastHybrid_helpers

open Vale.Def.Words_s
open Vale.Def.Types_s
open FStar.Mul
open FStar.Tactics
open FStar.Tactics.CanonCommSemiring
open Vale.Curve25519.Fast_defs
open FStar.Calc
val int_canon : _: _ -> FStar.Tactics.Effect.Tac Prims.unit
_: _ -> FStar.Tactics.Effect.Tac Prims.unit