{motive : Aesop.GoalOrigin → Sort u} →
  (t : Aesop.GoalOrigin) →
    ((«from» rep : Aesop.GoalId) → motive (Aesop.GoalOrigin.copied «from» rep)) →
      (Nat.hasNotBit 2 t.ctorIdx → motive t) → motive t