{motive : (a : Tactic.ComputeAsymptotics.Basis) → Tactic.ComputeAsymptotics.BasisExtension a → Sort u} →
  {a : Tactic.ComputeAsymptotics.Basis} →
    (t : Tactic.ComputeAsymptotics.BasisExtension a) →
      motive [] Tactic.ComputeAsymptotics.BasisExtension.nil →
        ((basis_hd : ℝ → ℝ) →
            {basis_tl : Tactic.ComputeAsymptotics.Basis} →
              (ex : Tactic.ComputeAsymptotics.BasisExtension basis_tl) →
                motive (basis_hd :: basis_tl) (Tactic.ComputeAsymptotics.BasisExtension.keep basis_hd ex)) →
          ({basis : Tactic.ComputeAsymptotics.Basis} →
              (f : ℝ → ℝ) →
                (ex : Tactic.ComputeAsymptotics.BasisExtension basis) →
                  motive basis (Tactic.ComputeAsymptotics.BasisExtension.insert f ex)) →
            motive a t