import Pretty.Defs.Basic
import Pretty.Supports.Domination

lemma merge_not_empty: ∀ {α : Type} {ms₁ ms₂ : List Meas} {F : Factory α}, ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (ms₁, ms₂) ≠ []
merge_not_empty (h: ms₁ ≠ [] ∨ ms₂ ≠ []
h : ms₁: ?m.5
ms₁ ≠ []: List ?m.44
[] ∨ ms₂: ?m.17
ms₂ ≠ []: List ?m.50
[]) : 
    @merge: {α : Type} → Factory α → List Meas × List Meas → List Meas
merge _: Type
_ F: ?m.38
F ⟨ms₁: ?m.5
ms₁, ms₂: ?m.17
ms₂⟩ ≠ []: List ?m.73
[] := by
Goals accomplished! 🐙 
  α✝: Type

ms₁, ms₂: List Meas

F: Factory α✝

h: ms₁ ≠ [] ∨ ms₂ ≠ []

merge F (ms₁, ms₂) ≠ []induction ms₁: List Meas
ms₁ generalizing ms₂: List Meas
ms₂α✝: Type

F: Factory α✝

ms₂: List Meas

h: [] ≠ [] ∨ ms₂ ≠ []

nilmerge F ([], ms₂) ≠ []
α✝: Type

F: Factory α✝

head✝: Meas

tail✝: List Meas

tail_ih✝: ∀ {ms₂ : List Meas}, tail✝ ≠ [] ∨ ms₂ ≠ [] → merge F (tail✝, ms₂) ≠ []

ms₂: List Meas

h: head✝ :: tail✝ ≠ [] ∨ ms₂ ≠ []

consmerge F (head✝ :: tail✝, ms₂) ≠ []
  α✝: Type

ms₁, ms₂: List Meas

F: Factory α✝

h: ms₁ ≠ [] ∨ ms₂ ≠ []

merge F (ms₁, ms₂) ≠ []case nil => 
    α✝: Type

F: Factory α✝

ms₂: List Meas

h: [] ≠ [] ∨ ms₂ ≠ []

merge F ([], ms₂) ≠ []dwi { α✝: Type

F: Factory α✝

ms₂: List Meas

h: [] ≠ [] ∨ ms₂ ≠ []

merge F ([], ms₂) ≠ []cases h: [] ≠ [] ∨ ms₂ ≠ []
hα✝: Type

F: Factory α✝

ms₂: List Meas

h✝: [] ≠ []

inlmerge F ([], ms₂) ≠ []
α✝: Type

F: Factory α✝

ms₂: List Meas

h✝: ms₂ ≠ []

inrmerge F ([], ms₂) ≠ [] }α✝: Type

F: Factory α✝

ms₂: List Meas

h✝: ms₂ ≠ []

inrmerge F ([], ms₂) ≠ []
    α✝: Type

F: Factory α✝

ms₂: List Meas

h: [] ≠ [] ∨ ms₂ ≠ []

merge F ([], ms₂) ≠ []case inr => α✝: Type

F: Factory α✝

ms₂: List Meas

h✝: ms₂ ≠ []

merge F ([], ms₂) ≠ []simpa [merge: {α : Type} → Factory α → List Meas × List Meas → List Meas
merge]
Goals accomplished! 🐙
  α✝: Type

ms₁, ms₂: List Meas

F: Factory α✝

h: ms₁ ≠ [] ∨ ms₂ ≠ []

merge F (ms₁, ms₂) ≠ []case cons m₁: ?m.107
m₁ ms₁: List ?m.107
ms₁ ih₁: ?m.108 ms₁
ih₁ =>
    α✝: Type

F: Factory α✝

m₁: Meas

ms₁: List Meas

ih₁: ∀ {ms₂ : List Meas}, ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (ms₁, ms₂) ≠ []

ms₂: List Meas

h: m₁ :: ms₁ ≠ [] ∨ ms₂ ≠ []

merge F (m₁ :: ms₁, ms₂) ≠ []induction ms₂: List Meas
ms₂α✝: Type

F: Factory α✝

m₁: Meas

ms₁: List Meas

ih₁: ∀ {ms₂ : List Meas}, ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (ms₁, ms₂) ≠ []

