{α β αΓ βΓ : Type} →
  {ea : α → List αΓ} →
    {eb : β → List βΓ} →
      {f : α → β} →
        {motive : Turing.TM2Computable ea eb f → Sort u} →
          (t : Turing.TM2Computable ea eb f) →
            ((toTM2ComputableAux : Turing.TM2ComputableAux αΓ βΓ) →
                (outputsFun :
                    (a : α) →
                      Turing.TM2Outputs toTM2ComputableAux.tm (List.map toTM2ComputableAux.inputAlphabet.invFun (ea a))
                        (some (List.map toTM2ComputableAux.outputAlphabet.invFun (eb (f a))))) →
                  motive { toTM2ComputableAux := toTM2ComputableAux, outputsFun := outputsFun }) →
              motive t