calc
  _ = ctx.ind_diff (n - m)                         := rfl
  _ ≃ fsubst des (ctx.ind_diff (n——m))             := Rel.symm ind_diff_subst
  _ = fsubst des (fsubst sed (ctx.on_diff n m))    := rfl
  _ ≃ fsubst (Rel.trans sed des) (ctx.on_diff n m) := fsubst_trans
  _ = fsubst Rel.refl (ctx.on_diff n m)            := rfl
  _ ≃ ctx.on_diff n m                              := fsubst_refl
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n m : ℕ
sed : n——0 - m——0 ≃ n——m
des : n——m ≃ n——0 - m——0
⊢ Induction.Context.ind_diff ctx (n——0 - m——0) ≃ Induction.Context.on_diff n m
no goals