∀ (R : Type u_1) [inst : Semiring R] (M : Type u_2) [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (N : Type u_3)
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} [inst_5 : Subsingleton ι] (i i_1 : ι),
  i = i_1 → AlternatingMap.ofSubsingleton R M N i = AlternatingMap.ofSubsingleton R M N i_1