Guarded fixpoints

Can we metaprogram away the functor/fixpoint construction everyone copy-pastes for defining partial weakest preconditions? I'm picturing something that behaves like partial_fixpoint but for guarded recursion:

def wp (s : Stuckness) (E : CoPset) (e₁ : Expr) (Φ : Val -> IProp GF) : IProp GF :=
  match toVal e₁ with
  | some v => iprop(|={E}=> Φ v)
  | none => iprop(∀ (σ₁ : State) (ns : Nat) (obs obs' : List Obs) (nt : Nat),
    stateInterp σ₁ ns (obs ++ obs') nt ={E,∅}=∗
    ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗
    ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -<obs>-> (e₂, σ₂, eₜ)⌝ -∗
      £ (ι.numLatersPerStep ns + 1) ={∅}▷=∗^[ι.numLatersPerStep ns + 1] |={∅,E}=>
      stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗
      wp E e₂ Φ ∗ [∗list] e' ∈ eₜ, wp ⊤ e' ι.forkPost)
guarded_fixpoint

Like partial_fixpoint and coinductive_fixpoint etc, I'd imagine that guarded_fixpoint first tries to solve the contractivity goal by something like aesop_contractive, but also gives an escape hatch for doing it manually

guarded_fixpoint contractive by  
    ...

Start by reading the existing partial_fixpoint and coinductive_fixpoint implementations, then inspect how aesop_contractive is used. Define the guarded_fixpoint interface, including automatic contractivity solving and the manual contractive by escape hatch. Done means the issue's guarded recursion example can use the new command.