{motive : Aesop.ExtractScriptM.State → Sort u} →
  ((script : Aesop.Script.UScript) →
      (proofHasMVar : Bool) → motive { script := script, proofHasMVar := proofHasMVar }) →
    (t : Aesop.ExtractScriptM.State) → motive t