h: m₁ :: ms₁ ≠ [] ∨ [] ≠ []

nilmerge F (m₁ :: ms₁, []) ≠ []
α✝: Type

F: Factory α✝

m₁: Meas

ms₁: List Meas

ih₁: ∀ {ms₂ : List Meas}, ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (ms₁, ms₂) ≠ []

head✝: Meas

tail✝: List Meas

tail_ih✝: m₁ :: ms₁ ≠ [] ∨ tail✝ ≠ [] → merge F (m₁ :: ms₁, tail✝) ≠ []

h: m₁ :: ms₁ ≠ [] ∨ head✝ :: tail✝ ≠ []

consmerge F (m₁ :: ms₁, head✝ :: tail✝) ≠ []
    α✝: Type

F: Factory α✝

m₁: Meas

ms₁: List Meas

ih₁: ∀ {ms₂ : List Meas}, ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (ms₁, ms₂) ≠ []

ms₂: List Meas

h: m₁ :: ms₁ ≠ [] ∨ ms₂ ≠ []

merge F (m₁ :: ms₁, ms₂) ≠ []case nil => α✝: Type

F: Factory α✝

m₁: Meas

ms₁: List Meas

ih₁: ∀ {ms₂ : List Meas}, ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (ms₁, ms₂) ≠ []

h: m₁ :: ms₁ ≠ [] ∨ [] ≠ []

merge F (m₁ :: ms₁, []) ≠ []dwi { α✝: Type

F: Factory α✝

m₁: Meas

ms₁: List Meas

ih₁: ∀ {ms₂ : List Meas}, ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (ms₁, ms₂) ≠ []

h: m₁ :: ms₁ ≠ [] ∨ [] ≠ []

merge F (m₁ :: ms₁, []) ≠ []cases h: m₁ :: ms₁ ≠ [] ∨ [] ≠ []
hα✝: Type

F: Factory α✝

m₁: Meas

ms₁: List Meas

ih₁: ∀ {ms₂ : List Meas}, ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (ms₁, ms₂) ≠ []

h✝: m₁ :: ms₁ ≠ []

inlmerge F (m₁ :: ms₁, []) ≠ []
α✝: Type

F: Factory α✝

m₁: Meas

ms₁: List Meas

ih₁: ∀ {ms₂ : List Meas}, ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (ms₁, ms₂) ≠ []

h✝: [] ≠ []

inrmerge F (m₁ :: ms₁, []) ≠ [] }
Goals accomplished! 🐙
    α✝: Type

F: Factory α✝

m₁: Meas

ms₁: List Meas

ih₁: ∀ {ms₂ : List Meas}, ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (ms₁, ms₂) ≠ []

ms₂: List Meas

h: m₁ :: ms₁ ≠ [] ∨ ms₂ ≠ []

merge F (m₁ :: ms₁, ms₂) ≠ []case cons m₂: ?m.2051
m₂ ms₂: List ?m.2051
ms₂ ih₂: ?m.2052 ms₂
ih₂ =>
      α✝: Type

F: Factory α✝

m₁: Meas

ms₁: List Meas

ih₁: ∀ {ms₂ : List Meas}, ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (ms₁, ms₂) ≠ []

m₂: Meas

ms₂: List Meas

ih₂: m₁ :: ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (m₁ :: ms₁, ms₂) ≠ []

h: m₁ :: ms₁ ≠ [] ∨ m₂ :: ms₂ ≠ []

merge F (m₁ :: ms₁, m₂ :: ms₂) ≠ []cases four_cases: ∀ {α : Type} (F : Factory α) (m₁ m₂ : Meas), FourCases F m₁ m₂
four_cases F: Factory α✝
F m₁: ?m.107
m₁ m₂: ?m.2051
m₂α✝: Type

F: Factory α✝

m₁: Meas

ms₁: List Meas

ih₁: ∀ {ms₂ : List Meas}, ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (ms₁, ms₂) ≠ []

m₂: Meas

ms₂: List Meas

ih₂: m₁ :: ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (m₁ :: ms₁, ms₂) ≠ []

h: m₁ :: ms₁ ≠ [] ∨ m₂ :: ms₂ ≠ []

