val mono_fun : a: Type -> Type
let mono_fun a = (f: (pred a -> pred a){mono f})
module Steel.Coinduction
open Steel.Memory

(** General interface for SL props defined coinductively **)

type pred a = (a -> slprop)

let implies #a (p q: pred a) = (forall x. slimp (p x) (q x))

let mono #a (f: pred a -> pred a) =
    (forall p q. implies p q ==> implies (f p) (f q))
/
Steel.Reference.fsti.checked Steel.Memory.fsti.checked Steel.FractionalPermission.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Steel.Coinduction.fsti
a: Type -> Type
Steel.Coinduction.pred Steel.Coinduction.mono
let mono_fun a =
  
(f: (pred a -> pred a){mono f})