{u : Lean.Level} →
  {α : Q(Type u)} →
    {mα : Q(Mul «$α»)} →
      {e v : Q(«$α»)} →
        {P : Sort u} →
          {cancelled : Q(«$α»)} →
            {pf : Q(«$v» * «$e» = «$cancelled»)} →
              {cancelled' : Q(«$α»)} →
                {pf' : Q(«$v» * «$e» = «$cancelled'»)} →
                  { cancelled := cancelled, pf := pf } = { cancelled := cancelled', pf := pf' } →
                    (cancelled = cancelled' → pf = pf' → P) → P