∀ {motive : Turing.ToPartrec.Cont → Sort u} (t : Turing.ToPartrec.Cont)
  (F_1 : (t : Turing.ToPartrec.Cont) → Turing.ToPartrec.Cont.below t → motive t),
  Turing.ToPartrec.Cont.brecOn t F_1 = F_1 t (Turing.ToPartrec.Cont.brecOn.go t F_1).2