Dappend eq add Cases

@[csimp]theorem dappend_eq_addCases : @dappend = @addCases := by  ext m n motive u v i  induction n with  | zero => simp [dappend, addCases, castLT]  | succ n ih =>    simp only [dappend, dconcat_eq_snoc]    have ih' : ∀ (motive : Fin (m + n) → Sort _)      (u : (i : Fin m) → motive (castAdd n i))      (v : (i : Fin n) → motive (natAdd m i)),        dappend (motive := motive) u v = addCases (motive := motive) u v := by      intro motive_1 u_1 v_1      ext x : 1      apply ih    rw [ih' (fun i => motive i.castSucc) u (fun i => v (castSucc i))]    simp [snoc, addCases, last, castLT, subNat]    by_cases h : i.val < m    · have : i.val < m + n := by omega      simp [h, this]    · by_cases h' : i.val < m + n      · grind only      · have : i.val = m + n := by omega        grind only [cases Or]