. intros; simp; ext; sorry_proof
case map_add
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
idx : Idx
⊢ ∀ (x y : Cont × Elem),
    (match x + y with
      | (cont, elem) => set cont idx elem) =
      (match x with
        | (cont, elem) => set cont idx elem) +
        match y with
        | (cont, elem) => set cont idx elem

case map_smul
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
idx : Idx
⊢ ∀ (c : R) (x : Cont × Elem),
    (match c • x with
      | (cont, elem) => set cont idx elem) =
      c •
        match x with
        | (cont, elem) => set cont idx elem
case map_smul
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
idx : Idx
⊢ ∀ (c : R) (x : Cont × Elem),
    (match c • x with
      | (cont, elem) => set cont idx elem) =
      c •
        match x with
        | (cont, elem) => set cont idx elem