val coerce (#b #a: Type) (x: a{a == b}) : b
let coerce (#b #a:Type) (x:a{a == b}) : b = x
val coerce (#b #a: Type) (x: a{a == b}) : b
let coerce (#b #a: Type) (x: a{a == b}) : b =
x
Spec.Agile.Hash.fst.checked
Spec.SHA3.fst.checked Spec.SHA2.fsti.checked Spec.SHA1.fsti.checked Spec.MD5.fsti.checked Spec.Hash.MD.fst.checked Spec.Hash.Definitions.fst.checked Spec.Blake2.fst.checked prims.fst.checked Lib.UpdateMulti.fst.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Spec.Agile.Hash.fst
Prims.eq2
module Spec.Agile.Hash

module S = FStar.Seq

open Spec.Hash.Definitions
open Spec.Hash.MD
open FStar.Mul
open Lib.IntTypes
val coerce (#b #a: Type) (x: a{a == b}) : b
x: a{a == b} -> b