import Pretty.Supports.DocSize
import Pretty.Defs.Resolve
import Pretty.Claims.MeasRender

/-!
## Determinism of resolving theorems
-/

mutual 
  /--
  The determinism of resolving (Page 19, Section 5.6)
  -/
  theorem Resolve_deterministic: ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {ms₁ ms₂ : MeasureSet},
  Resolve F d c i ms₁ → Resolve F d c i ms₂ → ms₁ = ms₂
Resolve_deterministic (h₁: Resolve F d c i ms₁
h₁ : Resolve: {α : Type} → Factory α → Doc → ℕ → ℕ → MeasureSet → Prop
Resolve F: ?m.4
F d: ?m.11
d c: ?m.17
c i: ?m.23
i ms₁: ?m.29
ms₁) (h₂: Resolve F d c i ms₂
h₂ : Resolve: {α : Type} → Factory α → Doc → ℕ → ℕ → MeasureSet → Prop
Resolve F: ?m.4
F d: ?m.11
d c: ?m.17
c i: ?m.23
i ms₂: ?m.39
ms₂) : ms₁: ?m.29
ms₁ = ms₂: ?m.39
ms₂ := by
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

h₁: Resolve F d c i ms₁

h₂: Resolve F d c i ms₂

ms₁ = ms₂{α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

h₁: Resolve F d c i ms₁

h₂: Resolve F d c i ms₂

ms₁ = ms₂
    α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

h₁: Resolve F d c i ms₁

h₂: Resolve F d c i ms₂

ms₁ = ms₂match d: Doc
d with 
    α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

h₁: Resolve F d c i ms₁

h₂: Resolve F d c i ms₂

ms₁ = ms₂| Doc.text: String → Doc
Doc.text _ =>α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

s✝: String

h₁: Resolve F (Doc.text s✝) c i ms₁

h₂: Resolve F (Doc.text s✝) c i ms₂

ms₁ = ms₂ 
      α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

h₁: Resolve F d c i ms₁

h₂: Resolve F d c i ms₂

ms₁ = ms₂cases h₁: Resolve F (Doc.text s✝) c i ms₁
h₁α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

s✝: String

h₂: Resolve F (Doc.text s✝) c i ms₂

m✝: Meas

h_bad✝: c + String.length s✝ > F.W ∨ i > F.W

h✝: MeasRender F (Doc.text s✝) c i m✝

text_taintMeasureSet.tainted m✝ = ms₂
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

s✝: String

h₂: Resolve F (Doc.text s✝) c i ms₂

m✝: Meas

h_c✝: c + String.length s✝ ≤ F.W

h_i✝: i ≤ F.W

h✝: MeasRender F (Doc.text s✝) c i m✝

text_setMeasureSet.set [m✝] (_ : ¬[m✝] = []) = ms₂ 
      α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

s✝: String

h₁: Resolve F (Doc.text s✝) c i ms₁

h₂: Resolve F (Doc.text s✝) c i ms₂

ms₁ = ms₂case text_taint h_bad: c + String.length s✝ > F.W ∨ i > F.W
h_bad h₁: MeasRender F (Doc.text s✝) c i m✝
h₁ => 
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

s✝: String

h₂: Resolve F (Doc.text s✝) c i ms₂

m✝: Meas

h_bad: c + String.length s✝ > F.W ∨ i > F.W

h₁: MeasRender F (Doc.text s✝) c i m✝

MeasureSet.tainted m✝ = ms₂cases h₂: Resolve F (Doc.text s✝) c i ms₂
h₂α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h_bad: c + String.length s✝ > F.W ∨ i > F.W

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h_bad✝: c + String.length s✝ > F.W ∨ i > F.W

h✝: MeasRender F (Doc.text s✝) c i m✝

text_taintMeasureSet.tainted m✝¹ = MeasureSet.tainted m✝
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h_bad: c + String.length s✝ > F.W ∨ i > F.W

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h_c✝: c + String.length s✝ ≤ F.W

h_i✝: i ≤ F.W

h✝: MeasRender F (Doc.text s✝) c i m✝

text_setMeasureSet.tainted m✝¹ = MeasureSet.set [m✝] (_ : ¬[m✝] = []) 
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

s✝: String

h₂: Resolve F (Doc.text s✝) c i ms₂

m✝: Meas

h_bad: c + String.length s✝ > F.W ∨ i > F.W

h₁: MeasRender F (Doc.text s✝) c i m✝

MeasureSet.tainted m✝ = ms₂case text_taint h₂: MeasRender F (Doc.text s✝) c i m✝
h₂ => 
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h_bad: c + String.length s✝ > F.W ∨ i > F.W

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h_bad✝: c + String.length s✝ > F.W ∨ i > F.W

h₂: MeasRender F (Doc.text s✝) c i m✝

MeasureSet.tainted m✝¹ = MeasureSet.tainted m✝have := MeasRender_deterministic: ∀ {α : Type} {d : Doc} {c i : ℕ} {F : Factory α} {m₁ m₂ : Meas}, MeasRender F d c i m₁ → MeasRender F d c i m₂ → m₁ = m₂
MeasRender_deterministic h₁: MeasRender F (Doc.text s✝) c i m✝¹
h₁ h₂: MeasRender F (Doc.text s✝) c i m✝
h₂α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h_bad: c + String.length s✝ > F.W ∨ i > F.W

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h_bad✝: c + String.length s✝ > F.W ∨ i > F.W

h₂: MeasRender F (Doc.text s✝) c i m✝

this: m✝¹ = m✝

MeasureSet.tainted m✝¹ = MeasureSet.tainted m✝
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h_bad: c + String.length s✝ > F.W ∨ i > F.W

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h_bad✝: c + String.length s✝ > F.W ∨ i > F.W

h₂: MeasRender F (Doc.text s✝) c i m✝

MeasureSet.tainted m✝¹ = MeasureSet.tainted m✝subst this: ?m.1758
thisα✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝: Meas

h_bad: c + String.length s✝ > F.W ∨ i > F.W

h₁: MeasRender F (Doc.text s✝) c i m✝

h_bad✝: c + String.length s✝ > F.W ∨ i > F.W

h₂: MeasRender F (Doc.text s✝) c i m✝

MeasureSet.tainted m✝ = MeasureSet.tainted m✝
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h_bad: c + String.length s✝ > F.W ∨ i > F.W

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h_bad✝: c + String.length s✝ > F.W ∨ i > F.W

h₂: MeasRender F (Doc.text s✝) c i m✝

MeasureSet.tainted m✝¹ = MeasureSet.tainted m✝simp
Goals accomplished! 🐙
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

s✝: String

h₂: Resolve F (Doc.text s✝) c i ms₂

m✝: Meas

h_bad: c + String.length s✝ > F.W ∨ i > F.W

h₁: MeasRender F (Doc.text s✝) c i m✝

MeasureSet.tainted m✝ = ms₂case text_set h_c: c + String.length s✝ ≤ F.W
h_c h_i: i ≤ F.W
h_i _=> 
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h_bad: c + String.length s✝ > F.W ∨ i > F.W

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h✝: MeasRender F (Doc.text s✝) c i m✝

MeasureSet.tainted m✝¹ = MeasureSet.set [m✝] (_ : ¬[m✝] = [])cases h_bad: c + String.length s✝ > F.W ∨ i > F.W
h_badα✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h✝¹: MeasRender F (Doc.text s✝) c i m✝

h✝: c + String.length s✝ > F.W

inlMeasureSet.tainted m✝¹ = MeasureSet.set [m✝] (_ : ¬[m✝] = [])
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h✝¹: MeasRender F (Doc.text s✝) c i m✝

h✝: i > F.W

inrMeasureSet.tainted m✝¹ = MeasureSet.set [m✝] (_ : ¬[m✝] = []) 
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h_bad: c + String.length s✝ > F.W ∨ i > F.W

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h✝: MeasRender F (Doc.text s✝) c i m✝

MeasureSet.tainted m✝¹ = MeasureSet.set [m✝] (_ : ¬[m✝] = [])case inl h_bad: ?m.1836
h_bad => 
            α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h✝: MeasRender F (Doc.text s✝) c i m✝

h_bad: c + String.length s✝ > F.W

MeasureSet.tainted m✝¹ = MeasureSet.set [m✝] (_ : ¬[m✝] = [])replace h_bad: ?m.1881
h_bad := Nat.not_le_of_lt: ∀ {n m : ℕ}, m < n → ¬n ≤ m
Nat.not_le_of_lt h_bad: ?m.1836
h_badα✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h✝: MeasRender F (Doc.text s✝) c i m✝

h_bad: ¬c + String.length s✝ ≤ F.W

MeasureSet.tainted m✝¹ = MeasureSet.set [m✝] (_ : ¬[m✝] = []) 
            α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h✝: MeasRender F (Doc.text s✝) c i m✝

h_bad: c + String.length s✝ > F.W

MeasureSet.tainted m✝¹ = MeasureSet.set [m✝] (_ : ¬[m✝] = [])contradiction
Goals accomplished! 🐙
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h_bad: c + String.length s✝ > F.W ∨ i > F.W

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h✝: MeasRender F (Doc.text s✝) c i m✝

MeasureSet.tainted m✝¹ = MeasureSet.set [m✝] (_ : ¬[m✝] = [])case inr h_bad: ?m.1837
h_bad =>
            α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h✝: MeasRender F (Doc.text s✝) c i m✝

h_bad: i > F.W

MeasureSet.tainted m✝¹ = MeasureSet.set [m✝] (_ : ¬[m✝] = [])replace h_bad: ?m.2639
h_bad := Nat.not_le_of_lt: ∀ {n m : ℕ}, m < n → ¬n ≤ m
Nat.not_le_of_lt h_bad: ?m.1837
h_badα✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h✝: MeasRender F (Doc.text s✝) c i m✝

h_bad: ¬i ≤ F.W

MeasureSet.tainted m✝¹ = MeasureSet.set [m✝] (_ : ¬[m✝] = []) 
            α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h✝: MeasRender F (Doc.text s✝) c i m✝

h_bad: i > F.W

MeasureSet.tainted m✝¹ = MeasureSet.set [m✝] (_ : ¬[m✝] = [])contradiction
Goals accomplished! 🐙
      α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

s✝: String

h₁: Resolve F (Doc.text s✝) c i ms₁

h₂: Resolve F (Doc.text s✝) c i ms₂

ms₁ = ms₂case text_set h_c: c + String.length s✝ ≤ F.W
h_c h_i: i ≤ F.W
h_i h₁: MeasRender F (Doc.text s✝) c i m✝
h₁ => 
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

s✝: String

h₂: Resolve F (Doc.text s✝) c i ms₂

m✝: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F (Doc.text s✝) c i m✝

MeasureSet.set [m✝] (_ : ¬[m✝] = []) = ms₂cases h₂: Resolve F (Doc.text s✝) c i ms₂
h₂α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h_bad✝: c + String.length s✝ > F.W ∨ i > F.W

h✝: MeasRender F (Doc.text s✝) c i m✝

text_taintMeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.tainted m✝
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h_c✝: c + String.length s✝ ≤ F.W

h_i✝: i ≤ F.W

h✝: MeasRender F (Doc.text s✝) c i m✝

text_setMeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.set [m✝] (_ : ¬[m✝] = []) 
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

s✝: String

h₂: Resolve F (Doc.text s✝) c i ms₂

m✝: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F (Doc.text s✝) c i m✝

MeasureSet.set [m✝] (_ : ¬[m✝] = []) = ms₂case text_taint h_bad: c + String.length s✝ > F.W ∨ i > F.W
h_bad _ => 
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h_bad: c + String.length s✝ > F.W ∨ i > F.W

h✝: MeasRender F (Doc.text s✝) c i m✝

MeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.tainted m✝cases h_bad: c + String.length s✝ > F.W ∨ i > F.W
h_badα✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h✝¹: MeasRender F (Doc.text s✝) c i m✝

h✝: c + String.length s✝ > F.W

inlMeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.tainted m✝
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h✝¹: MeasRender F (Doc.text s✝) c i m✝

h✝: i > F.W

inrMeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.tainted m✝ 
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h_bad: c + String.length s✝ > F.W ∨ i > F.W

h✝: MeasRender F (Doc.text s✝) c i m✝

MeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.tainted m✝case inl h_bad: ?m.3890
h_bad => 
            α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h✝: MeasRender F (Doc.text s✝) c i m✝

h_bad: c + String.length s✝ > F.W

MeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.tainted m✝replace h_bad: ?m.3935
h_bad := Nat.not_le_of_lt: ∀ {n m : ℕ}, m < n → ¬n ≤ m
Nat.not_le_of_lt h_bad: ?m.3890
h_badα✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h✝: MeasRender F (Doc.text s✝) c i m✝

h_bad: ¬c + String.length s✝ ≤ F.W

MeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.tainted m✝ 
            α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h✝: MeasRender F (Doc.text s✝) c i m✝

h_bad: c + String.length s✝ > F.W

MeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.tainted m✝contradiction
Goals accomplished! 🐙
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h_bad: c + String.length s✝ > F.W ∨ i > F.W

h✝: MeasRender F (Doc.text s✝) c i m✝

MeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.tainted m✝case inr h_bad: ?m.3891
h_bad =>
            α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h✝: MeasRender F (Doc.text s✝) c i m✝

h_bad: i > F.W

MeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.tainted m✝replace h_bad: ?m.4671
h_bad := Nat.not_le_of_lt: ∀ {n m : ℕ}, m < n → ¬n ≤ m
Nat.not_le_of_lt h_bad: ?m.3891
h_badα✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h✝: MeasRender F (Doc.text s✝) c i m✝

h_bad: ¬i ≤ F.W

MeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.tainted m✝ 
            α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h✝: MeasRender F (Doc.text s✝) c i m✝

h_bad: i > F.W

MeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.tainted m✝contradiction
Goals accomplished! 🐙
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

s✝: String

h₂: Resolve F (Doc.text s✝) c i ms₂

m✝: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F (Doc.text s✝) c i m✝

MeasureSet.set [m✝] (_ : ¬[m✝] = []) = ms₂case text_set h₂: MeasRender F (Doc.text s✝) c i m✝
h₂ => 
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h_c✝: c + String.length s✝ ≤ F.W

h_i✝: i ≤ F.W

h₂: MeasRender F (Doc.text s✝) c i m✝

MeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.set [m✝] (_ : ¬[m✝] = [])have := MeasRender_deterministic: ∀ {α : Type} {d : Doc} {c i : ℕ} {F : Factory α} {m₁ m₂ : Meas}, MeasRender F d c i m₁ → MeasRender F d c i m₂ → m₁ = m₂
MeasRender_deterministic h₁: MeasRender F (Doc.text s✝) c i m✝¹
h₁ h₂: MeasRender F (Doc.text s✝) c i m✝
h₂α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h_c✝: c + String.length s✝ ≤ F.W

h_i✝: i ≤ F.W

h₂: MeasRender F (Doc.text s✝) c i m✝

this: m✝¹ = m✝

MeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.set [m✝] (_ : ¬[m✝] = [])
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h_c✝: c + String.length s✝ ≤ F.W

h_i✝: i ≤ F.W

h₂: MeasRender F (Doc.text s✝) c i m✝

MeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.set [m✝] (_ : ¬[m✝] = [])subst this: ?m.5394
thisα✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F (Doc.text s✝) c i m✝

h_c✝: c + String.length s✝ ≤ F.W

h_i✝: i ≤ F.W

h₂: MeasRender F (Doc.text s✝) c i m✝

MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.set [m✝] (_ : ¬[m✝] = [])
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

s✝: String

m✝¹: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F (Doc.text s✝) c i m✝¹

m✝: Meas

h_c✝: c + String.length s✝ ≤ F.W

h_i✝: i ≤ F.W

h₂: MeasRender F (Doc.text s✝) c i m✝

MeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.set [m✝] (_ : ¬[m✝] = [])simp
Goals accomplished! 🐙
    α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

h₁: Resolve F d c i ms₁

h₂: Resolve F d c i ms₂

ms₁ = ms₂| Doc.nl: Doc
Doc.nl =>α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

h₁: Resolve F Doc.nl c i ms₁

h₂: Resolve F Doc.nl c i ms₂

ms₁ = ms₂ 
      α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

h₁: Resolve F d c i ms₁

h₂: Resolve F d c i ms₂

ms₁ = ms₂cases h₁: Resolve F Doc.nl c i ms₁
h₁α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

h₂: Resolve F Doc.nl c i ms₂

m✝: Meas

h_bad✝: c > F.W ∨ i > F.W

h✝: MeasRender F Doc.nl c i m✝

line_taintMeasureSet.tainted m✝ = ms₂
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

h₂: Resolve F Doc.nl c i ms₂

m✝: Meas

h_c✝: c ≤ F.W

h_i✝: i ≤ F.W

h✝: MeasRender F Doc.nl c i m✝

line_setMeasureSet.set [m✝] (_ : ¬[m✝] = []) = ms₂ 
      α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

h₁: Resolve F Doc.nl c i ms₁

h₂: Resolve F Doc.nl c i ms₂

ms₁ = ms₂case line_taint h_bad: c > F.W ∨ i > F.W
h_bad h₁: MeasRender F Doc.nl c i m✝
h₁ => 
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

h₂: Resolve F Doc.nl c i ms₂

m✝: Meas

h_bad: c > F.W ∨ i > F.W

h₁: MeasRender F Doc.nl c i m✝

MeasureSet.tainted m✝ = ms₂cases h₂: Resolve F Doc.nl c i ms₂
h₂α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h_bad: c > F.W ∨ i > F.W

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h_bad✝: c > F.W ∨ i > F.W

h✝: MeasRender F Doc.nl c i m✝

line_taintMeasureSet.tainted m✝¹ = MeasureSet.tainted m✝
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h_bad: c > F.W ∨ i > F.W

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h_c✝: c ≤ F.W

h_i✝: i ≤ F.W

h✝: MeasRender F Doc.nl c i m✝

line_setMeasureSet.tainted m✝¹ = MeasureSet.set [m✝] (_ : ¬[m✝] = []) 
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

h₂: Resolve F Doc.nl c i ms₂

m✝: Meas

h_bad: c > F.W ∨ i > F.W

h₁: MeasRender F Doc.nl c i m✝

MeasureSet.tainted m✝ = ms₂case line_taint h₂: MeasRender F Doc.nl c i m✝
h₂ => 
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h_bad: c > F.W ∨ i > F.W

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h_bad✝: c > F.W ∨ i > F.W

h₂: MeasRender F Doc.nl c i m✝

MeasureSet.tainted m✝¹ = MeasureSet.tainted m✝have := MeasRender_deterministic: ∀ {α : Type} {d : Doc} {c i : ℕ} {F : Factory α} {m₁ m₂ : Meas}, MeasRender F d c i m₁ → MeasRender F d c i m₂ → m₁ = m₂
MeasRender_deterministic h₁: MeasRender F Doc.nl c i m✝¹
h₁ h₂: MeasRender F Doc.nl c i m✝
h₂α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h_bad: c > F.W ∨ i > F.W

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h_bad✝: c > F.W ∨ i > F.W

h₂: MeasRender F Doc.nl c i m✝

this: m✝¹ = m✝

MeasureSet.tainted m✝¹ = MeasureSet.tainted m✝
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h_bad: c > F.W ∨ i > F.W

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h_bad✝: c > F.W ∨ i > F.W

h₂: MeasRender F Doc.nl c i m✝

MeasureSet.tainted m✝¹ = MeasureSet.tainted m✝subst this: ?m.6379
thisα✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝: Meas

h_bad: c > F.W ∨ i > F.W

h₁: MeasRender F Doc.nl c i m✝

h_bad✝: c > F.W ∨ i > F.W

h₂: MeasRender F Doc.nl c i m✝

MeasureSet.tainted m✝ = MeasureSet.tainted m✝
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h_bad: c > F.W ∨ i > F.W

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h_bad✝: c > F.W ∨ i > F.W

h₂: MeasRender F Doc.nl c i m✝

MeasureSet.tainted m✝¹ = MeasureSet.tainted m✝simp
Goals accomplished! 🐙
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

h₂: Resolve F Doc.nl c i ms₂

m✝: Meas

h_bad: c > F.W ∨ i > F.W

h₁: MeasRender F Doc.nl c i m✝

MeasureSet.tainted m✝ = ms₂case line_set h_c: c ≤ F.W
h_c h_i: i ≤ F.W
h_i _ => 
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h_bad: c > F.W ∨ i > F.W

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h✝: MeasRender F Doc.nl c i m✝

MeasureSet.tainted m✝¹ = MeasureSet.set [m✝] (_ : ¬[m✝] = [])cases h_bad: c > F.W ∨ i > F.W
h_badα✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h✝¹: MeasRender F Doc.nl c i m✝

h✝: c > F.W

inlMeasureSet.tainted m✝¹ = MeasureSet.set [m✝] (_ : ¬[m✝] = [])
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h✝¹: MeasRender F Doc.nl c i m✝

h✝: i > F.W

inrMeasureSet.tainted m✝¹ = MeasureSet.set [m✝] (_ : ¬[m✝] = []) 
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h_bad: c > F.W ∨ i > F.W

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h✝: MeasRender F Doc.nl c i m✝

MeasureSet.tainted m✝¹ = MeasureSet.set [m✝] (_ : ¬[m✝] = [])case inl h_bad: ?m.6427
h_bad => 
            α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h✝: MeasRender F Doc.nl c i m✝

h_bad: c > F.W

MeasureSet.tainted m✝¹ = MeasureSet.set [m✝] (_ : ¬[m✝] = [])replace h_bad: ?m.6472
h_bad := Nat.not_le_of_lt: ∀ {n m : ℕ}, m < n → ¬n ≤ m
Nat.not_le_of_lt h_bad: ?m.6427
h_badα✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h✝: MeasRender F Doc.nl c i m✝

h_bad: ¬c ≤ F.W

MeasureSet.tainted m✝¹ = MeasureSet.set [m✝] (_ : ¬[m✝] = []) 
            α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h✝: MeasRender F Doc.nl c i m✝

h_bad: c > F.W

MeasureSet.tainted m✝¹ = MeasureSet.set [m✝] (_ : ¬[m✝] = [])contradiction
Goals accomplished! 🐙
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h_bad: c > F.W ∨ i > F.W

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h✝: MeasRender F Doc.nl c i m✝

MeasureSet.tainted m✝¹ = MeasureSet.set [m✝] (_ : ¬[m✝] = [])case inr h_bad: ?m.6428
h_bad =>
            α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h✝: MeasRender F Doc.nl c i m✝

h_bad: i > F.W

MeasureSet.tainted m✝¹ = MeasureSet.set [m✝] (_ : ¬[m✝] = [])replace h_bad: ?m.7165
h_bad := Nat.not_le_of_lt: ∀ {n m : ℕ}, m < n → ¬n ≤ m
Nat.not_le_of_lt h_bad: ?m.6428
h_badα✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h✝: MeasRender F Doc.nl c i m✝

h_bad: ¬i ≤ F.W

MeasureSet.tainted m✝¹ = MeasureSet.set [m✝] (_ : ¬[m✝] = []) 
            α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h✝: MeasRender F Doc.nl c i m✝

h_bad: i > F.W

MeasureSet.tainted m✝¹ = MeasureSet.set [m✝] (_ : ¬[m✝] = [])contradiction
Goals accomplished! 🐙
      α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

h₁: Resolve F Doc.nl c i ms₁

h₂: Resolve F Doc.nl c i ms₂

ms₁ = ms₂case line_set h_c: c ≤ F.W
h_c h_i: i ≤ F.W
h_i h₁: MeasRender F Doc.nl c i m✝
h₁ => 
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

h₂: Resolve F Doc.nl c i ms₂

m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F Doc.nl c i m✝

MeasureSet.set [m✝] (_ : ¬[m✝] = []) = ms₂cases h₂: Resolve F Doc.nl c i ms₂
h₂α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h_bad✝: c > F.W ∨ i > F.W

h✝: MeasRender F Doc.nl c i m✝

line_taintMeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.tainted m✝
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h_c✝: c ≤ F.W

h_i✝: i ≤ F.W

h✝: MeasRender F Doc.nl c i m✝

line_setMeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.set [m✝] (_ : ¬[m✝] = []) 
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

h₂: Resolve F Doc.nl c i ms₂

m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F Doc.nl c i m✝

MeasureSet.set [m✝] (_ : ¬[m✝] = []) = ms₂case line_taint h_bad: c > F.W ∨ i > F.W
h_bad _ => 
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h_bad: c > F.W ∨ i > F.W

h✝: MeasRender F Doc.nl c i m✝

MeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.tainted m✝cases h_bad: c > F.W ∨ i > F.W
h_badα✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h✝¹: MeasRender F Doc.nl c i m✝

h✝: c > F.W

inlMeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.tainted m✝
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h✝¹: MeasRender F Doc.nl c i m✝

h✝: i > F.W

inrMeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.tainted m✝ 
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h_bad: c > F.W ∨ i > F.W

h✝: MeasRender F Doc.nl c i m✝

MeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.tainted m✝case inl h_bad: ?m.8321
h_bad => 
            α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h✝: MeasRender F Doc.nl c i m✝

h_bad: c > F.W

MeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.tainted m✝replace h_bad: ?m.8366
h_bad := Nat.not_le_of_lt: ∀ {n m : ℕ}, m < n → ¬n ≤ m
Nat.not_le_of_lt h_bad: ?m.8321
h_badα✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h✝: MeasRender F Doc.nl c i m✝

h_bad: ¬c ≤ F.W

MeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.tainted m✝ 
            α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h✝: MeasRender F Doc.nl c i m✝

h_bad: c > F.W

MeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.tainted m✝contradiction
Goals accomplished! 🐙
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h_bad: c > F.W ∨ i > F.W

h✝: MeasRender F Doc.nl c i m✝

MeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.tainted m✝case inr h_bad: ?m.8322
h_bad =>
            α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h✝: MeasRender F Doc.nl c i m✝

h_bad: i > F.W

MeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.tainted m✝replace h_bad: ?m.9057
h_bad := Nat.not_le_of_lt: ∀ {n m : ℕ}, m < n → ¬n ≤ m
Nat.not_le_of_lt h_bad: ?m.8322
h_badα✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h✝: MeasRender F Doc.nl c i m✝

h_bad: ¬i ≤ F.W

MeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.tainted m✝ 
            α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h✝: MeasRender F Doc.nl c i m✝

h_bad: i > F.W

MeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.tainted m✝contradiction
Goals accomplished! 🐙
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

h₂: Resolve F Doc.nl c i ms₂

m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F Doc.nl c i m✝

MeasureSet.set [m✝] (_ : ¬[m✝] = []) = ms₂case line_set h₂: MeasRender F Doc.nl c i m✝
h₂ => 
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h_c✝: c ≤ F.W

h_i✝: i ≤ F.W

h₂: MeasRender F Doc.nl c i m✝

MeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.set [m✝] (_ : ¬[m✝] = [])have := MeasRender_deterministic: ∀ {α : Type} {d : Doc} {c i : ℕ} {F : Factory α} {m₁ m₂ : Meas}, MeasRender F d c i m₁ → MeasRender F d c i m₂ → m₁ = m₂
MeasRender_deterministic h₁: MeasRender F Doc.nl c i m✝¹
h₁ h₂: MeasRender F Doc.nl c i m✝
h₂α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h_c✝: c ≤ F.W

h_i✝: i ≤ F.W

h₂: MeasRender F Doc.nl c i m✝

this: m✝¹ = m✝

MeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.set [m✝] (_ : ¬[m✝] = [])
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h_c✝: c ≤ F.W

h_i✝: i ≤ F.W

h₂: MeasRender F Doc.nl c i m✝

MeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.set [m✝] (_ : ¬[m✝] = [])subst this: ?m.9741
thisα✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F Doc.nl c i m✝

h_c✝: c ≤ F.W

h_i✝: i ≤ F.W

h₂: MeasRender F Doc.nl c i m✝

MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.set [m✝] (_ : ¬[m✝] = [])
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝¹: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h₁: MeasRender F Doc.nl c i m✝¹

m✝: Meas

h_c✝: c ≤ F.W

h_i✝: i ≤ F.W

h₂: MeasRender F Doc.nl c i m✝

MeasureSet.set [m✝¹] (_ : ¬[m✝¹] = []) = MeasureSet.set [m✝] (_ : ¬[m✝] = [])simp
Goals accomplished! 🐙
    α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

h₁: Resolve F d c i ms₁

h₂: Resolve F d c i ms₂

ms₁ = ms₂| Doc.nest: ℕ → Doc → Doc
Doc.nest n: ℕ
n d': Doc
d' =>α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

n: ℕ

d': Doc

h₁: Resolve F (Doc.nest n d') c i ms₁

h₂: Resolve F (Doc.nest n d') c i ms₂

ms₁ = ms₂ 
      α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

h₁: Resolve F d c i ms₁

h₂: Resolve F d c i ms₂

ms₁ = ms₂cases h₁: Resolve F (Doc.nest n d') c i ms₁
h₁α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

n: ℕ

d': Doc

h₂: Resolve F (Doc.nest n d') c i ms₂

ms✝: MeasureSet

h✝: Resolve F d' c (i + n) ms✝

nestMeasureSet.lift (Meas.adjust_nest n) ms✝ = ms₂
      α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

n: ℕ

d': Doc

h₁: Resolve F (Doc.nest n d') c i ms₁

h₂: Resolve F (Doc.nest n d') c i ms₂

ms₁ = ms₂case nest h₁: Resolve F d' c (i + n) ms✝
h₁ => 
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

n: ℕ

d': Doc

h₂: Resolve F (Doc.nest n d') c i ms₂

ms✝: MeasureSet

h₁: Resolve F d' c (i + n) ms✝

MeasureSet.lift (Meas.adjust_nest n) ms✝ = ms₂cases h₂: Resolve F (Doc.nest n d') c i ms₂
h₂α✝: Type

F: Factory α✝

d: Doc

c, i, n: ℕ

d': Doc

ms✝¹: MeasureSet

h₁: Resolve F d' c (i + n) ms✝¹

ms✝: MeasureSet

h✝: Resolve F d' c (i + n) ms✝

nestMeasureSet.lift (Meas.adjust_nest n) ms✝¹ = MeasureSet.lift (Meas.adjust_nest n) ms✝ 
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

n: ℕ

d': Doc

h₂: Resolve F (Doc.nest n d') c i ms₂

ms✝: MeasureSet

h₁: Resolve F d' c (i + n) ms✝

MeasureSet.lift (Meas.adjust_nest n) ms✝ = ms₂case nest h₂: Resolve F d' c (i + n) ms✝
h₂ => 
          α✝: Type

F: Factory α✝

d: Doc

c, i, n: ℕ

d': Doc

ms✝¹: MeasureSet

h₁: Resolve F d' c (i + n) ms✝¹

ms✝: MeasureSet

h₂: Resolve F d' c (i + n) ms✝

MeasureSet.lift (Meas.adjust_nest n) ms✝¹ = MeasureSet.lift (Meas.adjust_nest n) ms✝have := Resolve_deterministic: ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {ms₁ ms₂ : MeasureSet},
  Resolve F d c i ms₁ → Resolve F d c i ms₂ → ms₁ = ms₂
Resolve_deterministic h₁: Resolve F d' c (i + n) ms✝¹
h₁ h₂: Resolve F d' c (i + n) ms✝
h₂α✝: Type

F: Factory α✝

d: Doc

c, i, n: ℕ

d': Doc

ms✝¹: MeasureSet

h₁: Resolve F d' c (i + n) ms✝¹

ms✝: MeasureSet

h₂: Resolve F d' c (i + n) ms✝

this: ms✝¹ = ms✝

MeasureSet.lift (Meas.adjust_nest n) ms✝¹ = MeasureSet.lift (Meas.adjust_nest n) ms✝
          α✝: Type

F: Factory α✝

d: Doc

c, i, n: ℕ

d': Doc

ms✝¹: MeasureSet

h₁: Resolve F d' c (i + n) ms✝¹

ms✝: MeasureSet

h₂: Resolve F d' c (i + n) ms✝

MeasureSet.lift (Meas.adjust_nest n) ms✝¹ = MeasureSet.lift (Meas.adjust_nest n) ms✝subst this: ?m.10653
thisα✝: Type

F: Factory α✝

d: Doc

c, i, n: ℕ

d': Doc

ms✝: MeasureSet

h₁, h₂: Resolve F d' c (i + n) ms✝

MeasureSet.lift (Meas.adjust_nest n) ms✝ = MeasureSet.lift (Meas.adjust_nest n) ms✝ 
          α✝: Type

F: Factory α✝

d: Doc

c, i, n: ℕ

d': Doc

ms✝¹: MeasureSet

h₁: Resolve F d' c (i + n) ms✝¹

ms✝: MeasureSet

h₂: Resolve F d' c (i + n) ms✝

MeasureSet.lift (Meas.adjust_nest n) ms✝¹ = MeasureSet.lift (Meas.adjust_nest n) ms✝simp
Goals accomplished! 🐙
    α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

h₁: Resolve F d c i ms₁

h₂: Resolve F d c i ms₂

ms₁ = ms₂| Doc.align: Doc → Doc
Doc.align d': Doc
d' =>α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

d': Doc

h₁: Resolve F (Doc.align d') c i ms₁

h₂: Resolve F (Doc.align d') c i ms₂

ms₁ = ms₂ 
      α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

h₁: Resolve F d c i ms₁

h₂: Resolve F d c i ms₂

ms₁ = ms₂cases h₁: Resolve F (Doc.align d') c i ms₁
h₁α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

d': Doc

h₂: Resolve F (Doc.align d') c i ms₂

ms✝: MeasureSet

h✝: Resolve F d' c c ms✝

h_bad✝: i > F.W

align_taintMeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms✝) = ms₂
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

d': Doc

h₂: Resolve F (Doc.align d') c i ms₂

ms✝: MeasureSet

h✝: Resolve F d' c c ms✝

h_ok✝: i ≤ F.W

alignMeasureSet.lift (Meas.adjust_align i) ms✝ = ms₂ 
      α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

d': Doc

h₁: Resolve F (Doc.align d') c i ms₁

h₂: Resolve F (Doc.align d') c i ms₂

ms₁ = ms₂case align h₁: Resolve F d' c c ms✝
h₁ h_ok: i ≤ F.W
h_ok =>
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

d': Doc

h₂: Resolve F (Doc.align d') c i ms₂

ms✝: MeasureSet

h₁: Resolve F d' c c ms✝

h_ok: i ≤ F.W

MeasureSet.lift (Meas.adjust_align i) ms✝ = ms₂cases h₂: Resolve F (Doc.align d') c i ms₂
h₂α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d': Doc

ms✝¹: MeasureSet

h₁: Resolve F d' c c ms✝¹

h_ok: i ≤ F.W

ms✝: MeasureSet

h✝: Resolve F d' c c ms✝

h_bad✝: i > F.W

align_taintMeasureSet.lift (Meas.adjust_align i) ms✝¹ = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms✝)
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d': Doc

ms✝¹: MeasureSet

h₁: Resolve F d' c c ms✝¹

h_ok: i ≤ F.W

ms✝: MeasureSet

h✝: Resolve F d' c c ms✝

h_ok✝: i ≤ F.W

alignMeasureSet.lift (Meas.adjust_align i) ms✝¹ = MeasureSet.lift (Meas.adjust_align i) ms✝ 
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

d': Doc

h₂: Resolve F (Doc.align d') c i ms₂

ms✝: MeasureSet

h₁: Resolve F d' c c ms✝

h_ok: i ≤ F.W

MeasureSet.lift (Meas.adjust_align i) ms✝ = ms₂case align_taint h_bad: i > F.W
h_bad => 
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d': Doc

ms✝¹: MeasureSet

h₁: Resolve F d' c c ms✝¹

h_ok: i ≤ F.W

ms✝: MeasureSet

h✝: Resolve F d' c c ms✝

h_bad: i > F.W

MeasureSet.lift (Meas.adjust_align i) ms✝¹ = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms✝)replace h_bad: ?m.11714
h_bad := Nat.not_le_of_lt: ∀ {n m : ℕ}, m < n → ¬n ≤ m
Nat.not_le_of_lt h_bad: i > F.W
h_badα✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d': Doc

ms✝¹: MeasureSet

h₁: Resolve F d' c c ms✝¹

h_ok: i ≤ F.W

ms✝: MeasureSet

h✝: Resolve F d' c c ms✝

h_bad: ¬i ≤ F.W

MeasureSet.lift (Meas.adjust_align i) ms✝¹ = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms✝)
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d': Doc

ms✝¹: MeasureSet

h₁: Resolve F d' c c ms✝¹

h_ok: i ≤ F.W

ms✝: MeasureSet

h✝: Resolve F d' c c ms✝

h_bad: i > F.W

MeasureSet.lift (Meas.adjust_align i) ms✝¹ = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms✝)contradiction
Goals accomplished! 🐙
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

d': Doc

h₂: Resolve F (Doc.align d') c i ms₂

ms✝: MeasureSet

h₁: Resolve F d' c c ms✝

h_ok: i ≤ F.W

MeasureSet.lift (Meas.adjust_align i) ms✝ = ms₂case align h₂: Resolve F d' c c ms✝
h₂ _ => α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d': Doc

ms✝¹: MeasureSet

h₁: Resolve F d' c c ms✝¹

h_ok: i ≤ F.W

ms✝: MeasureSet

h₂: Resolve F d' c c ms✝

h_ok✝: i ≤ F.W

MeasureSet.lift (Meas.adjust_align i) ms✝¹ = MeasureSet.lift (Meas.adjust_align i) ms✝simp [Resolve_deterministic: ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {ms₁ ms₂ : MeasureSet},
  Resolve F d c i ms₁ → Resolve F d c i ms₂ → ms₁ = ms₂
Resolve_deterministic h₁: Resolve F d' c c ms✝¹
h₁ h₂: Resolve F d' c c ms✝
h₂]
Goals accomplished! 🐙
      α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

d': Doc

h₁: Resolve F (Doc.align d') c i ms₁

h₂: Resolve F (Doc.align d') c i ms₂

ms₁ = ms₂case align_taint h: Resolve F d' c c ms✝
h h_bad: i > F.W
h_bad => 
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

d': Doc

h₂: Resolve F (Doc.align d') c i ms₂

ms✝: MeasureSet

h: Resolve F d' c c ms✝

h_bad: i > F.W

MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms✝) = ms₂cases h₂: Resolve F (Doc.align d') c i ms₂
h₂α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d': Doc

ms✝¹: MeasureSet

h: Resolve F d' c c ms✝¹

h_bad: i > F.W

ms✝: MeasureSet

h✝: Resolve F d' c c ms✝

h_bad✝: i > F.W

align_taintMeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms✝¹) =   MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms✝)
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d': Doc

ms✝¹: MeasureSet

h: Resolve F d' c c ms✝¹

h_bad: i > F.W

ms✝: MeasureSet

h✝: Resolve F d' c c ms✝

h_ok✝: i ≤ F.W

alignMeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms✝¹) = MeasureSet.lift (Meas.adjust_align i) ms✝ 
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

d': Doc

h₂: Resolve F (Doc.align d') c i ms₂

ms✝: MeasureSet

h: Resolve F d' c c ms✝

h_bad: i > F.W

MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms✝) = ms₂case align_taint h': Resolve F d' c c ms✝
h' _ => α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d': Doc

ms✝¹: MeasureSet

h: Resolve F d' c c ms✝¹

h_bad: i > F.W

ms✝: MeasureSet

h': Resolve F d' c c ms✝

h_bad✝: i > F.W

MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms✝¹) =   MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms✝)simp [Resolve_deterministic: ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {ms₁ ms₂ : MeasureSet},
  Resolve F d c i ms₁ → Resolve F d c i ms₂ → ms₁ = ms₂
Resolve_deterministic h: Resolve F d' c c ms✝¹
h h': Resolve F d' c c ms✝
h']
Goals accomplished! 🐙 
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

d': Doc

h₂: Resolve F (Doc.align d') c i ms₂

ms✝: MeasureSet

h: Resolve F d' c c ms✝

h_bad: i > F.W

MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms✝) = ms₂case align => 
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d': Doc

ms✝¹: MeasureSet

h: Resolve F d' c c ms✝¹

h_bad: i > F.W

ms✝: MeasureSet

h✝: Resolve F d' c c ms✝

h_ok✝: i ≤ F.W

MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms✝¹) = MeasureSet.lift (Meas.adjust_align i) ms✝replace h_bad: ?m.15329
h_bad := Nat.not_le_of_lt: ∀ {n m : ℕ}, m < n → ¬n ≤ m
Nat.not_le_of_lt h_bad: i > F.W
h_badα✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d': Doc

ms✝¹: MeasureSet

h: Resolve F d' c c ms✝¹

ms✝: MeasureSet

h✝: Resolve F d' c c ms✝

h_ok✝: i ≤ F.W

h_bad: ¬i ≤ F.W

MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms✝¹) = MeasureSet.lift (Meas.adjust_align i) ms✝
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d': Doc

ms✝¹: MeasureSet

h: Resolve F d' c c ms✝¹

h_bad: i > F.W

ms✝: MeasureSet

h✝: Resolve F d' c c ms✝

h_ok✝: i ≤ F.W

MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms✝¹) = MeasureSet.lift (Meas.adjust_align i) ms✝contradiction
Goals accomplished! 🐙
    α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

h₁: Resolve F d c i ms₁

h₂: Resolve F d c i ms₂

ms₁ = ms₂| Doc.choice: Doc → Doc → Doc
Doc.choice d₁: Doc
d₁ d₂: Doc
d₂ =>α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

d₁, d₂: Doc

h₁: Resolve F (Doc.choice d₁ d₂) c i ms₁

h₂: Resolve F (Doc.choice d₁ d₂) c i ms₂

ms₁ = ms₂ 
      α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

h₁: Resolve F d c i ms₁

h₂: Resolve F d c i ms₂

ms₁ = ms₂cases h₁: Resolve F (Doc.choice d₁ d₂) c i ms₁
h₁α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

d₁, d₂: Doc

h₂: Resolve F (Doc.choice d₁ d₂) c i ms₂

ms✝, ms'✝: MeasureSet

h_left✝: Resolve F d₁ c i ms✝

h_right✝: Resolve F d₂ c i ms'✝

choiceMeasureSet.union F ms✝ ms'✝ = ms₂
      α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

d₁, d₂: Doc

h₁: Resolve F (Doc.choice d₁ d₂) c i ms₁

h₂: Resolve F (Doc.choice d₁ d₂) c i ms₂

ms₁ = ms₂case choice h_right: Resolve F d₁ c i ms✝
h_right h_left: Resolve F d₂ c i ms'✝
h_left => 
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

d₁, d₂: Doc

h₂: Resolve F (Doc.choice d₁ d₂) c i ms₂

ms✝, ms'✝: MeasureSet

h_right: Resolve F d₁ c i ms✝

h_left: Resolve F d₂ c i ms'✝

MeasureSet.union F ms✝ ms'✝ = ms₂cases h₂: Resolve F (Doc.choice d₁ d₂) c i ms₂
h₂α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms✝¹, ms'✝¹: MeasureSet

h_right: Resolve F d₁ c i ms✝¹

h_left: Resolve F d₂ c i ms'✝¹

ms✝, ms'✝: MeasureSet

h_left✝: Resolve F d₁ c i ms✝

h_right✝: Resolve F d₂ c i ms'✝

choiceMeasureSet.union F ms✝¹ ms'✝¹ = MeasureSet.union F ms✝ ms'✝ 
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

d₁, d₂: Doc

h₂: Resolve F (Doc.choice d₁ d₂) c i ms₂

ms✝, ms'✝: MeasureSet

h_right: Resolve F d₁ c i ms✝

h_left: Resolve F d₂ c i ms'✝

MeasureSet.union F ms✝ ms'✝ = ms₂case choice h_right': Resolve F d₁ c i ms✝
h_right' h_left': Resolve F d₂ c i ms'✝
h_left' => 
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms✝¹, ms'✝¹: MeasureSet

h_right: Resolve F d₁ c i ms✝¹

h_left: Resolve F d₂ c i ms'✝¹

ms✝, ms'✝: MeasureSet

h_right': Resolve F d₁ c i ms✝

h_left': Resolve F d₂ c i ms'✝

MeasureSet.union F ms✝¹ ms'✝¹ = MeasureSet.union F ms✝ ms'✝simp [Resolve_deterministic: ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {ms₁ ms₂ : MeasureSet},
  Resolve F d c i ms₁ → Resolve F d c i ms₂ → ms₁ = ms₂
Resolve_deterministic h_left: Resolve F d₂ c i ms'✝¹
h_left h_left': Resolve F d₂ c i ms'✝
h_left', Resolve_deterministic: ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {ms₁ ms₂ : MeasureSet},
  Resolve F d c i ms₁ → Resolve F d c i ms₂ → ms₁ = ms₂
Resolve_deterministic h_right: Resolve F d₁ c i ms✝¹
h_right h_right': Resolve F d₁ c i ms✝
h_right']
Goals accomplished! 🐙
    α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

h₁: Resolve F d c i ms₁

h₂: Resolve F d c i ms₂

ms₁ = ms₂| Doc.concat: Doc → Doc → Doc
Doc.concat d₁: Doc
d₁ d₂: Doc
d₂ =>α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

d₁, d₂: Doc

h₁: Resolve F (Doc.concat d₁ d₂) c i ms₁

h₂: Resolve F (Doc.concat d₁ d₂) c i ms₂

ms₁ = ms₂ 
      α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

h₁: Resolve F d c i ms₁

h₂: Resolve F d c i ms₂

ms₁ = ms₂cases h₁: Resolve F (Doc.concat d₁ d₂) c i ms₁
h₁α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

d₁, d₂: Doc

h₂: Resolve F (Doc.concat d₁ d₂) c i ms₂

m✝: Meas

ms'✝: MeasureSet

m'✝: Meas

h_taint✝: MeasureSet.taint ms'✝ = MeasureSet.tainted m'✝

h_right✝: Resolve F d₂ m✝.last i ms'✝

h_left✝: Resolve F d₁ c i (MeasureSet.tainted m✝)

concat_taintMeasureSet.tainted (Meas.concat F m✝ m'✝) = ms₂
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

d₁, d₂: Doc

h₂: Resolve F (Doc.concat d₁ d₂) c i ms₂

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h_left✝: Resolve F d₁ c i (MeasureSet.set ms✝ h_non_empty✝)

h✝: ResolveConcat F ms✝ d₂ i ms₁

concat_setms₁ = ms₂ 
      α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

d₁, d₂: Doc

h₁: Resolve F (Doc.concat d₁ d₂) c i ms₁

h₂: Resolve F (Doc.concat d₁ d₂) c i ms₂

ms₁ = ms₂case concat_taint h_taint₁: MeasureSet.taint ms'✝ = MeasureSet.tainted m'✝
h_taint₁ h_right₁: Resolve F d₂ m✝.last i ms'✝
h_right₁ h_left₁: Resolve F d₁ c i (MeasureSet.tainted m✝)
h_left₁ => 
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

d₁, d₂: Doc

h₂: Resolve F (Doc.concat d₁ d₂) c i ms₂

m✝: Meas

ms'✝: MeasureSet

m'✝: Meas

h_taint₁: MeasureSet.taint ms'✝ = MeasureSet.tainted m'✝

h_right₁: Resolve F d₂ m✝.last i ms'✝

h_left₁: Resolve F d₁ c i (MeasureSet.tainted m✝)

MeasureSet.tainted (Meas.concat F m✝ m'✝) = ms₂cases h₂: Resolve F (Doc.concat d₁ d₂) c i ms₂
h₂α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d₁, d₂: Doc

m✝¹: Meas

ms'✝¹: MeasureSet

m'✝¹: Meas

h_taint₁: MeasureSet.taint ms'✝¹ = MeasureSet.tainted m'✝¹

h_right₁: Resolve F d₂ m✝¹.last i ms'✝¹

h_left₁: Resolve F d₁ c i (MeasureSet.tainted m✝¹)

m✝: Meas

ms'✝: MeasureSet

m'✝: Meas

h_taint✝: MeasureSet.taint ms'✝ = MeasureSet.tainted m'✝

h_right✝: Resolve F d₂ m✝.last i ms'✝

h_left✝: Resolve F d₁ c i (MeasureSet.tainted m✝)

concat_taintMeasureSet.tainted (Meas.concat F m✝¹ m'✝¹) = MeasureSet.tainted (Meas.concat F m✝ m'✝)
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

d₁, d₂: Doc

m✝: Meas

ms'✝: MeasureSet

m'✝: Meas

h_taint₁: MeasureSet.taint ms'✝ = MeasureSet.tainted m'✝

h_right₁: Resolve F d₂ m✝.last i ms'✝

h_left₁: Resolve F d₁ c i (MeasureSet.tainted m✝)

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h_left✝: Resolve F d₁ c i (MeasureSet.set ms✝ h_non_empty✝)

h✝: ResolveConcat F ms✝ d₂ i ms₂

concat_setMeasureSet.tainted (Meas.concat F m✝ m'✝) = ms₂
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

d₁, d₂: Doc

h₂: Resolve F (Doc.concat d₁ d₂) c i ms₂

m✝: Meas

ms'✝: MeasureSet

m'✝: Meas

h_taint₁: MeasureSet.taint ms'✝ = MeasureSet.tainted m'✝

h_right₁: Resolve F d₂ m✝.last i ms'✝

h_left₁: Resolve F d₁ c i (MeasureSet.tainted m✝)

MeasureSet.tainted (Meas.concat F m✝ m'✝) = ms₂case concat_taint h_taint₂: MeasureSet.taint ms'✝ = MeasureSet.tainted m'✝
h_taint₂ h_right₂: Resolve F d₂ m✝.last i ms'✝
h_right₂ h_left₂: Resolve F d₁ c i (MeasureSet.tainted m✝)
h_left₂ => 
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d₁, d₂: Doc

m✝¹: Meas

ms'✝¹: MeasureSet

m'✝¹: Meas

h_taint₁: MeasureSet.taint ms'✝¹ = MeasureSet.tainted m'✝¹

h_right₁: Resolve F d₂ m✝¹.last i ms'✝¹

h_left₁: Resolve F d₁ c i (MeasureSet.tainted m✝¹)

m✝: Meas

ms'✝: MeasureSet

m'✝: Meas

h_taint₂: MeasureSet.taint ms'✝ = MeasureSet.tainted m'✝

h_right₂: Resolve F d₂ m✝.last i ms'✝

h_left₂: Resolve F d₁ c i (MeasureSet.tainted m✝)

MeasureSet.tainted (Meas.concat F m✝¹ m'✝¹) = MeasureSet.tainted (Meas.concat F m✝ m'✝)cases Resolve_deterministic: ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {ms₁ ms₂ : MeasureSet},
  Resolve F d c i ms₁ → Resolve F d c i ms₂ → ms₁ = ms₂
Resolve_deterministic h_left₁: Resolve F d₁ c i (MeasureSet.tainted m✝¹)
h_left₁ h_left₂: Resolve F d₁ c i (MeasureSet.tainted m✝)
h_left₂α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d₁, d₂: Doc

m✝: Meas

ms'✝¹: MeasureSet

m'✝¹: Meas

h_taint₁: MeasureSet.taint ms'✝¹ = MeasureSet.tainted m'✝¹

h_right₁: Resolve F d₂ m✝.last i ms'✝¹

h_left₁: Resolve F d₁ c i (MeasureSet.tainted m✝)

ms'✝: MeasureSet

m'✝: Meas

h_taint₂: MeasureSet.taint ms'✝ = MeasureSet.tainted m'✝

h_right₂: Resolve F d₂ m✝.last i ms'✝

h_left₂: Resolve F d₁ c i (MeasureSet.tainted m✝)

reflMeasureSet.tainted (Meas.concat F m✝ m'✝¹) = MeasureSet.tainted (Meas.concat F m✝ m'✝)
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d₁, d₂: Doc

m✝¹: Meas

ms'✝¹: MeasureSet

m'✝¹: Meas

h_taint₁: MeasureSet.taint ms'✝¹ = MeasureSet.tainted m'✝¹

h_right₁: Resolve F d₂ m✝¹.last i ms'✝¹

h_left₁: Resolve F d₁ c i (MeasureSet.tainted m✝¹)

m✝: Meas

ms'✝: MeasureSet

m'✝: Meas

h_taint₂: MeasureSet.taint ms'✝ = MeasureSet.tainted m'✝

h_right₂: Resolve F d₂ m✝.last i ms'✝

h_left₂: Resolve F d₁ c i (MeasureSet.tainted m✝)

MeasureSet.tainted (Meas.concat F m✝¹ m'✝¹) = MeasureSet.tainted (Meas.concat F m✝ m'✝)cases Resolve_deterministic: ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {ms₁ ms₂ : MeasureSet},
  Resolve F d c i ms₁ → Resolve F d c i ms₂ → ms₁ = ms₂
Resolve_deterministic h_right₁: Resolve F d₂ m✝.last i ms'✝¹
h_right₁ h_right₂: Resolve F d₂ m✝.last i ms'✝
h_right₂α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d₁, d₂: Doc

m✝: Meas

ms'✝: MeasureSet

m'✝¹: Meas

h_taint₁: MeasureSet.taint ms'✝ = MeasureSet.tainted m'✝¹

h_right₁: Resolve F d₂ m✝.last i ms'✝

h_left₁: Resolve F d₁ c i (MeasureSet.tainted m✝)

m'✝: Meas

h_left₂: Resolve F d₁ c i (MeasureSet.tainted m✝)

h_taint₂: MeasureSet.taint ms'✝ = MeasureSet.tainted m'✝

h_right₂: Resolve F d₂ m✝.last i ms'✝

refl.reflMeasureSet.tainted (Meas.concat F m✝ m'✝¹) = MeasureSet.tainted (Meas.concat F m✝ m'✝)
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d₁, d₂: Doc

m✝¹: Meas

ms'✝¹: MeasureSet

m'✝¹: Meas

h_taint₁: MeasureSet.taint ms'✝¹ = MeasureSet.tainted m'✝¹

h_right₁: Resolve F d₂ m✝¹.last i ms'✝¹

h_left₁: Resolve F d₁ c i (MeasureSet.tainted m✝¹)

m✝: Meas

ms'✝: MeasureSet

m'✝: Meas

h_taint₂: MeasureSet.taint ms'✝ = MeasureSet.tainted m'✝

h_right₂: Resolve F d₂ m✝.last i ms'✝

h_left₂: Resolve F d₁ c i (MeasureSet.tainted m✝)

MeasureSet.tainted (Meas.concat F m✝¹ m'✝¹) = MeasureSet.tainted (Meas.concat F m✝ m'✝)simp [h_taint₁: MeasureSet.taint ms'✝ = MeasureSet.tainted m'✝¹
h_taint₁] at h_taint₂: MeasureSet.taint ms'✝ = MeasureSet.tainted m'✝
h_taint₂α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d₁, d₂: Doc

m✝: Meas

ms'✝: MeasureSet

m'✝¹: Meas

h_taint₁: MeasureSet.taint ms'✝ = MeasureSet.tainted m'✝¹

h_right₁: Resolve F d₂ m✝.last i ms'✝

h_left₁: Resolve F d₁ c i (MeasureSet.tainted m✝)

m'✝: Meas

h_left₂: Resolve F d₁ c i (MeasureSet.tainted m✝)

h_right₂: Resolve F d₂ m✝.last i ms'✝

h_taint₂: m'✝¹ = m'✝

refl.reflMeasureSet.tainted (Meas.concat F m✝ m'✝¹) = MeasureSet.tainted (Meas.concat F m✝ m'✝)
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d₁, d₂: Doc

m✝¹: Meas

ms'✝¹: MeasureSet

m'✝¹: Meas

h_taint₁: MeasureSet.taint ms'✝¹ = MeasureSet.tainted m'✝¹

h_right₁: Resolve F d₂ m✝¹.last i ms'✝¹

h_left₁: Resolve F d₁ c i (MeasureSet.tainted m✝¹)

m✝: Meas

ms'✝: MeasureSet

m'✝: Meas

h_taint₂: MeasureSet.taint ms'✝ = MeasureSet.tainted m'✝

h_right₂: Resolve F d₂ m✝.last i ms'✝

h_left₂: Resolve F d₁ c i (MeasureSet.tainted m✝)

MeasureSet.tainted (Meas.concat F m✝¹ m'✝¹) = MeasureSet.tainted (Meas.concat F m✝ m'✝)simp [*]
Goals accomplished! 🐙
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

d₁, d₂: Doc

h₂: Resolve F (Doc.concat d₁ d₂) c i ms₂

m✝: Meas

ms'✝: MeasureSet

m'✝: Meas

h_taint₁: MeasureSet.taint ms'✝ = MeasureSet.tainted m'✝

h_right₁: Resolve F d₂ m✝.last i ms'✝

h_left₁: Resolve F d₁ c i (MeasureSet.tainted m✝)

MeasureSet.tainted (Meas.concat F m✝ m'✝) = ms₂case concat_set h_left₂: Resolve F d₁ c i (MeasureSet.set ms✝ h_non_empty✝)
h_left₂ _ => α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₂: MeasureSet

d₁, d₂: Doc

m✝: Meas

ms'✝: MeasureSet

m'✝: Meas

h_taint₁: MeasureSet.taint ms'✝ = MeasureSet.tainted m'✝

h_right₁: Resolve F d₂ m✝.last i ms'✝

h_left₁: Resolve F d₁ c i (MeasureSet.tainted m✝)

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h_left₂: Resolve F d₁ c i (MeasureSet.set ms✝ h_non_empty✝)

h✝: ResolveConcat F ms✝ d₂ i ms₂

MeasureSet.tainted (Meas.concat F m✝ m'✝) = ms₂cases Resolve_deterministic: ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {ms₁ ms₂ : MeasureSet},
  Resolve F d c i ms₁ → Resolve F d c i ms₂ → ms₁ = ms₂
Resolve_deterministic h_left₁: Resolve F d₁ c i (MeasureSet.tainted m✝)
h_left₁ h_left₂: Resolve F d₁ c i (MeasureSet.set ms✝ h_non_empty✝)
h_left₂
Goals accomplished! 🐙
      α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

d₁, d₂: Doc

h₁: Resolve F (Doc.concat d₁ d₂) c i ms₁

h₂: Resolve F (Doc.concat d₁ d₂) c i ms₂

ms₁ = ms₂case concat_set h_left₁: Resolve F d₁ c i (MeasureSet.set ms✝ h_non_empty✝)
h_left₁ h_right₁: ResolveConcat F ms✝ d₂ i ms₁
h_right₁ =>
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

d₁, d₂: Doc

h₂: Resolve F (Doc.concat d₁ d₂) c i ms₂

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h_left₁: Resolve F d₁ c i (MeasureSet.set ms✝ h_non_empty✝)

h_right₁: ResolveConcat F ms✝ d₂ i ms₁

ms₁ = ms₂cases h₂: Resolve F (Doc.concat d₁ d₂) c i ms₂
h₂α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁: MeasureSet

d₁, d₂: Doc

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h_left₁: Resolve F d₁ c i (MeasureSet.set ms✝ h_non_empty✝)

h_right₁: ResolveConcat F ms✝ d₂ i ms₁

m✝: Meas

ms'✝: MeasureSet

m'✝: Meas

h_taint✝: MeasureSet.taint ms'✝ = MeasureSet.tainted m'✝

h_right✝: Resolve F d₂ m✝.last i ms'✝

h_left✝: Resolve F d₁ c i (MeasureSet.tainted m✝)

concat_taintms₁ = MeasureSet.tainted (Meas.concat F m✝ m'✝)
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

d₁, d₂: Doc

ms✝¹: List Meas

h_non_empty✝¹: ms✝¹ ≠ []

h_left₁: Resolve F d₁ c i (MeasureSet.set ms✝¹ h_non_empty✝¹)

h_right₁: ResolveConcat F ms✝¹ d₂ i ms₁

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h_left✝: Resolve F d₁ c i (MeasureSet.set ms✝ h_non_empty✝)

h✝: ResolveConcat F ms✝ d₂ i ms₂

concat_setms₁ = ms₂ 
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

d₁, d₂: Doc

h₂: Resolve F (Doc.concat d₁ d₂) c i ms₂

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h_left₁: Resolve F d₁ c i (MeasureSet.set ms✝ h_non_empty✝)

h_right₁: ResolveConcat F ms✝ d₂ i ms₁

ms₁ = ms₂case concat_taint h_taint₂: MeasureSet.taint ms'✝ = MeasureSet.tainted m'✝
h_taint₂ h_right₂: Resolve F d₂ m✝.last i ms'✝
h_right₂ h_left₂: Resolve F d₁ c i (MeasureSet.tainted m✝)
h_left₂ => α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁: MeasureSet

d₁, d₂: Doc

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h_left₁: Resolve F d₁ c i (MeasureSet.set ms✝ h_non_empty✝)

h_right₁: ResolveConcat F ms✝ d₂ i ms₁

m✝: Meas

ms'✝: MeasureSet

m'✝: Meas

h_taint₂: MeasureSet.taint ms'✝ = MeasureSet.tainted m'✝

h_right₂: Resolve F d₂ m✝.last i ms'✝

h_left₂: Resolve F d₁ c i (MeasureSet.tainted m✝)

ms₁ = MeasureSet.tainted (Meas.concat F m✝ m'✝)cases Resolve_deterministic: ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {ms₁ ms₂ : MeasureSet},
  Resolve F d c i ms₁ → Resolve F d c i ms₂ → ms₁ = ms₂
Resolve_deterministic h_left₁: Resolve F d₁ c i (MeasureSet.set ms✝ h_non_empty✝)
h_left₁ h_left₂: Resolve F d₁ c i (MeasureSet.tainted m✝)
h_left₂
Goals accomplished! 🐙
        α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

d₁, d₂: Doc

h₂: Resolve F (Doc.concat d₁ d₂) c i ms₂

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h_left₁: Resolve F d₁ c i (MeasureSet.set ms✝ h_non_empty✝)

h_right₁: ResolveConcat F ms✝ d₂ i ms₁

ms₁ = ms₂case concat_set h_left₂: Resolve F d₁ c i (MeasureSet.set ms✝ h_non_empty✝)
h_left₂ h_right₂: ResolveConcat F ms✝ d₂ i ms₂
h_right₂ => 
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

d₁, d₂: Doc

ms✝¹: List Meas

h_non_empty✝¹: ms✝¹ ≠ []

h_left₁: Resolve F d₁ c i (MeasureSet.set ms✝¹ h_non_empty✝¹)

h_right₁: ResolveConcat F ms✝¹ d₂ i ms₁

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h_left₂: Resolve F d₁ c i (MeasureSet.set ms✝ h_non_empty✝)

h_right₂: ResolveConcat F ms✝ d₂ i ms₂

ms₁ = ms₂cases Resolve_deterministic: ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {ms₁ ms₂ : MeasureSet},
  Resolve F d c i ms₁ → Resolve F d c i ms₂ → ms₁ = ms₂
Resolve_deterministic h_left₁: Resolve F d₁ c i (MeasureSet.set ms✝¹ h_non_empty✝¹)
h_left₁ h_left₂: Resolve F d₁ c i (MeasureSet.set ms✝ h_non_empty✝)
h_left₂α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

d₁, d₂: Doc

ms✝: List Meas

h_non_empty✝¹: ms✝ ≠ []

h_left₁: Resolve F d₁ c i (MeasureSet.set ms✝ h_non_empty✝¹)

h_right₁: ResolveConcat F ms✝ d₂ i ms₁

h_non_empty✝: ms✝ ≠ []

h_left₂: Resolve F d₁ c i (MeasureSet.set ms✝ h_non_empty✝)

h_right₂: ResolveConcat F ms✝ d₂ i ms₂

reflms₁ = ms₂
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

d₁, d₂: Doc

ms✝¹: List Meas

h_non_empty✝¹: ms✝¹ ≠ []

h_left₁: Resolve F d₁ c i (MeasureSet.set ms✝¹ h_non_empty✝¹)

h_right₁: ResolveConcat F ms✝¹ d₂ i ms₁

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h_left₂: Resolve F d₁ c i (MeasureSet.set ms✝ h_non_empty✝)

h_right₂: ResolveConcat F ms✝ d₂ i ms₂

ms₁ = ms₂cases ResolveConcat_deterministic: ∀ {α : Type} {F : Factory α} {d : Doc} {i : ℕ} {msr₁ msr₂ : MeasureSet} {ms : List Meas},
  ResolveConcat F ms d i msr₁ → ResolveConcat F ms d i msr₂ → msr₁ = msr₂
ResolveConcat_deterministic h_right₁: ResolveConcat F ms✝ d₂ i ms₁
h_right₁ h_right₂: ResolveConcat F ms✝ d₂ i ms₂
h_right₂α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁: MeasureSet

d₁, d₂: Doc

ms✝: List Meas

h_non_empty✝¹: ms✝ ≠ []

h_left₁: Resolve F d₁ c i (MeasureSet.set ms✝ h_non_empty✝¹)

h_right₁: ResolveConcat F ms✝ d₂ i ms₁

h_non_empty✝: ms✝ ≠ []

h_left₂: Resolve F d₁ c i (MeasureSet.set ms✝ h_non_empty✝)

h_right₂: ResolveConcat F ms✝ d₂ i ms₁

refl.reflms₁ = ms₁ 
          α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms₁, ms₂: MeasureSet

d₁, d₂: Doc

ms✝¹: List Meas

h_non_empty✝¹: ms✝¹ ≠ []

h_left₁: Resolve F d₁ c i (MeasureSet.set ms✝¹ h_non_empty✝¹)

h_right₁: ResolveConcat F ms✝¹ d₂ i ms₁

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h_left₂: Resolve F d₁ c i (MeasureSet.set ms✝ h_non_empty✝)

h_right₂: ResolveConcat F ms✝ d₂ i ms₂

ms₁ = ms₂simp
Goals accomplished! 🐙         
  }
Goals accomplished! 🐙

  theorem ResolveConcatOne_deterministic: ∀ {α : Type} {F : Factory α} {d : Doc} {m : Meas} {i : ℕ} {msr₁ msr₂ : MeasureSet},
  ResolveConcatOne F d m i msr₁ → ResolveConcatOne F d m i msr₂ → msr₁ = msr₂
ResolveConcatOne_deterministic 
      (h₁: ResolveConcatOne F d m i msr₁
h₁ : ResolveConcatOne: {α : Type} → Factory α → Doc → Meas → ℕ → MeasureSet → Prop
ResolveConcatOne F: ?m.55
F d: ?m.62
d m: ?m.68
m i: ?m.75
i msr₁: ?m.81
msr₁)
      (h₂: ResolveConcatOne F d m i msr₂
h₂ : ResolveConcatOne: {α : Type} → Factory α → Doc → Meas → ℕ → MeasureSet → Prop
ResolveConcatOne F: ?m.55
F d: ?m.62
d m: ?m.68
m i: ?m.75
i msr₂: ?m.91
msr₂) : 
      msr₁: ?m.81
msr₁ = msr₂: ?m.91
msr₂ := by
Goals accomplished! 🐙
    α✝: Type

F: Factory α✝

d: Doc

m: Meas

i: ℕ

msr₁, msr₂: MeasureSet

h₁: ResolveConcatOne F d m i msr₁

h₂: ResolveConcatOne F d m i msr₂

msr₁ = msr₂cases h₁: ResolveConcatOne F d m i msr₁
h₁α✝: Type

F: Factory α✝

d: Doc

m: Meas

i: ℕ

msr₂: MeasureSet

h₂: ResolveConcatOne F d m i msr₂

m'✝: Meas

h✝: Resolve F d m.last i (MeasureSet.tainted m'✝)

taintedMeasureSet.tainted (Meas.concat F m m'✝) = msr₂
α✝: Type

F: Factory α✝

d: Doc

m: Meas

i: ℕ

msr₂: MeasureSet

h₂: ResolveConcatOne F d m i msr₂

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h✝: Resolve F d m.last i (MeasureSet.set ms✝ h_non_empty✝)

setMeasureSet.set (dedup F (List.map (fun m' => Meas.concat F m m') ms✝))
    (_ : dedup F (List.map (fun m' => Meas.concat F m m') ms✝) ≠ []) =   msr₂
    α✝: Type

F: Factory α✝

d: Doc

m: Meas

i: ℕ

msr₁, msr₂: MeasureSet

h₁: ResolveConcatOne F d m i msr₁

h₂: ResolveConcatOne F d m i msr₂

msr₁ = msr₂case tainted h₁: Resolve F d m.last i (MeasureSet.tainted m'✝)
h₁ => 
      α✝: Type

F: Factory α✝

d: Doc

m: Meas

i: ℕ

msr₂: MeasureSet

h₂: ResolveConcatOne F d m i msr₂

m'✝: Meas

h₁: Resolve F d m.last i (MeasureSet.tainted m'✝)

MeasureSet.tainted (Meas.concat F m m'✝) = msr₂cases h₂: ResolveConcatOne F d m i msr₂
h₂α✝: Type

F: Factory α✝

d: Doc

m: Meas

i: ℕ

m'✝¹: Meas

h₁: Resolve F d m.last i (MeasureSet.tainted m'✝¹)

m'✝: Meas

h✝: Resolve F d m.last i (MeasureSet.tainted m'✝)

taintedMeasureSet.tainted (Meas.concat F m m'✝¹) = MeasureSet.tainted (Meas.concat F m m'✝)
α✝: Type

F: Factory α✝

d: Doc

m: Meas

i: ℕ

m'✝: Meas

h₁: Resolve F d m.last i (MeasureSet.tainted m'✝)

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h✝: Resolve F d m.last i (MeasureSet.set ms✝ h_non_empty✝)

setMeasureSet.tainted (Meas.concat F m m'✝) =   MeasureSet.set (dedup F (List.map (fun m' => Meas.concat F m m') ms✝))
    (_ : dedup F (List.map (fun m' => Meas.concat F m m') ms✝) ≠ [])
      α✝: Type

F: Factory α✝

d: Doc

m: Meas

i: ℕ

msr₂: MeasureSet

h₂: ResolveConcatOne F d m i msr₂

m'✝: Meas

h₁: Resolve F d m.last i (MeasureSet.tainted m'✝)

MeasureSet.tainted (Meas.concat F m m'✝) = msr₂case tainted h₂: Resolve F d m.last i (MeasureSet.tainted m'✝)
h₂ => 
        α✝: Type

F: Factory α✝

d: Doc

m: Meas

i: ℕ

m'✝¹: Meas

h₁: Resolve F d m.last i (MeasureSet.tainted m'✝¹)

m'✝: Meas

h₂: Resolve F d m.last i (MeasureSet.tainted m'✝)

MeasureSet.tainted (Meas.concat F m m'✝¹) = MeasureSet.tainted (Meas.concat F m m'✝)cases Resolve_deterministic: ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {ms₁ ms₂ : MeasureSet},
  Resolve F d c i ms₁ → Resolve F d c i ms₂ → ms₁ = ms₂
Resolve_deterministic h₁: Resolve F d m.last i (MeasureSet.tainted m'✝¹)
h₁ h₂: Resolve F d m.last i (MeasureSet.tainted m'✝)
h₂α✝: Type

F: Factory α✝

d: Doc

m: Meas

i: ℕ

m'✝: Meas

h₁, h₂: Resolve F d m.last i (MeasureSet.tainted m'✝)

reflMeasureSet.tainted (Meas.concat F m m'✝) = MeasureSet.tainted (Meas.concat F m m'✝)
        α✝: Type

F: Factory α✝

d: Doc

m: Meas

i: ℕ

m'✝¹: Meas

h₁: Resolve F d m.last i (MeasureSet.tainted m'✝¹)

m'✝: Meas

h₂: Resolve F d m.last i (MeasureSet.tainted m'✝)

MeasureSet.tainted (Meas.concat F m m'✝¹) = MeasureSet.tainted (Meas.concat F m m'✝)simp
Goals accomplished! 🐙
      α✝: Type

F: Factory α✝

d: Doc

m: Meas

i: ℕ

msr₂: MeasureSet

h₂: ResolveConcatOne F d m i msr₂

m'✝: Meas

h₁: Resolve F d m.last i (MeasureSet.tainted m'✝)

MeasureSet.tainted (Meas.concat F m m'✝) = msr₂case set h₂: Resolve F d m.last i (MeasureSet.set ms✝ h_non_empty✝)
h₂ => α✝: Type

F: Factory α✝

d: Doc

m: Meas

i: ℕ

m'✝: Meas

h₁: Resolve F d m.last i (MeasureSet.tainted m'✝)

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h₂: Resolve F d m.last i (MeasureSet.set ms✝ h_non_empty✝)

MeasureSet.tainted (Meas.concat F m m'✝) =   MeasureSet.set (dedup F (List.map (fun m' => Meas.concat F m m') ms✝))
    (_ : dedup F (List.map (fun m' => Meas.concat F m m') ms✝) ≠ [])cases Resolve_deterministic: ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {ms₁ ms₂ : MeasureSet},
  Resolve F d c i ms₁ → Resolve F d c i ms₂ → ms₁ = ms₂
Resolve_deterministic h₁: Resolve F d m.last i (MeasureSet.tainted m'✝)
h₁ h₂: Resolve F d m.last i (MeasureSet.set ms✝ h_non_empty✝)
h₂
Goals accomplished! 🐙
    α✝: Type

F: Factory α✝

d: Doc

m: Meas

i: ℕ

msr₁, msr₂: MeasureSet

h₁: ResolveConcatOne F d m i msr₁

h₂: ResolveConcatOne F d m i msr₂

msr₁ = msr₂case set h₁: Resolve F d m.last i (MeasureSet.set ms✝ h_non_empty✝)
h₁ => 
      α✝: Type

F: Factory α✝

d: Doc

m: Meas

i: ℕ

msr₂: MeasureSet

h₂: ResolveConcatOne F d m i msr₂

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h₁: Resolve F d m.last i (MeasureSet.set ms✝ h_non_empty✝)

MeasureSet.set (dedup F (List.map (fun m' => Meas.concat F m m') ms✝))
    (_ : dedup F (List.map (fun m' => Meas.concat F m m') ms✝) ≠ []) =   msr₂cases h₂: ResolveConcatOne F d m i msr₂
h₂α✝: Type

F: Factory α✝

d: Doc

m: Meas

i: ℕ

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h₁: Resolve F d m.last i (MeasureSet.set ms✝ h_non_empty✝)

m'✝: Meas

h✝: Resolve F d m.last i (MeasureSet.tainted m'✝)

taintedMeasureSet.set (dedup F (List.map (fun m' => Meas.concat F m m') ms✝))
    (_ : dedup F (List.map (fun m' => Meas.concat F m m') ms✝) ≠ []) =   MeasureSet.tainted (Meas.concat F m m'✝)
α✝: Type

F: Factory α✝

d: Doc

m: Meas

i: ℕ

ms✝¹: List Meas

h_non_empty✝¹: ms✝¹ ≠ []

h₁: Resolve F d m.last i (MeasureSet.set ms✝¹ h_non_empty✝¹)

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h✝: Resolve F d m.last i (MeasureSet.set ms✝ h_non_empty✝)

setMeasureSet.set (dedup F (List.map (fun m' => Meas.concat F m m') ms✝¹))
    (_ : dedup F (List.map (fun m' => Meas.concat F m m') ms✝¹) ≠ []) =   MeasureSet.set (dedup F (List.map (fun m' => Meas.concat F m m') ms✝))
    (_ : dedup F (List.map (fun m' => Meas.concat F m m') ms✝) ≠ [])
      α✝: Type

F: Factory α✝

d: Doc

m: Meas

i: ℕ

msr₂: MeasureSet

h₂: ResolveConcatOne F d m i msr₂

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h₁: Resolve F d m.last i (MeasureSet.set ms✝ h_non_empty✝)

MeasureSet.set (dedup F (List.map (fun m' => Meas.concat F m m') ms✝))
    (_ : dedup F (List.map (fun m' => Meas.concat F m m') ms✝) ≠ []) =   msr₂case tainted h₂: Resolve F d m.last i (MeasureSet.tainted m'✝)
h₂ => α✝: Type

F: Factory α✝

d: Doc

m: Meas

i: ℕ

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h₁: Resolve F d m.last i (MeasureSet.set ms✝ h_non_empty✝)

m'✝: Meas

h₂: Resolve F d m.last i (MeasureSet.tainted m'✝)

MeasureSet.set (dedup F (List.map (fun m' => Meas.concat F m m') ms✝))
    (_ : dedup F (List.map (fun m' => Meas.concat F m m') ms✝) ≠ []) =   MeasureSet.tainted (Meas.concat F m m'✝)cases Resolve_deterministic: ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {ms₁ ms₂ : MeasureSet},
  Resolve F d c i ms₁ → Resolve F d c i ms₂ → ms₁ = ms₂
Resolve_deterministic h₁: Resolve F d m.last i (MeasureSet.set ms✝ h_non_empty✝)
h₁ h₂: Resolve F d m.last i (MeasureSet.tainted m'✝)
h₂
Goals accomplished! 🐙
      α✝: Type

F: Factory α✝

d: Doc

m: Meas

i: ℕ

msr₂: MeasureSet

h₂: ResolveConcatOne F d m i msr₂

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h₁: Resolve F d m.last i (MeasureSet.set ms✝ h_non_empty✝)

MeasureSet.set (dedup F (List.map (fun m' => Meas.concat F m m') ms✝))
    (_ : dedup F (List.map (fun m' => Meas.concat F m m') ms✝) ≠ []) =   msr₂case set h₂: Resolve F d m.last i (MeasureSet.set ms✝ h_non_empty✝)
h₂ => 
        α✝: Type

F: Factory α✝

d: Doc

m: Meas

i: ℕ

ms✝¹: List Meas

h_non_empty✝¹: ms✝¹ ≠ []

h₁: Resolve F d m.last i (MeasureSet.set ms✝¹ h_non_empty✝¹)

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h₂: Resolve F d m.last i (MeasureSet.set ms✝ h_non_empty✝)

MeasureSet.set (dedup F (List.map (fun m' => Meas.concat F m m') ms✝¹))
    (_ : dedup F (List.map (fun m' => Meas.concat F m m') ms✝¹) ≠ []) =   MeasureSet.set (dedup F (List.map (fun m' => Meas.concat F m m') ms✝))
    (_ : dedup F (List.map (fun m' => Meas.concat F m m') ms✝) ≠ [])cases Resolve_deterministic: ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {ms₁ ms₂ : MeasureSet},
  Resolve F d c i ms₁ → Resolve F d c i ms₂ → ms₁ = ms₂
Resolve_deterministic h₁: Resolve F d m.last i (MeasureSet.set ms✝¹ h_non_empty✝¹)
h₁ h₂: Resolve F d m.last i (MeasureSet.set ms✝ h_non_empty✝)
h₂α✝: Type

F: Factory α✝

d: Doc

m: Meas

i: ℕ

ms✝: List Meas

h_non_empty✝¹: ms✝ ≠ []

h₁: Resolve F d m.last i (MeasureSet.set ms✝ h_non_empty✝¹)

h_non_empty✝: ms✝ ≠ []

h₂: Resolve F d m.last i (MeasureSet.set ms✝ h_non_empty✝)

reflMeasureSet.set (dedup F (List.map (fun m' => Meas.concat F m m') ms✝))
    (_ : dedup F (List.map (fun m' => Meas.concat F m m') ms✝) ≠ []) =   MeasureSet.set (dedup F (List.map (fun m' => Meas.concat F m m') ms✝))
    (_ : dedup F (List.map (fun m' => Meas.concat F m m') ms✝) ≠ [])
        α✝: Type

F: Factory α✝

d: Doc

m: Meas

i: ℕ

ms✝¹: List Meas

h_non_empty✝¹: ms✝¹ ≠ []

h₁: Resolve F d m.last i (MeasureSet.set ms✝¹ h_non_empty✝¹)

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h₂: Resolve F d m.last i (MeasureSet.set ms✝ h_non_empty✝)

MeasureSet.set (dedup F (List.map (fun m' => Meas.concat F m m') ms✝¹))
    (_ : dedup F (List.map (fun m' => Meas.concat F m m') ms✝¹) ≠ []) =   MeasureSet.set (dedup F (List.map (fun m' => Meas.concat F m m') ms✝))
    (_ : dedup F (List.map (fun m' => Meas.concat F m m') ms✝) ≠ [])simp
Goals accomplished! 🐙

  theorem ResolveConcat_deterministic: ∀ {α : Type} {F : Factory α} {d : Doc} {i : ℕ} {msr₁ msr₂ : MeasureSet} {ms : List Meas},
  ResolveConcat F ms d i msr₁ → ResolveConcat F ms d i msr₂ → msr₁ = msr₂
ResolveConcat_deterministic {ms: List Meas
ms : List: Type ?u.165 → Type ?u.165
List Meas: {α : Type} → Type
Meas}
      (h₁: ResolveConcat F ms d i msr₁
h₁ : ResolveConcat: {α : Type} → Factory α → List Meas → Doc → ℕ → MeasureSet → Prop
ResolveConcat F: ?m.111
F ms: List Meas
ms d: ?m.125
d i: ?m.136
i msr₁: ?m.147
msr₁)
      (h₂: ResolveConcat F ms d i msr₂
h₂ : ResolveConcat: {α : Type} → Factory α → List Meas → Doc → ℕ → MeasureSet → Prop
ResolveConcat F: ?m.111
F ms: List Meas
ms d: ?m.125
d i: ?m.136
i msr₂: ?m.162
msr₂) : 
      msr₁: ?m.147
msr₁ = msr₂: ?m.162
msr₂ := by
Goals accomplished! 🐙
    α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₁, msr₂: MeasureSet

ms: List Meas

h₁: ResolveConcat F ms d i msr₁

h₂: ResolveConcat F ms d i msr₂

msr₁ = msr₂cases h₁: ResolveConcat F ms d i msr₁
h₁α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₁, msr₂: MeasureSet

m✝: Meas

h₂: ResolveConcat F [m✝] d i msr₂

h_current✝: ResolveConcatOne F d m✝ i msr₁

onemsr₁ = msr₂
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₂: MeasureSet

ms✝: List Meas

msr✝: MeasureSet

m✝: Meas

msr'✝: MeasureSet

h₂: ResolveConcat F (m✝ :: ms✝) d i msr₂

h_rest✝: ResolveConcat F ms✝ d i msr✝

h_current✝: ResolveConcatOne F d m✝ i msr'✝

consMeasureSet.union F msr'✝ msr✝ = msr₂ 
    α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₁, msr₂: MeasureSet

ms: List Meas

h₁: ResolveConcat F ms d i msr₁

h₂: ResolveConcat F ms d i msr₂

msr₁ = msr₂case one => 
      α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₁, msr₂: MeasureSet

m✝: Meas

h₂: ResolveConcat F [m✝] d i msr₂

h_current✝: ResolveConcatOne F d m✝ i msr₁

msr₁ = msr₂dwi { α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₁, msr₂: MeasureSet

m✝: Meas

h₂: ResolveConcat F [m✝] d i msr₂

h_current✝: ResolveConcatOne F d m✝ i msr₁

msr₁ = msr₂cases h₂: ResolveConcat F [m✝] d i msr₂
h₂α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₁, msr₂: MeasureSet

m✝: Meas

h_current✝¹: ResolveConcatOne F d m✝ i msr₁

h_current✝: ResolveConcatOne F d m✝ i msr₂

onemsr₁ = msr₂
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₁: MeasureSet

m✝: Meas

h_current✝¹: ResolveConcatOne F d m✝ i msr₁

msr✝, msr'✝: MeasureSet

h_current✝: ResolveConcatOne F d m✝ i msr'✝

h_rest✝: ResolveConcat F [] d i msr✝

consmsr₁ = MeasureSet.union F msr'✝ msr✝ }α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₁, msr₂: MeasureSet

m✝: Meas

h_current✝¹: ResolveConcatOne F d m✝ i msr₁

h_current✝: ResolveConcatOne F d m✝ i msr₂

onemsr₁ = msr₂
      α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₁, msr₂: MeasureSet

m✝: Meas

h₂: ResolveConcat F [m✝] d i msr₂

h_current✝: ResolveConcatOne F d m✝ i msr₁

msr₁ = msr₂case one => α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₁, msr₂: MeasureSet

m✝: Meas

h_current✝¹: ResolveConcatOne F d m✝ i msr₁

h_current✝: ResolveConcatOne F d m✝ i msr₂

msr₁ = msr₂apply ResolveConcatOne_deterministic: ∀ {α : Type} {F : Factory α} {d : Doc} {m : Meas} {i : ℕ} {msr₁ msr₂ : MeasureSet},
  ResolveConcatOne F d m i msr₁ → ResolveConcatOne F d m i msr₂ → msr₁ = msr₂
ResolveConcatOne_deterministicα✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₁, msr₂: MeasureSet

m✝: Meas

h_current✝¹: ResolveConcatOne F d m✝ i msr₁

h_current✝: ResolveConcatOne F d m✝ i msr₂

h₁ResolveConcatOne ?F ?d ?m ?i msr₁
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₁, msr₂: MeasureSet

m✝: Meas

h_current✝¹: ResolveConcatOne F d m✝ i msr₁

h_current✝: ResolveConcatOne F d m✝ i msr₂

h₂ResolveConcatOne ?F ?d ?m ?i msr₂
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₁, msr₂: MeasureSet

m✝: Meas

h_current✝¹: ResolveConcatOne F d m✝ i msr₁

h_current✝: ResolveConcatOne F d m✝ i msr₂

FFactory α✝
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₁, msr₂: MeasureSet

m✝: Meas

h_current✝¹: ResolveConcatOne F d m✝ i msr₁

h_current✝: ResolveConcatOne F d m✝ i msr₂

dDoc
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₁, msr₂: MeasureSet

m✝: Meas

h_current✝¹: ResolveConcatOne F d m✝ i msr₁

h_current✝: ResolveConcatOne F d m✝ i msr₂

mMeas
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₁, msr₂: MeasureSet

m✝: Meas

h_current✝¹: ResolveConcatOne F d m✝ i msr₁

h_current✝: ResolveConcatOne F d m✝ i msr₂

iℕ α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₁, msr₂: MeasureSet

m✝: Meas

h_current✝¹: ResolveConcatOne F d m✝ i msr₁

h_current✝: ResolveConcatOne F d m✝ i msr₂

msr₁ = msr₂<;>α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₁, msr₂: MeasureSet

m✝: Meas

h_current✝¹: ResolveConcatOne F d m✝ i msr₁

h_current✝: ResolveConcatOne F d m✝ i msr₂

h₁ResolveConcatOne ?F ?d ?m ?i msr₁
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₁, msr₂: MeasureSet

m✝: Meas

h_current✝¹: ResolveConcatOne F d m✝ i msr₁

h_current✝: ResolveConcatOne F d m✝ i msr₂

h₂ResolveConcatOne ?F ?d ?m ?i msr₂
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₁, msr₂: MeasureSet

m✝: Meas

h_current✝¹: ResolveConcatOne F d m✝ i msr₁

h_current✝: ResolveConcatOne F d m✝ i msr₂

FFactory α✝
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₁, msr₂: MeasureSet

m✝: Meas

h_current✝¹: ResolveConcatOne F d m✝ i msr₁

h_current✝: ResolveConcatOne F d m✝ i msr₂

dDoc
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₁, msr₂: MeasureSet

m✝: Meas

h_current✝¹: ResolveConcatOne F d m✝ i msr₁

h_current✝: ResolveConcatOne F d m✝ i msr₂

mMeas
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₁, msr₂: MeasureSet

m✝: Meas

h_current✝¹: ResolveConcatOne F d m✝ i msr₁

h_current✝: ResolveConcatOne F d m✝ i msr₂

iℕ α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₁, msr₂: MeasureSet

m✝: Meas

h_current✝¹: ResolveConcatOne F d m✝ i msr₁

h_current✝: ResolveConcatOne F d m✝ i msr₂

msr₁ = msr₂assumption
Goals accomplished! 🐙
    α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₁, msr₂: MeasureSet

ms: List Meas

h₁: ResolveConcat F ms d i msr₁

h₂: ResolveConcat F ms d i msr₂

msr₁ = msr₂case cons h_rest₁: ResolveConcat F ms✝ d i msr✝
h_rest₁ h_current₁: ResolveConcatOne F d m✝ i msr'✝
h_current₁ => 
      α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₂: MeasureSet

ms✝: List Meas

msr✝: MeasureSet

m✝: Meas

msr'✝: MeasureSet

h₂: ResolveConcat F (m✝ :: ms✝) d i msr₂

h_rest₁: ResolveConcat F ms✝ d i msr✝

h_current₁: ResolveConcatOne F d m✝ i msr'✝

MeasureSet.union F msr'✝ msr✝ = msr₂dwi { α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₂: MeasureSet

ms✝: List Meas

msr✝: MeasureSet

m✝: Meas

msr'✝: MeasureSet

h₂: ResolveConcat F (m✝ :: ms✝) d i msr₂

h_rest₁: ResolveConcat F ms✝ d i msr✝

h_current₁: ResolveConcatOne F d m✝ i msr'✝

MeasureSet.union F msr'✝ msr✝ = msr₂cases h₂: ResolveConcat F (m✝ :: ms✝) d i msr₂
h₂α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₂, msr✝: MeasureSet

m✝: Meas

msr'✝: MeasureSet

h_current₁: ResolveConcatOne F d m✝ i msr'✝

h_rest₁: ResolveConcat F [] d i msr✝

h_current✝: ResolveConcatOne F d m✝ i msr₂

oneMeasureSet.union F msr'✝ msr✝ = msr₂
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

ms✝: List Meas

msr✝¹: MeasureSet

m✝: Meas

msr'✝¹: MeasureSet

h_rest₁: ResolveConcat F ms✝ d i msr✝¹

h_current₁: ResolveConcatOne F d m✝ i msr'✝¹

msr✝, msr'✝: MeasureSet

h_current✝: ResolveConcatOne F d m✝ i msr'✝

h_rest✝: ResolveConcat F ms✝ d i msr✝

consMeasureSet.union F msr'✝¹ msr✝¹ = MeasureSet.union F msr'✝ msr✝ }α✝: Type

F: Factory α✝

d: Doc

i: ℕ

ms✝: List Meas

msr✝¹: MeasureSet

m✝: Meas

msr'✝¹: MeasureSet

h_rest₁: ResolveConcat F ms✝ d i msr✝¹

h_current₁: ResolveConcatOne F d m✝ i msr'✝¹

msr✝, msr'✝: MeasureSet

h_current✝: ResolveConcatOne F d m✝ i msr'✝

h_rest✝: ResolveConcat F ms✝ d i msr✝

consMeasureSet.union F msr'✝¹ msr✝¹ = MeasureSet.union F msr'✝ msr✝ 
      α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr₂: MeasureSet

ms✝: List Meas

msr✝: MeasureSet

m✝: Meas

msr'✝: MeasureSet

h₂: ResolveConcat F (m✝ :: ms✝) d i msr₂

h_rest₁: ResolveConcat F ms✝ d i msr✝

h_current₁: ResolveConcatOne F d m✝ i msr'✝

MeasureSet.union F msr'✝ msr✝ = msr₂case cons h_current₂: ResolveConcatOne F d m✝ i msr'✝
h_current₂ h_rest₂: ResolveConcat F ms✝ d i msr✝
h_rest₂ => 
        α✝: Type

F: Factory α✝

d: Doc

i: ℕ

ms✝: List Meas

msr✝¹: MeasureSet

m✝: Meas

msr'✝¹: MeasureSet

h_rest₁: ResolveConcat F ms✝ d i msr✝¹

h_current₁: ResolveConcatOne F d m✝ i msr'✝¹

msr✝, msr'✝: MeasureSet

h_current₂: ResolveConcatOne F d m✝ i msr'✝

h_rest₂: ResolveConcat F ms✝ d i msr✝

MeasureSet.union F msr'✝¹ msr✝¹ = MeasureSet.union F msr'✝ msr✝cases ResolveConcatOne_deterministic: ∀ {α : Type} {F : Factory α} {d : Doc} {m : Meas} {i : ℕ} {msr₁ msr₂ : MeasureSet},
  ResolveConcatOne F d m i msr₁ → ResolveConcatOne F d m i msr₂ → msr₁ = msr₂
ResolveConcatOne_deterministic h_current₁: ResolveConcatOne F d m✝ i msr'✝¹
h_current₁ h_current₂: ResolveConcatOne F d m✝ i msr'✝
h_current₂α✝: Type

F: Factory α✝

d: Doc

i: ℕ

ms✝: List Meas

msr✝¹: MeasureSet

m✝: Meas

msr'✝: MeasureSet

h_rest₁: ResolveConcat F ms✝ d i msr✝¹

h_current₁: ResolveConcatOne F d m✝ i msr'✝

msr✝: MeasureSet

h_rest₂: ResolveConcat F ms✝ d i msr✝

h_current₂: ResolveConcatOne F d m✝ i msr'✝

reflMeasureSet.union F msr'✝ msr✝¹ = MeasureSet.union F msr'✝ msr✝
        α✝: Type

F: Factory α✝

d: Doc

i: ℕ

ms✝: List Meas

msr✝¹: MeasureSet

m✝: Meas

msr'✝¹: MeasureSet

h_rest₁: ResolveConcat F ms✝ d i msr✝¹

h_current₁: ResolveConcatOne F d m✝ i msr'✝¹

msr✝, msr'✝: MeasureSet

h_current₂: ResolveConcatOne F d m✝ i msr'✝

h_rest₂: ResolveConcat F ms✝ d i msr✝

MeasureSet.union F msr'✝¹ msr✝¹ = MeasureSet.union F msr'✝ msr✝cases ResolveConcat_deterministic: ∀ {α : Type} {F : Factory α} {d : Doc} {i : ℕ} {msr₁ msr₂ : MeasureSet} {ms : List Meas},
  ResolveConcat F ms d i msr₁ → ResolveConcat F ms d i msr₂ → msr₁ = msr₂
ResolveConcat_deterministic h_rest₁: ResolveConcat F ms✝ d i msr✝¹
h_rest₁ h_rest₂: ResolveConcat F ms✝ d i msr✝
h_rest₂α✝: Type

F: Factory α✝

d: Doc

i: ℕ

ms✝: List Meas

msr✝: MeasureSet

m✝: Meas

msr'✝: MeasureSet

h_rest₁: ResolveConcat F ms✝ d i msr✝

h_current₁, h_current₂: ResolveConcatOne F d m✝ i msr'✝

h_rest₂: ResolveConcat F ms✝ d i msr✝

refl.reflMeasureSet.union F msr'✝ msr✝ = MeasureSet.union F msr'✝ msr✝
        α✝: Type

F: Factory α✝

d: Doc

i: ℕ

ms✝: List Meas

msr✝¹: MeasureSet

m✝: Meas

msr'✝¹: MeasureSet

h_rest₁: ResolveConcat F ms✝ d i msr✝¹

h_current₁: ResolveConcatOne F d m✝ i msr'✝¹

msr✝, msr'✝: MeasureSet

h_current₂: ResolveConcatOne F d m✝ i msr'✝

h_rest₂: ResolveConcat F ms✝ d i msr✝

MeasureSet.union F msr'✝¹ msr✝¹ = MeasureSet.union F msr'✝ msr✝simp
Goals accomplished! 🐙
end
termination_by 
  ResolveConcatOne_deterministic => (d: Doc
d.size: Doc → ℕ
size, 1: ?m.51073
1, 0: ?m.51080
0)
  ResolveConcat_deterministic => (d: Doc
d.size: Doc → ℕ
size, 2: ?m.50895
2, ms: List Meas
ms.length: {α : Type ?u.50904} → List α → ℕ
length)
  Resolve_deterministic => (d: Doc
d.size: Doc → ℕ
size, 0: ?m.50668
0, 0: ?m.50679
0)