let a₁ := n₁——m₁
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
⊢ ∀ {a_eqv : n₁——m₁ ≃ n₂——m₂},
    fsubst a_eqv (Induction.Context.ind_diff ctx (n₁——m₁)) ≃ Induction.Context.ind_diff ctx (n₂——m₂)
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
⊢ ∀ {a_eqv : n₁——m₁ ≃ n₂——m₂},
    fsubst a_eqv (Induction.Context.ind_diff ctx (n₁——m₁)) ≃ Induction.Context.ind_diff ctx (n₂——m₂)