val inner_gfp_equiv (#a: _) (f: (pred a -> pred a)) (x: a) (p: pred a) (m: _)
    : Lemma (interp (inner_gfp f x p) m <==> interp (p x) m /\ implies p (f p))
val inner_gfp_equiv (#a: _) (f: (pred a -> pred a)) (x: a) (p: pred a) (m: _)
    : Lemma (interp (inner_gfp f x p) m <==> interp (p x) m /\ implies p (f p))
let inner_gfp_equiv
#a (f: pred a -> pred a) (x: a) (p: pred a) m
: Lemma (
    interp (inner_gfp f x p) m 
    <==> interp (p x) m /\ implies p (f p)
)
= h_and_equiv (p x) (pure (implies p (f p))) m;
  pure_interp (implies p (f p)) m
module Steel.Coinduction

open Steel.Memory

#push-options "--print_universes"

unfold
let inner_gfp #a (f: pred a -> pred a) (x: a) (p: pred a)
= h_and (p x) (pure (implies p (f p)))

let h_and_equiv (p q: slprop) (m:mem)
  : Lemma ((interp p m /\ interp q m) <==> interp (h_and p q) m)
= elim_h_and p q m; intro_h_and p q m
/
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 ->
    m: Steel.Memory.mem
  -> FStar.Pervasives.Lemma
    (ensures
      Steel.Memory.interp (Steel.Coinduction.inner_gfp f x p) m <==>
      Steel.Memory.interp (p x) m /\ Steel.Coinduction.implies p (f p))
Steel.Coinduction.pred Steel.Memory.mem Steel.Memory.pure_interp Steel.Coinduction.implies Prims.unit Steel.Coinduction.h_and_equiv Steel.Memory.pure Prims.l_True Prims.squash Prims.l_iff Steel.Memory.interp Steel.Coinduction.inner_gfp Prims.l_and Prims.Nil FStar.Pervasives.pattern
let inner_gfp_equiv #a (f: (pred a -> pred a)) (x: a) (p: pred a) m
    : Lemma (interp (inner_gfp f x p) m <==> interp (p x) m /\ implies p (f p)) =
  
h_and_equiv (p x) (pure (implies p (f p))) m;
pure_interp (implies p (f p)) m