val h_and_equiv (p q: slprop) (m: mem)
    : Lemma ((interp p m /\ interp q m) <==> interp (h_and p q) m)
val h_and_equiv (p q: slprop) (m: mem)
    : Lemma ((interp p m /\ interp q m) <==> interp (h_and p q) m)
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
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)))
/
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
p: Steel.Memory.slprop -> q: Steel.Memory.slprop -> m: Steel.Memory.mem
  -> FStar.Pervasives.Lemma
    (ensures
      Steel.Memory.interp p m /\ Steel.Memory.interp q m <==>
      Steel.Memory.interp (Steel.Memory.h_and p q) m)
Steel.Memory.slprop Steel.Memory.mem Steel.Memory.intro_h_and Prims.unit Steel.Memory.elim_h_and Prims.l_True Prims.squash Prims.l_iff Prims.l_and Steel.Memory.interp Steel.Memory.h_and Prims.Nil FStar.Pervasives.pattern
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