{A : Type u} →
  {B : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] →
          {motive : Algebra.Smooth.DescentAux✝ A B → Sort u_1} →
            (t : Algebra.Smooth.DescentAux✝¹ A B) →
              ((vars rels : Type) →
                  (P : Algebra.Presentation A B vars rels) →
                    (σ : B →ₐ[A] MvPolynomial vars A ⧸ P.ker ^ 2) →
                      (h : vars → MvPolynomial vars A) →
                        (p : rels → MvPolynomial rels (MvPolynomial vars A)) →
                          (hphom : ∀ (j : rels), (p j).IsHomogeneous 2) →
                            (hp :
                                ∀ (j : rels),
                                  (MvPolynomial.eval P.relation) (p j) = (MvPolynomial.aeval h) (P.relation j)) →
                              (q : vars → MvPolynomial rels P.Ring) →
                                (hqhom : ∀ (i : vars), (q i).IsHomogeneous 1) →
                                  (hq : ∀ (i : vars), (MvPolynomial.eval P.relation) (q i) = h i - MvPolynomial.X i) →
                                    motive
                                      { vars := vars, rels := rels, P := P, σ := σ, h := h, p := p, hphom := hphom,
                                        hp := hp, q := q, hqhom := hqhom, hq := hq }) →
                motive t