∀ {σ : Type u_1} {syn : Type u_2} {acm : autoParam (AddCommMonoid syn) MonomialOrder.acm._autoParam}
  {lo : autoParam (LinearOrder syn) MonomialOrder.lo._autoParam}
  {iocam : autoParam (IsOrderedCancelAddMonoid syn) MonomialOrder.iocam._autoParam} {toSyn : (σ →₀ ℕ) ≃+ syn}
  {toSyn_monotone : Monotone ⇑toSyn} {wf : autoParam (WellFoundedLT syn) MonomialOrder.wf._autoParam} {syn_1 : Type u_2}
  {acm_1 : autoParam (AddCommMonoid syn_1) MonomialOrder.acm._autoParam}
  {lo_1 : autoParam (LinearOrder syn_1) MonomialOrder.lo._autoParam}
  {iocam_1 : autoParam (IsOrderedCancelAddMonoid syn_1) MonomialOrder.iocam._autoParam} {toSyn_1 : (σ →₀ ℕ) ≃+ syn_1}
  {toSyn_monotone_1 : Monotone ⇑toSyn_1} {wf_1 : autoParam (WellFoundedLT syn_1) MonomialOrder.wf._autoParam},
  { syn := syn, acm := acm, lo := lo, iocam := iocam, toSyn := toSyn, toSyn_monotone := toSyn_monotone, wf := wf } =
      { syn := syn_1, acm := acm_1, lo := lo_1, iocam := iocam_1, toSyn := toSyn_1, toSyn_monotone := toSyn_monotone_1,
        wf := wf_1 } →
    syn = syn_1 ∧ acm ≍ acm_1 ∧ lo ≍ lo_1 ∧ toSyn ≍ toSyn_1