English
Let α be a type with a symmetric difference operation, and let a,b ∈ α. The embedding a ↦ some a preserves the operation, i.e. some a \ some b = some (a \ b).
Русский
Пусть α — тип с операцией симметрической разности, и возьмём a, b ∈ α. Встраивание a ↦ some a сохраняет операцию: some a \ some b = some (a \ b).
LaTeX
$$$$ \\operatorname{some}(a) \\backslash \\operatorname{some}(b) = \\operatorname{some}(a \\backslash b) $$$$
Lean4
theorem some_sdiff_some [SDiff α] (a b : α) : some a \ some b = some (a \ b) := by simp [sdiff_def]