val cast_up
  (#t1: inttype { unsigned t1 })
  (t2: inttype { unsigned t2 /\ bits t1 <= bits t2 })
  (#sec: secrecy_level)
  (x: uint_t t1 sec)
: Tot (y: uint_t t2 SEC { v y == v x })
val cast_up
  (#t1: inttype { unsigned t1 })
  (t2: inttype { unsigned t2 /\ bits t1 <= bits t2 })
  (#sec: secrecy_level)
  (x: uint_t t1 sec)
: Tot (y: uint_t t2 SEC { v y == v x })
let cast_up
  #t1 t2 #sec x
= cast t2 SEC x
module QUIC.Secret.Int
module Aux = QUIC.Secret.Int.Aux

let usub
  #t #sec x y
= x `sub` y
/
QUIC.Secret.Int.Aux.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked
QUIC.Secret.Int.fst

    t2:
      Lib.IntTypes.inttype{Lib.IntTypes.unsigned t2 /\ Lib.IntTypes.bits t1 <= Lib.IntTypes.bits t2} ->
    x: Lib.IntTypes.uint_t t1 sec
  -> y:
    Lib.IntTypes.uint_t t2 Lib.IntTypes.SEC {QUIC.Secret.Int.Base.v y == QUIC.Secret.Int.Base.v x}
Lib.IntTypes.inttype Prims.b2t Lib.IntTypes.unsigned Prims.l_and Prims.op_LessThanOrEqual Lib.IntTypes.bits Lib.IntTypes.secrecy_level Lib.IntTypes.uint_t Lib.IntTypes.cast Lib.IntTypes.SEC Prims.eq2 Prims.int Prims.l_or Lib.IntTypes.range QUIC.Secret.Int.Base.v
let cast_up #t1 t2 #sec x =
  
cast t2 SEC x