{P : Sort u} →
  {x : Lean.IR.VarId} →
    {ty : Lean.IR.IRType} →
      {e : Lean.IR.Expr} →
        {b : Lean.IR.FnBody} →
          {x' : Lean.IR.VarId} →
            {ty' : Lean.IR.IRType} →
              {e' : Lean.IR.Expr} →
                {b' : Lean.IR.FnBody} →
                  Lean.IR.FnBody.vdecl x ty e b = Lean.IR.FnBody.vdecl x' ty' e' b' →
                    (x = x' → ty = ty' → e = e' → b = b' → P) → P