let msubst {x₁ x₂ : ℤ} : x₁ ≃ x₂ → motive x₁ → motive x₂ := by
  intro (_ : x₁ ≃ x₂) (_ : motive x₁)
  show motive x₂
  have Exists.intro (n : ℕ) (Exists.intro (m : ℕ) (_ : x₁ ≃ n - m)) :=
    ‹motive x₁›
  have : x₂ ≃ n - m := calc
    _ = x₂    := rfl
    _ ≃ x₁    := Rel.symm ‹x₁ ≃ x₂›
    _ ≃ n - m := ‹x₁ ≃ n - m›
  have : ∃ (n m : ℕ), x₂ ≃ n - m := Exists.intro n (Exists.intro m this)
  have : motive x₂ := this
  exact this
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
msubst : ∀ {x₁ x₂ : ℤ}, x₁ ≃ x₂ → motive x₁ → motive x₂ :=
  fun {x₁ x₂} h =>
    match h with
    | x => fun h =>
      match h with
      | x_1 =>
        let_fun this :=
          match x_1 with
          | Exists.intro n (Exists.intro m h) =>
            let_fun this := trans (trans rfl (Rel.symm x)) h;
            let_fun this := Exists.intro n (Exists.intro m this);
            let_fun this := this;
            this;
        this
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m