val crf : _: MiTLS.Hashing.Spec.alg -> Prims.bool
let crf (_:alg) = false
(** computational assumption: collision resistance *)
module MiTLS.Hashing.CRF
open MiTLS

open MiTLS.Mem
include MiTLS.Hashing
open FStar.Bytes

//2018.04.24 SZ: to be moved elsewhere, set to false for real extraction
/
prims.fst.checked MiTLS.Mem.fst.checked MiTLS.Hashing.fsti.checked FStar.Pervasives.fsti.checked FStar.Monotonic.DependentMap.fsti.checked FStar.Bytes.fsti.checked
MiTLS.Hashing.CRF.fsti
_: MiTLS.Hashing.Spec.alg -> Prims.bool
MiTLS.Hashing.Spec.alg Prims.bool
let crf (_: alg) =
  
false