ink

theorem merge_not_empty : ∀ {α : Type} {ms₁ ms₂ : List Meas} {F : Factory α}, ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (ms₁, ms₂) ≠ []