val mono : f: (_: Steel.Coinduction.pred a -> Steel.Coinduction.pred a) -> Prims.logical
let mono #a (f: pred a -> pred a) =
    (forall p q. implies p q ==> implies (f p) (f q))
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))
/
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
f: (_: Steel.Coinduction.pred a -> Steel.Coinduction.pred a) -> Prims.logical
Steel.Coinduction.pred Prims.l_Forall Prims.l_imp Steel.Coinduction.implies Prims.logical
let mono #a (f: (pred a -> pred a)) =
  
(forall p q. implies p q ==> implies (f p) (f q))