val inner_gfp : f: (_: Steel.Coinduction.pred a -> Steel.Coinduction.pred a) -> x: a -> p: Steel.Coinduction.pred a
  -> Steel.Memory.slprop
let inner_gfp #a (f: pred a -> pred a) (x: a) (p: pred a)
= h_and (p x) (pure (implies p (f p)))
module Steel.Coinduction

open Steel.Memory

#push-options "--print_universes"
/
Steel.Memory.fsti.checked prims.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Calc.fsti.checked
Steel.Coinduction.fst
f: (_: Steel.Coinduction.pred a -> Steel.Coinduction.pred a) -> x: a -> p: Steel.Coinduction.pred a
  -> Steel.Memory.slprop
Steel.Coinduction.pred Steel.Memory.h_and Steel.Memory.pure Steel.Coinduction.implies Steel.Memory.slprop
let inner_gfp #a (f: (pred a -> pred a)) (x: a) (p: pred a) =
  
h_and (p x) (pure (implies p (f p)))