h_dom✝: dominates F m₁ m₂ = true

first_dommerge F (m₁ :: ms₁, m₂ :: ms₂) ≠ []
α✝: Type

F: Factory α✝

m₁: Meas

ms₁: List Meas

ih₁: ∀ {ms₂ : List Meas}, ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (ms₁, ms₂) ≠ []

m₂: Meas

ms₂: List Meas

ih₂: m₁ :: ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (m₁ :: ms₁, ms₂) ≠ []

h: m₁ :: ms₁ ≠ [] ∨ m₂ :: ms₂ ≠ []

h_non_dom✝: ¬dominates F m₁ m₂ = true

h_dom✝: dominates F m₂ m₁ = true

second_dommerge F (m₁ :: ms₁, m₂ :: ms₂) ≠ []
α✝: Type

F: Factory α✝

m₁: Meas

ms₁: List Meas

ih₁: ∀ {ms₂ : List Meas}, ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (ms₁, ms₂) ≠ []

m₂: Meas

ms₂: List Meas

ih₂: m₁ :: ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (m₁ :: ms₁, ms₂) ≠ []

h: m₁ :: ms₁ ≠ [] ∨ m₂ :: ms₂ ≠ []

h_non_dom₁✝: ¬dominates F m₁ m₂ = true

h_non_dom₂✝: ¬dominates F m₂ m₁ = true

h✝: m₁.last > m₂.last

first_lastmerge F (m₁ :: ms₁, m₂ :: ms₂) ≠ []
α✝: Type

F: Factory α✝

m₁: Meas

ms₁: List Meas

ih₁: ∀ {ms₂ : List Meas}, ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (ms₁, ms₂) ≠ []

m₂: Meas

ms₂: List Meas

ih₂: m₁ :: ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (m₁ :: ms₁, ms₂) ≠ []

h: m₁ :: ms₁ ≠ [] ∨ m₂ :: ms₂ ≠ []

h_non_dom₁✝: ¬dominates F m₁ m₂ = true

h_non_dom₂✝: ¬dominates F m₂ m₁ = true

h✝: m₂.last > m₁.last

second_lastmerge F (m₁ :: ms₁, m₂ :: ms₂) ≠ []
      α✝: Type

F: Factory α✝

m₁: Meas

ms₁: List Meas

ih₁: ∀ {ms₂ : List Meas}, ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (ms₁, ms₂) ≠ []

m₂: Meas

ms₂: List Meas

ih₂: m₁ :: ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (m₁ :: ms₁, ms₂) ≠ []

h: m₁ :: ms₁ ≠ [] ∨ m₂ :: ms₂ ≠ []

merge F (m₁ :: ms₁, m₂ :: ms₂) ≠ []case first_dom | second_dom => 
        α✝: Type

F: Factory α✝

m₁: Meas

ms₁: List Meas

ih₁: ∀ {ms₂ : List Meas}, ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (ms₁, ms₂) ≠ []

m₂: Meas

ms₂: List Meas

ih₂: m₁ :: ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (m₁ :: ms₁, ms₂) ≠ []

h: m₁ :: ms₁ ≠ [] ∨ m₂ :: ms₂ ≠ []

h_non_dom✝: ¬dominates F m₁ m₂ = true

h_dom✝: dominates F m₂ m₁ = true

merge F (m₁ :: ms₁, m₂ :: ms₂) ≠ []simp [merge: {α : Type} → Factory α → List Meas × List Meas → List Meas
merge, *]
Goals accomplished! 🐙
      α✝: Type

F: Factory α✝

m₁: Meas

ms₁: List Meas

ih₁: ∀ {ms₂ : List Meas}, ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (ms₁, ms₂) ≠ []

m₂: Meas

ms₂: List Meas

ih₂: m₁ :: ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (m₁ :: ms₁, ms₂) ≠ []

h: m₁ :: ms₁ ≠ [] ∨ m₂ :: ms₂ ≠ []

merge F (m₁ :: ms₁, m₂ :: ms₂) ≠ []case first_last => 
        α✝: Type

F: Factory α✝

m₁: Meas

ms₁: List Meas

ih₁: ∀ {ms₂ : List Meas}, ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (ms₁, ms₂) ≠ []

m₂: Meas

