val fsub_e: normal lowstar_Fsub_t
let fsub_e //: normal lowstar_Fsub_t
  = as_normal_t #lowstar_Fsub_t lowstar_Fsub
val fsub_e: normal lowstar_Fsub_t
let fsub_e =
as_normal_t #lowstar_Fsub_t lowstar_Fsub
Vale.Stdcalls.X64.Fsub.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.fst.checked
Vale.Stdcalls.X64.Fsub.fst
Vale.Stdcalls.X64.Fsub.as_normal_t Vale.Stdcalls.X64.Fsub.lowstar_Fsub_t Vale.Stdcalls.X64.Fsub.lowstar_Fsub
module Vale.Stdcalls.X64.Fsub
open FStar.Mul

#reset-options "--z3rlimit 50"
let z3rlimit_hack x = ()

(* And here's the fsub wrapper itself *)
let lowstar_Fsub : lowstar_Fsub_t  =
  assert_norm (List.length dom + List.length ([]<:list arg) <= 4);
  IX64.wrap_weak_stdcall
    code_Fsub
    dom
    (W.mk_prediction code_Fsub dom [] (fsub_lemma code_Fsub IA.win))
val fsub_e: normal lowstar_Fsub_t
Vale.Interop.Base.normal Vale.Stdcalls.X64.Fsub.lowstar_Fsub_t