{motive : Aesop.RuleState → Sort u} →
  (t : Aesop.RuleState) →
    ((rule : Aesop.ForwardRule) →
        (clusterStates : Array Aesop.ClusterState) →
          (patSubstSources : Lean.PHashMap Aesop.Substitution (Lean.PHashSet Aesop.PatSubstSource)) →
            motive { rule := rule, clusterStates := clusterStates, patSubstSources := patSubstSources }) →
      motive t