∀ (motive : (x x_1 : CircleDeg1Lift) → (fun f => f.toFun) x = (fun f => f.toFun) x_1 → Prop) (x x_1 : CircleDeg1Lift)
  (x_2 : (fun f => f.toFun) x = (fun f => f.toFun) x_1),
  (∀ (toFun : ℝ → ℝ) (monotone' : Monotone toFun)
      (map_add_one' :
        ∀ (x : ℝ),
          { toFun := toFun, monotone' := monotone' }.toFun (x + 1) =
            { toFun := toFun, monotone' := monotone' }.toFun x + 1)
      (monotone'_1 : Monotone toFun)
      (map_add_one'_1 :
        ∀ (x : ℝ),
          { toFun := toFun, monotone' := monotone'_1 }.toFun (x + 1) =
            { toFun := toFun, monotone' := monotone'_1 }.toFun x + 1),
      motive { toFun := toFun, monotone' := monotone', map_add_one' := map_add_one' }
        { toFun := toFun, monotone' := monotone'_1, map_add_one' := map_add_one'_1 } ⋯) →
    motive x x_1 x_2