ms₂: List Meas

ih₂: m₁ :: ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (m₁ :: ms₁, ms₂) ≠ []

h: m₁ :: ms₁ ≠ [] ∨ m₂ :: ms₂ ≠ []

h_non_dom₁✝: ¬dominates F m₁ m₂ = true

h_non_dom₂✝: ¬dominates F m₂ m₁ = true

h✝: m₁.last > m₂.last

merge F (m₁ :: ms₁, m₂ :: ms₂) ≠ []simp [merge: {α : Type} → Factory α → List Meas × List Meas → List Meas
merge, *]
Goals accomplished! 🐙
      α✝: Type

F: Factory α✝

m₁: Meas

ms₁: List Meas

ih₁: ∀ {ms₂ : List Meas}, ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (ms₁, ms₂) ≠ []

m₂: Meas

ms₂: List Meas

ih₂: m₁ :: ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (m₁ :: ms₁, ms₂) ≠ []

h: m₁ :: ms₁ ≠ [] ∨ m₂ :: ms₂ ≠ []

merge F (m₁ :: ms₁, m₂ :: ms₂) ≠ []case second_last =>
        α✝: Type

F: Factory α✝

m₁: Meas

ms₁: List Meas

ih₁: ∀ {ms₂ : List Meas}, ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (ms₁, ms₂) ≠ []

m₂: Meas

ms₂: List Meas

ih₂: m₁ :: ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (m₁ :: ms₁, ms₂) ≠ []

h: m₁ :: ms₁ ≠ [] ∨ m₂ :: ms₂ ≠ []

h_non_dom₁✝: ¬dominates F m₁ m₂ = true

h_non_dom₂✝: ¬dominates F m₂ m₁ = true

h✝: m₂.last > m₁.last

merge F (m₁ :: ms₁, m₂ :: ms₂) ≠ []have : ¬ m₁: ?m.107
m₁.last: {α : Type} → Meas → ℕ
last > m₂: ?m.2051
m₂.last: {α : Type} → Meas → ℕ
last := α✝: Type

F: Factory α✝

m₁: Meas

ms₁: List Meas

ih₁: ∀ {ms₂ : List Meas}, ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (ms₁, ms₂) ≠ []

m₂: Meas

ms₂: List Meas

ih₂: m₁ :: ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (m₁ :: ms₁, ms₂) ≠ []

h: m₁ :: ms₁ ≠ [] ∨ m₂ :: ms₂ ≠ []

h_non_dom₁✝: ¬dominates F m₁ m₂ = true

h_non_dom₂✝: ¬dominates F m₂ m₁ = true

h✝: m₂.last > m₁.last

merge F (m₁ :: ms₁, m₂ :: ms₂) ≠ []by
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

m₁: Meas

ms₁: List Meas

ih₁: ∀ {ms₂ : List Meas}, ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (ms₁, ms₂) ≠ []

m₂: Meas

ms₂: List Meas

ih₂: m₁ :: ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (m₁ :: ms₁, ms₂) ≠ []

h: m₁ :: ms₁ ≠ [] ∨ m₂ :: ms₂ ≠ []

h_non_dom₁✝: ¬dominates F m₁ m₂ = true

h_non_dom₂✝: ¬dominates F m₂ m₁ = true

h✝: m₂.last > m₁.last

¬m₁.last > m₂.lastlinarith
Goals accomplished! 🐙
        α✝: Type

F: Factory α✝

m₁: Meas

ms₁: List Meas

ih₁: ∀ {ms₂ : List Meas}, ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (ms₁, ms₂) ≠ []

m₂: Meas

ms₂: List Meas

ih₂: m₁ :: ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (m₁ :: ms₁, ms₂) ≠ []

h: m₁ :: ms₁ ≠ [] ∨ m₂ :: ms₂ ≠ []

h_non_dom₁✝: ¬dominates F m₁ m₂ = true

h_non_dom₂✝: ¬dominates F m₂ m₁ = true

h✝: m₂.last > m₁.last

merge F (m₁ :: ms₁, m₂ :: ms₂) ≠ []simp [merge: {α : Type} → Factory α → List Meas × List Meas → List Meas
merge, *]
Goals accomplished! 🐙