val implies : p: Steel.Coinduction.pred a -> q: Steel.Coinduction.pred a -> Prims.logical
let implies #a (p q: pred a) = (forall x. slimp (p x) (q x))
module Steel.Coinduction
open Steel.Memory

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

type pred a = (a -> slprop)
/
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
p: Steel.Coinduction.pred a -> q: Steel.Coinduction.pred a -> Prims.logical
Steel.Coinduction.pred Prims.l_Forall Steel.Memory.slimp Prims.logical
let implies #a (p: pred a) (q: pred a) =
  
(forall x. slimp (p x) (q x))