Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
import Pretty.Claims.MeasRender

/--
Measure computation at higher column position or indentation level 
is worse
-/
lemma 
MeasRender_dom_monotonic: ∀ {α : Type} {d : Doc} {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas} {F : Factory α}, MeasRender F d c i m₁MeasRender F d c' i' m₂c c'i i'dominates F m₁ m₂ = true
MeasRender_dom_monotonic
{
F: Factory α
F
:
Factory: TypeType
Factory
α: ?m.3
α
} (
h: MeasRender F d c i m₁
h
:
MeasRender: {α : Type} → Factory αDocMeasProp
MeasRender
F: Factory α
F
d: ?m.11
d
c: ?m.18
c
i: ?m.25
i
m₁: ?m.32
m₁
) (
h': MeasRender F d c' i' m₂
h'
:
MeasRender: {α : Type} → Factory αDocMeasProp
MeasRender
F: Factory α
F
d: ?m.11
d
c': ?m.43
c'
i': ?m.53
i'
m₂: ?m.63
m₂
) (
h_c: c c'
h_c
:
c: ?m.18
c
c': ?m.43
c'
) (
h_i: i i'
h_i
:
i: ?m.25
i
i': ?m.53
i'
) :
dominates: {α : Type} → Factory αMeasMeasBool
dominates
F: Factory α
F
m₁: ?m.32
m₁
m₂: ?m.63
m₂
:=

Goals accomplished! 🐙
α: Type

d: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

F: Factory α

h: MeasRender F d c i m₁

h': MeasRender F d c' i' m₂

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true
α: Type

d: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

F: Factory α

h: MeasRender F d c i m₁

h': MeasRender F d c' i' m₂

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true
α: Type

d: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

F: Factory α

h: MeasRender F d c i m₁

h': MeasRender F d c' i' m₂

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true
α: Type

F: Factory α

s✝: String

c, i:

m₁: Meas

c', i':

m₂: Meas

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

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

h_c: c c'

h_i: i i'


text
dominates F m₁ m₂ = true
α: Type

F: Factory α

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F Doc.nl c i m₁

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

h_c: c c'

h_i: i i'


nl
dominates F m₁ m₂ = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

d₁_ih✝: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

d₂_ih✝: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.concat d₁✝ d₂✝) c i m₁

h': MeasRender F (Doc.concat d₁✝ d₂✝) c' i' m₂

h_c: c c'

h_i: i i'


concat
dominates F m₁ m₂ = true
α: Type

F: Factory α

n✝:

d✝: Doc

d_ih✝: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.nest n✝ d✝) c i m₁

h': MeasRender F (Doc.nest n✝ d✝) c' i' m₂

h_c: c c'

h_i: i i'


nest
dominates F m₁ m₂ = true
α: Type

F: Factory α

d✝: Doc

d_ih✝: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.align d✝) c i m₁

h': MeasRender F (Doc.align d✝) c' i' m₂

h_c: c c'

h_i: i i'


align
dominates F m₁ m₂ = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

d₁_ih✝: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

d₂_ih✝: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.choice d₁✝ d₂✝) c i m₁

h': MeasRender F (Doc.choice d₁✝ d₂✝) c' i' m₂

h_c: c c'

h_i: i i'


choice
dominates F m₁ m₂ = true
α: Type

d: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

F: Factory α

h: MeasRender F d c i m₁

h': MeasRender F d c' i' m₂

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true
α: Type

F: Factory α

s✝: String

c, i:

m₁: Meas

c', i':

m₂: Meas

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

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

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true
α: Type

F: Factory α

s✝: String

c, i, c', i':

m₂: Meas

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

h_c: c c'

h_i: i i'


text
dominates F { last := c + String.length s✝, cost := Factory.text F c (String.length s✝), doc := Doc.text s✝, x := c + String.length s✝, y := i } m₂ = true
α: Type

F: Factory α

s✝: String

c, i:

m₁: Meas

c', i':

m₂: Meas

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

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

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true
α: Type

F: Factory α

s✝: String

c, i, c', i':

h_c: c c'

h_i: i i'


text.text
dominates F { last := c + String.length s✝, cost := Factory.text F c (String.length s✝), doc := Doc.text s✝, x := c + String.length s✝, y := i } { last := c' + String.length s✝, cost := Factory.text F c' (String.length s✝), doc := Doc.text s✝, x := c' + String.length s✝, y := i' } = true
α: Type

F: Factory α

s✝: String

c, i:

m₁: Meas

c', i':

m₂: Meas

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

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

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true
α: Type

F: Factory α

s✝: String

c, i, c', i':

h_c: c c'

h_i: i i'


text.text
α: Type

F: Factory α

s✝: String

c, i:

m₁: Meas

c', i':

m₂: Meas

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

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

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true
α: Type

F: Factory α

s✝: String

c, i, c', i':

h_c: c c'

h_i: i i'


text.text.left
c c'
α: Type

F: Factory α

s✝: String

c, i, c', i':

h_c: c c'

h_i: i i'


text.text.right
α: Type

F: Factory α

s✝: String

c, i:

m₁: Meas

c', i':

m₂: Meas

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

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

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true
α: Type

F: Factory α

s✝: String

c, i, c', i':

h_c: c c'

h_i: i i'


c c'

Goals accomplished! 🐙
α: Type

F: Factory α

s✝: String

c, i:

m₁: Meas

c', i':

m₂: Meas

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

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

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true
α: Type

F: Factory α

s✝: String

c, i, c', i':

h_c: c c'

h_i: i i'


α: Type

F: Factory α

s✝: String

c, i, c', i':

h_c: c c'

h_i: i i'


α: Type

F: Factory α

s✝: String

c, i, c', i':

h_c: c c'

h_i: i i'


c c'

Goals accomplished! 🐙
α: Type

d: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

F: Factory α

h: MeasRender F d c i m₁

h': MeasRender F d c' i' m₂

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true
α: Type

F: Factory α

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F Doc.nl c i m₁

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

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true
α: Type

F: Factory α

c, i, c', i':

m₂: Meas

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

h_c: c c'

h_i: i i'


nl
dominates F { last := i, cost := Factory.nl F i, doc := Doc.nl, x := max c i, y := i } m₂ = true
α: Type

F: Factory α

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F Doc.nl c i m₁

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

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'


nl.nl
dominates F { last := i, cost := Factory.nl F i, doc := Doc.nl, x := max c i, y := i } { last := i', cost := Factory.nl F i', doc := Doc.nl, x := max c' i', y := i' } = true
α: Type

F: Factory α

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F Doc.nl c i m₁

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

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'


nl.nl
α: Type

F: Factory α

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F Doc.nl c i m₁

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

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'


nl.nl
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'


nl.nl.left
i i'
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'


nl.nl.right
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'


nl.nl.right
α: Type

F: Factory α

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F Doc.nl c i m₁

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

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'


α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'


α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'


a
i i'

Goals accomplished! 🐙
α: Type

d: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

F: Factory α

h: MeasRender F d c i m₁

h': MeasRender F d c' i' m₂

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.align d✝) c i m₁

h': MeasRender F (Doc.align d✝) c' i' m₂

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true
α: Type

F: Factory α

n✝:

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i, c', i':

m₂: Meas

h': MeasRender F (Doc.nest n✝ d✝) c' i' m₂

h_c: c c'

h_i: i i'

last✝:

cost✝: α

x✝, y✝:

h✝: MeasRender F d✝ c (i + n✝) { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }


nest
dominates F { last := last✝, cost := cost✝, doc := Doc.nest n✝ d✝, x := x✝, y := y✝ } m₂ = true
α: Type

F: Factory α

n✝:

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.nest n✝ d✝) c i m₁

h': MeasRender F (Doc.nest n✝ d✝) c' i' m₂

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i, c', i':

m₂: Meas

h': MeasRender F (Doc.align d✝) c' i' m₂

h_c: c c'

h_i: i i'

last✝:

cost✝: α

x✝, y✝:

h: MeasRender F d✝ c c { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }


align
dominates F { last := last✝, cost := cost✝, doc := Doc.align d✝, x := x✝, y := max i y✝ } m₂ = true
α: Type

F: Factory α

n✝:

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.nest n✝ d✝) c i m₁

h': MeasRender F (Doc.nest n✝ d✝) c' i' m₂

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true
α: Type

F: Factory α

n✝:

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c (i + n✝) { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h✝: MeasRender F d✝ c' (i' + n✝) { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }


nest.nest
dominates F { last := last✝¹, cost := cost✝¹, doc := Doc.nest n✝ d✝, x := x✝¹, y := y✝¹ } { last := last✝, cost := cost✝, doc := Doc.nest n✝ d✝, x := x✝, y := y✝ } = true
α: Type

F: Factory α

n✝:

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.nest n✝ d✝) c i m₁

h': MeasRender F (Doc.nest n✝ d✝) c' i' m₂

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }


align.align
dominates F { last := last✝¹, cost := cost✝¹, doc := Doc.align d✝, x := x✝¹, y := max i y✝¹ } { last := last✝, cost := cost✝, doc := Doc.align d✝, x := x✝, y := max i' y✝ } = true
α: Type

F: Factory α

n✝:

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.nest n✝ d✝) c i m₁

h': MeasRender F (Doc.nest n✝ d✝) c' i' m₂

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }


align.align
dominates F { last := last✝¹, cost := cost✝¹, doc := Doc.align d✝, x := x✝¹, y := max i y✝¹ } { last := last✝, cost := cost✝, doc := Doc.align d✝, x := x✝, y := max i' y✝ } = true

Goals accomplished! 🐙
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }


c c'

Goals accomplished! 🐙
α: Type

F: Factory α

d✝: Doc

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

ih: dominates F { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ } { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ } = true


align.align
dominates F { last := last✝¹, cost := cost✝¹, doc := Doc.align d✝, x := x✝¹, y := max i y✝¹ } { last := last✝, cost := cost✝, doc := Doc.align d✝, x := x✝, y := max i' y✝ } = true
α: Type

F: Factory α

n✝:

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.nest n✝ d✝) c i m₁

h': MeasRender F (Doc.nest n✝ d✝) c' i' m₂

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true

Goals accomplished! 🐙
α: Type

d: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

F: Factory α

h: MeasRender F d c i m₁

h': MeasRender F d c' i' m₂

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.concat d₁✝ d₂✝) c i m₁

h': MeasRender F (Doc.concat d₁✝ d₂✝) c' i' m₂

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h': MeasRender F (Doc.concat d₁✝ d₂✝) c' i' m₂

h_c: c c'

h_i: i i'

m₁✝, m₂✝: Meas

h₂✝: MeasRender F d₂✝ m₁✝.last i m₂✝

h₁✝: MeasRender F d₁✝ c i m₁✝

h✝: m₁ = Meas.concat F m₁✝ m₂✝


concat
dominates F m₁ m₂ = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.concat d₁✝ d₂✝) c i m₁

h': MeasRender F (Doc.concat d₁✝ d₂✝) c' i' m₂

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h': MeasRender F (Doc.concat d₁✝ d₂✝) c' i' m₂

h_c: c c'

h_i: i i'

m₁✝, m₂✝: Meas

h₂: MeasRender F d₂✝ m₁✝.last i m₂✝

h₁: MeasRender F d₁✝ c i m₁✝

h_eq: m₁ = Meas.concat F m₁✝ m₂✝


dominates F m₁ m₂ = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂✝: MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁✝: MeasRender F d₁✝ c' i' m₁✝

h✝: m₂ = Meas.concat F m₁✝ m₂✝


concat
dominates F m₁ m₂ = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h': MeasRender F (Doc.concat d₁✝ d₂✝) c' i' m₂

h_c: c c'

h_i: i i'

m₁✝, m₂✝: Meas

h₂: MeasRender F d₂✝ m₁✝.last i m₂✝

h₁: MeasRender F d₁✝ c i m₁✝

h_eq: m₁ = Meas.concat F m₁✝ m₂✝


dominates F m₁ m₂ = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝


dominates F m₁ m₂ = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝


dominates F m₁ m₂ = true

Goals accomplished! 🐙
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝


i i'

Goals accomplished! 🐙
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝

ih₁: dominates F m₁✝¹ m₁✝ = true


dominates F m₁ m₂ = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝


dominates F m₁ m₂ = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝

ih₁: m₁✝¹.last m₁✝.last Factory.le F m₁✝¹.cost m₁✝.cost = true


dominates F m₁ m₂ = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝


dominates F m₁ m₂ = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝

ih₁: m₁✝¹.last m₁✝.last Factory.le F m₁✝¹.cost m₁✝.cost = true


dominates F m₁ m₂ = true

Goals accomplished! 🐙
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝

ih₁: m₁✝¹.last m₁✝.last Factory.le F m₁✝¹.cost m₁✝.cost = true


m₁✝¹.last m₁✝.last

Goals accomplished! 🐙
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝

ih₁: m₁✝¹.last m₁✝.last Factory.le F m₁✝¹.cost m₁✝.cost = true


dominates F m₁ m₂ = true

Goals accomplished! 🐙
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝

ih₁: m₁✝¹.last m₁✝.last Factory.le F m₁✝¹.cost m₁✝.cost = true


i i'

Goals accomplished! 🐙
α: Type

F: Factory α

d₁✝, d₂✝: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝

ih₁: m₁✝¹.last m₁✝.last Factory.le F m₁✝¹.cost m₁✝.cost = true

ih₂: dominates F m₂✝¹ m₂✝ = true


dominates F m₁ m₂ = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝


dominates F m₁ m₂ = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝

ih₁: m₁✝¹.last m₁✝.last Factory.le F m₁✝¹.cost m₁✝.cost = true

ih₂: m₂✝¹.last m₂✝.last Factory.le F m₂✝¹.cost m₂✝.cost = true


m₁.last m₂.last Factory.le F m₁.cost m₂.cost = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝


dominates F m₁ m₂ = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝

ih₁: m₁✝¹.last m₁✝.last Factory.le F m₁✝¹.cost m₁✝.cost = true

ih₂: m₂✝¹.last m₂✝.last Factory.le F m₂✝¹.cost m₂✝.cost = true


left
m₁.last m₂.last
α: Type

F: Factory α

d₁✝, d₂✝: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝

ih₁: m₁✝¹.last m₁✝.last Factory.le F m₁✝¹.cost m₁✝.cost = true

ih₂: m₂✝¹.last m₂✝.last Factory.le F m₂✝¹.cost m₂✝.cost = true


right
Factory.le F m₁.cost m₂.cost = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝


dominates F m₁ m₂ = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝

ih₁: m₁✝¹.last m₁✝.last Factory.le F m₁✝¹.cost m₁✝.cost = true

ih₂: m₂✝¹.last m₂✝.last Factory.le F m₂✝¹.cost m₂✝.cost = true


m₁.last m₂.last

Goals accomplished! 🐙
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝


dominates F m₁ m₂ = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝

ih₁: m₁✝¹.last m₁✝.last Factory.le F m₁✝¹.cost m₁✝.cost = true

ih₂: m₂✝¹.last m₂✝.last Factory.le F m₂✝¹.cost m₂✝.cost = true


Factory.le F m₁.cost m₂.cost = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝

ih₁: m₁✝¹.last m₁✝.last Factory.le F m₁✝¹.cost m₁✝.cost = true

ih₂: m₂✝¹.last m₂✝.last Factory.le F m₂✝¹.cost m₂✝.cost = true


Factory.le F (Factory.concat F m₁✝¹.cost m₂✝¹.cost) (Factory.concat F m₁✝.cost m₂✝.cost) = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝

ih₁: m₁✝¹.last m₁✝.last Factory.le F m₁✝¹.cost m₁✝.cost = true

ih₂: m₂✝¹.last m₂✝.last Factory.le F m₂✝¹.cost m₂✝.cost = true


Factory.le F m₁.cost m₂.cost = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝

ih₁: m₁✝¹.last m₁✝.last Factory.le F m₁✝¹.cost m₁✝.cost = true

ih₂: m₂✝¹.last m₂✝.last Factory.le F m₂✝¹.cost m₂✝.cost = true


a
Factory.le F m₁✝¹.cost m₁✝.cost = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝

ih₁: m₁✝¹.last m₁✝.last Factory.le F m₁✝¹.cost m₁✝.cost = true

ih₂: m₂✝¹.last m₂✝.last Factory.le F m₂✝¹.cost m₂✝.cost = true


a
Factory.le F m₂✝¹.cost m₂✝.cost = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝

ih₁: m₁✝¹.last m₁✝.last Factory.le F m₁✝¹.cost m₁✝.cost = true

ih₂: m₂✝¹.last m₂✝.last Factory.le F m₂✝¹.cost m₂✝.cost = true


Factory.le F m₁.cost m₂.cost = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝

ih₁: m₁✝¹.last m₁✝.last Factory.le F m₁✝¹.cost m₁✝.cost = true

ih₂: m₂✝¹.last m₂✝.last Factory.le F m₂✝¹.cost m₂✝.cost = true


a
Factory.le F m₁✝¹.cost m₁✝.cost = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝

ih₁: m₁✝¹.last m₁✝.last Factory.le F m₁✝¹.cost m₁✝.cost = true

ih₂: m₂✝¹.last m₂✝.last Factory.le F m₂✝¹.cost m₂✝.cost = true


a
Factory.le F m₂✝¹.cost m₂✝.cost = true

Goals accomplished! 🐙
α: Type

F: Factory α

d₁✝, d₂✝: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝

ih₁: m₁✝¹.last m₁✝.last Factory.le F m₁✝¹.cost m₁✝.cost = true

ih₂: m₂✝¹.last m₂✝.last Factory.le F m₂✝¹.cost m₂✝.cost = true


Factory.le F m₁.cost m₂.cost = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

h_eq: m₁ = Meas.concat F m₁✝¹ m₂✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝

ih₁: m₁✝¹.last m₁✝.last Factory.le F m₁✝¹.cost m₁✝.cost = true

ih₂: m₂✝¹.last m₂✝.last Factory.le F m₂✝¹.cost m₂✝.cost = true


a
Factory.le F m₂✝¹.cost m₂✝.cost = true

Goals accomplished! 🐙
α: Type

d: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

F: Factory α

h: MeasRender F d c i m₁

h': MeasRender F d c' i' m₂

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true
α: Type

F: Factory α

d₁✝, d₂✝: Doc

d₁_ih✝: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

d₂_ih✝: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'dominates F m₁ m₂ = true

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.choice d₁✝ d₂✝) c i m₁

h': MeasRender F (Doc.choice d₁✝ d₂✝) c' i' m₂

h_c: c c'

h_i: i i'


dominates F m₁ m₂ = true

Goals accomplished! 🐙

Goals accomplished! 🐙
/-- Measure computation on a choiceless document preserves the doc component -/ lemma
MeasRender_doc: ∀ {α : Type} {F : Factory α} {d : Doc} {c i : } {m : Meas}, MeasRender F d c i mChoiceless dm.doc = d
MeasRender_doc
(
h_render: MeasRender F d c i m
h_render
:
MeasRender: {α : Type} → Factory αDocMeasProp
MeasRender
F: ?m.10215
F
d: ?m.10222
d
c: ?m.10228
c
i: ?m.10234
i
m: ?m.10240
m
) (h :
Choiceless: DocProp
Choiceless
d: ?m.10222
d
) :
m: ?m.10240
m
.
doc: {α : Type} → MeasDoc
doc
=
d: ?m.10222
d
:=

Goals accomplished! 🐙
α✝: Type

F: Factory α✝

d: Doc

c, i:

m: Meas

h_render: MeasRender F d c i m

h: Choiceless d


m.doc = d
α✝: Type

F: Factory α✝

d: Doc

c, i:

m: Meas

h_render: MeasRender F d c i m

h: Choiceless d


m.doc = d
α✝: Type

F: Factory α✝

d: Doc

c, i:

m: Meas

h_render: MeasRender F d c i m

h: Choiceless d


m.doc = d
α✝: Type

F: Factory α✝

d: Doc

c, i:

m: Meas

h_render: MeasRender F d c i m

h✝: Choiceless d

s: String

ss: List String

h: Render d c i { fst := s, rst := ss }


m.doc = d
α✝: Type

F: Factory α✝

d: Doc

c, i:

m: Meas

h_render: MeasRender F d c i m

h: Choiceless d


m.doc = d
α✝: Type

F: Factory α✝

d: Doc

c, i:

m: Meas

h_render: MeasRender F d c i m

h✝: Choiceless d

s: String

h: Render d c i { fst := s, rst := [] }


nil
m.doc = d
α✝: Type

F: Factory α✝

d: Doc

c, i:

m: Meas

h_render: MeasRender F d c i m

h✝: Choiceless d

s, head✝: String

tail✝: List String

h: Render d c i { fst := s, rst := head✝ :: tail✝ }


cons
m.doc = d
α✝: Type

F: Factory α✝

d: Doc

c, i:

m: Meas

h_render: MeasRender F d c i m

h: Choiceless d


m.doc = d
α✝: Type

F: Factory α✝

d: Doc

c, i:

m: Meas

h_render: MeasRender F d c i m

h✝: Choiceless d

s: String

h: Render d c i { fst := s, rst := [] }


m.doc = d
α✝: Type

F: Factory α✝

d: Doc

c, i:

m: Meas

h_render: MeasRender F d c i m

h✝: Choiceless d

s: String

h: Render d c i { fst := s, rst := [] }

cost: α✝

y:

h_render': MeasRender F d c i { last := c + String.length s, cost := cost, doc := d, x := c + String.length s, y := y }


m.doc = d
α✝: Type

F: Factory α✝

d: Doc

c, i:

m: Meas

h_render: MeasRender F d c i m

h✝: Choiceless d

s: String

h: Render d c i { fst := s, rst := [] }


m.doc = d
α✝: Type

F: Factory α✝

d: Doc

c, i:

h✝: Choiceless d

s: String

h: Render d c i { fst := s, rst := [] }

cost: α✝

y:

h_render', h_render: MeasRender F d c i { last := c + String.length s, cost := cost, doc := d, x := c + String.length s, y := y }


refl
{ last := c + String.length s, cost := cost, doc := d, x := c + String.length s, y := y }.doc = d
α✝: Type

F: Factory α✝

d: Doc

c, i:

m: Meas

h_render: MeasRender F d c i m

h✝: Choiceless d

s: String

h: Render d c i { fst := s, rst := [] }


m.doc = d

Goals accomplished! 🐙
α✝: Type

F: Factory α✝

d: Doc

c, i:

m: Meas

h_render: MeasRender F d c i m

h: Choiceless d


m.doc = d
α✝: Type

F: Factory α✝

d: Doc

c, i:

m: Meas

h_render: MeasRender F d c i m

h✝: Choiceless d

s, hd: String

tl: List String

h: Render d c i { fst := s, rst := hd :: tl }


m.doc = d
α✝: Type

F: Factory α✝

d: Doc

c, i:

m: Meas

h_render: MeasRender F d c i m

h✝: Choiceless d

s, hd: String

tl: List String

h: Render d c i { fst := s, rst := hd :: tl }


m.doc = d

Goals accomplished! 🐙
α✝: Type

F: Factory α✝

d: Doc

c, i:

m: Meas

h_render: MeasRender F d c i m

h✝: Choiceless d

s, hd: String

tl: List String

h: Render d c i { fst := s, rst := hd :: tl }


hd :: tl []

Goals accomplished! 🐙
α✝: Type

F: Factory α✝

d: Doc

c, i:

m: Meas

h_render: MeasRender F d c i m

h✝: Choiceless d

s, hd: String

tl: List String

h: Render d c i { fst := s, rst := hd :: tl }

cost: α✝

y:

h_render': MeasRender F d c i { last := String.length (List.getLast (hd :: tl) (_ : ¬hd :: tl = [])), cost := cost, doc := d, x := Layout.max_with_offset c { fst := s, rst := hd :: tl }, y := y }


m.doc = d
α✝: Type

F: Factory α✝

d: Doc

c, i:

m: Meas

h_render: MeasRender F d c i m

h✝: Choiceless d

s, hd: String

tl: List String

h: Render d c i { fst := s, rst := hd :: tl }


m.doc = d
α✝: Type

F: Factory α✝

d: Doc

c, i:

h✝: Choiceless d

s, hd: String

tl: List String

h: Render d c i { fst := s, rst := hd :: tl }

cost: α✝

y:

h_render', h_render: MeasRender F d c i { last := String.length (List.getLast (hd :: tl) (_ : ¬hd :: tl = [])), cost := cost, doc := d, x := Layout.max_with_offset c { fst := s, rst := hd :: tl }, y := y }


refl
{ last := String.length (List.getLast (hd :: tl) (_ : ¬hd :: tl = [])), cost := cost, doc := d, x := Layout.max_with_offset c { fst := s, rst := hd :: tl }, y := y }.doc = d
α✝: Type

F: Factory α✝

d: Doc

c, i:

m: Meas

h_render: MeasRender F d c i m

h✝: Choiceless d

s, hd: String

tl: List String

h: Render d c i { fst := s, rst := hd :: tl }


m.doc = d

Goals accomplished! 🐙

Goals accomplished! 🐙
/-- If measure computation at higher column position or indentation level does not exceed the computation width limit, then the current measure computation also does not exceed the computation width limit -/ lemma
MeasRender_dom_is_good: ∀ {α : Type} {d : Doc} {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas} {F : Factory α}, MeasRender F d c i m₁MeasRender F d c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W
MeasRender_dom_is_good
{
F: Factory α
F
:
Factory: TypeType
Factory
α: ?m.11376
α
} (
h: MeasRender F d c i m₁
h
:
MeasRender: {α : Type} → Factory αDocMeasProp
MeasRender
F: Factory α
F
d: ?m.11384
d
c: ?m.11391
c
i: ?m.11398
i
m₁: ?m.11405
m₁
) (
h': MeasRender F d c' i' m₂
h'
:
MeasRender: {α : Type} → Factory αDocMeasProp
MeasRender
F: Factory α
F
d: ?m.11384
d
c': ?m.11416
c'
i': ?m.11426
i'
m₂: ?m.11436
m₂
) (
h_c: c c'
h_c
:
c: ?m.11391
c
c': ?m.11416
c'
) (
h_i: i i'
h_i
:
i: ?m.11398
i
i': ?m.11426
i'
) (
h_x: m₂.x F.W
h_x
:
m₂: ?m.11436
m₂
.
x: {α : Type} → Meas
x
F: Factory α
F
.
W: {α : Type} → Factory α
W
) (
h_y: m₂.y F.W
h_y
:
m₂: ?m.11436
m₂
.
y: {α : Type} → Meas
y
F: Factory α
F
.
W: {α : Type} → Factory α
W
) :
m₁: ?m.11405
m₁
.
x: {α : Type} → Meas
x
F: Factory α
F
.
W: {α : Type} → Factory α
W
m₁: ?m.11405
m₁
.
y: {α : Type} → Meas
y
F: Factory α
F
.
W: {α : Type} → Factory α
W
:=

Goals accomplished! 🐙
α: Type

d: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

F: Factory α

h: MeasRender F d c i m₁

h': MeasRender F d c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

d: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

F: Factory α

h: MeasRender F d c i m₁

h': MeasRender F d c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

d: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

F: Factory α

h: MeasRender F d c i m₁

h': MeasRender F d c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

s✝: String

c, i:

m₁: Meas

c', i':

m₂: Meas

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

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

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


text
m₁.x F.W m₁.y F.W
α: Type

F: Factory α

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F Doc.nl c i m₁

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

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


nl
m₁.x F.W m₁.y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

d₁_ih✝: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

d₂_ih✝: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.concat d₁✝ d₂✝) c i m₁

h': MeasRender F (Doc.concat d₁✝ d₂✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


concat
m₁.x F.W m₁.y F.W
α: Type

F: Factory α

n✝:

d✝: Doc

d_ih✝: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.nest n✝ d✝) c i m₁

h': MeasRender F (Doc.nest n✝ d✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


nest
m₁.x F.W m₁.y F.W
α: Type

F: Factory α

d✝: Doc

d_ih✝: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.align d✝) c i m₁

h': MeasRender F (Doc.align d✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


align
m₁.x F.W m₁.y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

d₁_ih✝: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

d₂_ih✝: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.choice d₁✝ d₂✝) c i m₁

h': MeasRender F (Doc.choice d₁✝ d₂✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


choice
m₁.x F.W m₁.y F.W
α: Type

d: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

F: Factory α

h: MeasRender F d c i m₁

h': MeasRender F d c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

s✝: String

c, i:

m₁: Meas

c', i':

m₂: Meas

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

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

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

s✝: String

c, i, c', i':

m₂: Meas

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

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


text
{ last := c + String.length s✝, cost := Factory.text F c (String.length s✝), doc := Doc.text s✝, x := c + String.length s✝, y := i }.x F.W { last := c + String.length s✝, cost := Factory.text F c (String.length s✝), doc := Doc.text s✝, x := c + String.length s✝, y := i }.y F.W
α: Type

F: Factory α

s✝: String

c, i:

m₁: Meas

c', i':

m₂: Meas

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

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

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

s✝: String

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := c' + String.length s✝, cost := Factory.text F c' (String.length s✝), doc := Doc.text s✝, x := c' + String.length s✝, y := i' }.x F.W

h_y: { last := c' + String.length s✝, cost := Factory.text F c' (String.length s✝), doc := Doc.text s✝, x := c' + String.length s✝, y := i' }.y F.W


text.text
{ last := c + String.length s✝, cost := Factory.text F c (String.length s✝), doc := Doc.text s✝, x := c + String.length s✝, y := i }.x F.W { last := c + String.length s✝, cost := Factory.text F c (String.length s✝), doc := Doc.text s✝, x := c + String.length s✝, y := i }.y F.W
α: Type

F: Factory α

s✝: String

c, i:

m₁: Meas

c', i':

m₂: Meas

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

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

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

s✝: String

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := c' + String.length s✝, cost := Factory.text F c' (String.length s✝), doc := Doc.text s✝, x := c' + String.length s✝, y := i' }.x F.W

h_y: { last := c' + String.length s✝, cost := Factory.text F c' (String.length s✝), doc := Doc.text s✝, x := c' + String.length s✝, y := i' }.y F.W


text.text
c + String.length s✝ F.W i F.W
α: Type

F: Factory α

s✝: String

c, i:

m₁: Meas

c', i':

m₂: Meas

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

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

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

s✝: String

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := c' + String.length s✝, cost := Factory.text F c' (String.length s✝), doc := Doc.text s✝, x := c' + String.length s✝, y := i' }.x F.W

h_y: { last := c' + String.length s✝, cost := Factory.text F c' (String.length s✝), doc := Doc.text s✝, x := c' + String.length s✝, y := i' }.y F.W


text.text.left
c + String.length s✝ F.W
α: Type

F: Factory α

s✝: String

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := c' + String.length s✝, cost := Factory.text F c' (String.length s✝), doc := Doc.text s✝, x := c' + String.length s✝, y := i' }.x F.W

h_y: { last := c' + String.length s✝, cost := Factory.text F c' (String.length s✝), doc := Doc.text s✝, x := c' + String.length s✝, y := i' }.y F.W


text.text.right
i F.W
α: Type

F: Factory α

s✝: String

c, i:

m₁: Meas

c', i':

m₂: Meas

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

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

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

s✝: String

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := c' + String.length s✝, cost := Factory.text F c' (String.length s✝), doc := Doc.text s✝, x := c' + String.length s✝, y := i' }.x F.W

h_y: { last := c' + String.length s✝, cost := Factory.text F c' (String.length s✝), doc := Doc.text s✝, x := c' + String.length s✝, y := i' }.y F.W


c + String.length s✝ F.W

Goals accomplished! 🐙
α: Type

F: Factory α

s✝: String

c, i:

m₁: Meas

c', i':

m₂: Meas

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

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

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

s✝: String

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := c' + String.length s✝, cost := Factory.text F c' (String.length s✝), doc := Doc.text s✝, x := c' + String.length s✝, y := i' }.x F.W

h_y: { last := c' + String.length s✝, cost := Factory.text F c' (String.length s✝), doc := Doc.text s✝, x := c' + String.length s✝, y := i' }.y F.W


i F.W
α: Type

F: Factory α

s✝: String

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := c' + String.length s✝, cost := Factory.text F c' (String.length s✝), doc := Doc.text s✝, x := c' + String.length s✝, y := i' }.x F.W

h_y: i' F.W


i F.W
α: Type

F: Factory α

s✝: String

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := c' + String.length s✝, cost := Factory.text F c' (String.length s✝), doc := Doc.text s✝, x := c' + String.length s✝, y := i' }.x F.W

h_y: { last := c' + String.length s✝, cost := Factory.text F c' (String.length s✝), doc := Doc.text s✝, x := c' + String.length s✝, y := i' }.y F.W


i F.W
α: Type

F: Factory α

s✝: String

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := c' + String.length s✝, cost := Factory.text F c' (String.length s✝), doc := Doc.text s✝, x := c' + String.length s✝, y := i' }.x F.W

h_y: i' F.W


i F.W
α: Type

F: Factory α

s✝: String

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := c' + String.length s✝, cost := Factory.text F c' (String.length s✝), doc := Doc.text s✝, x := c' + String.length s✝, y := i' }.x F.W

h_y: i' F.W


a
i ?b
α: Type

F: Factory α

s✝: String

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := c' + String.length s✝, cost := Factory.text F c' (String.length s✝), doc := Doc.text s✝, x := c' + String.length s✝, y := i' }.x F.W

h_y: i' F.W


a
?b F.W
α: Type

F: Factory α

s✝: String

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := c' + String.length s✝, cost := Factory.text F c' (String.length s✝), doc := Doc.text s✝, x := c' + String.length s✝, y := i' }.x F.W

h_y: i' F.W


b

Goals accomplished! 🐙
α: Type

d: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

F: Factory α

h: MeasRender F d c i m₁

h': MeasRender F d c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F Doc.nl c i m₁

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

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

c, i, c', i':

m₂: Meas

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

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


nl
{ last := i, cost := Factory.nl F i, doc := Doc.nl, x := max c i, y := i }.x F.W { last := i, cost := Factory.nl F i, doc := Doc.nl, x := max c i, y := i }.y F.W
α: Type

F: Factory α

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F Doc.nl c i m₁

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

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := i', cost := Factory.nl F i', doc := Doc.nl, x := max c' i', y := i' }.x F.W

h_y: { last := i', cost := Factory.nl F i', doc := Doc.nl, x := max c' i', y := i' }.y F.W


nl.nl
{ last := i, cost := Factory.nl F i, doc := Doc.nl, x := max c i, y := i }.x F.W { last := i, cost := Factory.nl F i, doc := Doc.nl, x := max c i, y := i }.y F.W
α: Type

F: Factory α

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F Doc.nl c i m₁

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

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := i', cost := Factory.nl F i', doc := Doc.nl, x := max c' i', y := i' }.x F.W

h_y: { last := i', cost := Factory.nl F i', doc := Doc.nl, x := max c' i', y := i' }.y F.W


nl.nl
max c i F.W i F.W
α: Type

F: Factory α

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F Doc.nl c i m₁

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

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := i', cost := Factory.nl F i', doc := Doc.nl, x := max c' i', y := i' }.x F.W

h_y: { last := i', cost := Factory.nl F i', doc := Doc.nl, x := max c' i', y := i' }.y F.W


nl.nl.left
max c i F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := i', cost := Factory.nl F i', doc := Doc.nl, x := max c' i', y := i' }.x F.W

h_y: { last := i', cost := Factory.nl F i', doc := Doc.nl, x := max c' i', y := i' }.y F.W


nl.nl.right
i F.W
α: Type

F: Factory α

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F Doc.nl c i m₁

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

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := i', cost := Factory.nl F i', doc := Doc.nl, x := max c' i', y := i' }.x F.W

h_y: { last := i', cost := Factory.nl F i', doc := Doc.nl, x := max c' i', y := i' }.y F.W


max c i F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_y: i' F.W

h_x: c' F.W i' F.W


c F.W i F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := i', cost := Factory.nl F i', doc := Doc.nl, x := max c' i', y := i' }.x F.W

h_y: { last := i', cost := Factory.nl F i', doc := Doc.nl, x := max c' i', y := i' }.y F.W


max c i F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_y: i' F.W

h_x: c' F.W i' F.W


left
c F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_y: i' F.W

h_x: c' F.W i' F.W


right
i F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := i', cost := Factory.nl F i', doc := Doc.nl, x := max c' i', y := i' }.x F.W

h_y: { last := i', cost := Factory.nl F i', doc := Doc.nl, x := max c' i', y := i' }.y F.W


max c i F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_y: i' F.W

h_x: c' F.W i' F.W


c F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_y: i' F.W

h_x: c' F.W i' F.W


a
c ?b
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_y: i' F.W

h_x: c' F.W i' F.W


a
?b F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_y: i' F.W

h_x: c' F.W i' F.W


b
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_y: i' F.W

h_x: c' F.W i' F.W


c F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_y: i' F.W

h_x: c' F.W i' F.W


a
c ?b
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_y: i' F.W

h_x: c' F.W i' F.W


a
?b F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_y: i' F.W

h_x: c' F.W i' F.W


b

Goals accomplished! 🐙
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_y: i' F.W

h_x: c' F.W i' F.W


c F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_y: i' F.W

h_x: c' F.W i' F.W


a
c' F.W

Goals accomplished! 🐙
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := i', cost := Factory.nl F i', doc := Doc.nl, x := max c' i', y := i' }.x F.W

h_y: { last := i', cost := Factory.nl F i', doc := Doc.nl, x := max c' i', y := i' }.y F.W


max c i F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_y: i' F.W

h_x: c' F.W i' F.W


i F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_y: i' F.W

h_x: c' F.W i' F.W


a
i ?b
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_y: i' F.W

h_x: c' F.W i' F.W


a
?b F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_y: i' F.W

h_x: c' F.W i' F.W


b
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_y: i' F.W

h_x: c' F.W i' F.W


i F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_y: i' F.W

h_x: c' F.W i' F.W


a
i ?b
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_y: i' F.W

h_x: c' F.W i' F.W


a
?b F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_y: i' F.W

h_x: c' F.W i' F.W


b

Goals accomplished! 🐙
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_y: i' F.W

h_x: c' F.W i' F.W


i F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_y: i' F.W

h_x: c' F.W i' F.W


a
i' F.W

Goals accomplished! 🐙
α: Type

F: Factory α

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F Doc.nl c i m₁

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

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := i', cost := Factory.nl F i', doc := Doc.nl, x := max c' i', y := i' }.x F.W

h_y: { last := i', cost := Factory.nl F i', doc := Doc.nl, x := max c' i', y := i' }.y F.W


i F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := i', cost := Factory.nl F i', doc := Doc.nl, x := max c' i', y := i' }.x F.W

h_y: i' F.W


i F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := i', cost := Factory.nl F i', doc := Doc.nl, x := max c' i', y := i' }.x F.W

h_y: { last := i', cost := Factory.nl F i', doc := Doc.nl, x := max c' i', y := i' }.y F.W


i F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := i', cost := Factory.nl F i', doc := Doc.nl, x := max c' i', y := i' }.x F.W

h_y: i' F.W


i F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := i', cost := Factory.nl F i', doc := Doc.nl, x := max c' i', y := i' }.x F.W

h_y: i' F.W


a
i ?b
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := i', cost := Factory.nl F i', doc := Doc.nl, x := max c' i', y := i' }.x F.W

h_y: i' F.W


a
?b F.W
α: Type

F: Factory α

c, i, c', i':

h_c: c c'

h_i: i i'

h_x: { last := i', cost := Factory.nl F i', doc := Doc.nl, x := max c' i', y := i' }.x F.W

h_y: i' F.W


b

Goals accomplished! 🐙
α: Type

d: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

F: Factory α

h: MeasRender F d c i m₁

h': MeasRender F d c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

n✝:

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.nest n✝ d✝) c i m₁

h': MeasRender F (Doc.nest n✝ d✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

n✝:

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

m₂: Meas

h': MeasRender F (Doc.nest n✝ d✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W

last✝:

cost✝: α

x✝, y✝:

h✝: MeasRender F d✝ c (i + n✝) { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }


nest
{ last := last✝, cost := cost✝, doc := Doc.nest n✝ d✝, x := x✝, y := y✝ }.x F.W { last := last✝, cost := cost✝, doc := Doc.nest n✝ d✝, x := x✝, y := y✝ }.y F.W
α: Type

F: Factory α

n✝:

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.nest n✝ d✝) c i m₁

h': MeasRender F (Doc.nest n✝ d✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

n✝:

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

m₂: Meas

h': MeasRender F (Doc.nest n✝ d✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W

last✝:

cost✝: α

x✝, y✝:

h: MeasRender F d✝ c (i + n✝) { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }


nest
{ last := last✝, cost := cost✝, doc := Doc.nest n✝ d✝, x := x✝, y := y✝ }.x F.W { last := last✝, cost := cost✝, doc := Doc.nest n✝ d✝, x := x✝, y := y✝ }.y F.W
α: Type

F: Factory α

n✝:

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.nest n✝ d✝) c i m₁

h': MeasRender F (Doc.nest n✝ d✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

n✝:

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c (i + n✝) { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h✝: MeasRender F d✝ c' (i' + n✝) { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: { last := last✝, cost := cost✝, doc := Doc.nest n✝ d✝, x := x✝, y := y✝ }.x F.W

h_y: { last := last✝, cost := cost✝, doc := Doc.nest n✝ d✝, x := x✝, y := y✝ }.y F.W


nest.nest
{ last := last✝¹, cost := cost✝¹, doc := Doc.nest n✝ d✝, x := x✝¹, y := y✝¹ }.x F.W { last := last✝¹, cost := cost✝¹, doc := Doc.nest n✝ d✝, x := x✝¹, y := y✝¹ }.y F.W
α: Type

F: Factory α

n✝:

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.nest n✝ d✝) c i m₁

h': MeasRender F (Doc.nest n✝ d✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

n✝:

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c (i + n✝) { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' (i' + n✝) { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: { last := last✝, cost := cost✝, doc := Doc.nest n✝ d✝, x := x✝, y := y✝ }.x F.W

h_y: { last := last✝, cost := cost✝, doc := Doc.nest n✝ d✝, x := x✝, y := y✝ }.y F.W


nest.nest
{ last := last✝¹, cost := cost✝¹, doc := Doc.nest n✝ d✝, x := x✝¹, y := y✝¹ }.x F.W { last := last✝¹, cost := cost✝¹, doc := Doc.nest n✝ d✝, x := x✝¹, y := y✝¹ }.y F.W
α: Type

F: Factory α

n✝:

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.nest n✝ d✝) c i m₁

h': MeasRender F (Doc.nest n✝ d✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

n✝:

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c (i + n✝) { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' (i' + n✝) { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: y✝ F.W


nest.nest
x✝¹ F.W y✝¹ F.W
α: Type

F: Factory α

n✝:

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.nest n✝ d✝) c i m₁

h': MeasRender F (Doc.nest n✝ d✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

n✝:

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c (i + n✝) { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' (i' + n✝) { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: y✝ F.W


nest.nest
x✝¹ F.W y✝¹ F.W

Goals accomplished! 🐙
α: Type

F: Factory α

n✝:

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c (i + n✝) { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' (i' + n✝) { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: y✝ F.W


i + n✝ i' + n✝

Goals accomplished! 🐙

Goals accomplished! 🐙
α: Type

d: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

F: Factory α

h: MeasRender F d c i m₁

h': MeasRender F d c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.align d✝) c i m₁

h': MeasRender F (Doc.align d✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

m₂: Meas

h': MeasRender F (Doc.align d✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W

last✝:

cost✝: α

x✝, y✝:

h✝: MeasRender F d✝ c c { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }


align
{ last := last✝, cost := cost✝, doc := Doc.align d✝, x := x✝, y := max i y✝ }.x F.W { last := last✝, cost := cost✝, doc := Doc.align d✝, x := x✝, y := max i y✝ }.y F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.align d✝) c i m₁

h': MeasRender F (Doc.align d✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

m₂: Meas

h': MeasRender F (Doc.align d✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W

last✝:

cost✝: α

x✝, y✝:

h: MeasRender F d✝ c c { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }


align
{ last := last✝, cost := cost✝, doc := Doc.align d✝, x := x✝, y := max i y✝ }.x F.W { last := last✝, cost := cost✝, doc := Doc.align d✝, x := x✝, y := max i y✝ }.y F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.align d✝) c i m₁

h': MeasRender F (Doc.align d✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h✝: MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: { last := last✝, cost := cost✝, doc := Doc.align d✝, x := x✝, y := max i' y✝ }.x F.W

h_y: { last := last✝, cost := cost✝, doc := Doc.align d✝, x := x✝, y := max i' y✝ }.y F.W


align.align
{ last := last✝¹, cost := cost✝¹, doc := Doc.align d✝, x := x✝¹, y := max i y✝¹ }.x F.W { last := last✝¹, cost := cost✝¹, doc := Doc.align d✝, x := x✝¹, y := max i y✝¹ }.y F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.align d✝) c i m₁

h': MeasRender F (Doc.align d✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: { last := last✝, cost := cost✝, doc := Doc.align d✝, x := x✝, y := max i' y✝ }.x F.W

h_y: { last := last✝, cost := cost✝, doc := Doc.align d✝, x := x✝, y := max i' y✝ }.y F.W


align.align
{ last := last✝¹, cost := cost✝¹, doc := Doc.align d✝, x := x✝¹, y := max i y✝¹ }.x F.W { last := last✝¹, cost := cost✝¹, doc := Doc.align d✝, x := x✝¹, y := max i y✝¹ }.y F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.align d✝) c i m₁

h': MeasRender F (Doc.align d✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W


align.align
x✝¹ F.W i F.W y✝¹ F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.align d✝) c i m₁

h': MeasRender F (Doc.align d✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W


align.align
x✝¹ F.W i F.W y✝¹ F.W

Goals accomplished! 🐙
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W


c c'

Goals accomplished! 🐙
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W


align.align
x✝¹ F.W i F.W y✝¹ F.W

Goals accomplished! 🐙
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W


{ last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }.y F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W


{ last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }.y F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W


{ last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }.y F.W

Goals accomplished! 🐙

Goals accomplished! 🐙
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W

this: { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }.x F.W { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }.y F.W


align.align
x✝¹ F.W i F.W y✝¹ F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.align d✝) c i m₁

h': MeasRender F (Doc.align d✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W

this: x✝¹ F.W y✝¹ F.W


align.align
x✝¹ F.W i F.W y✝¹ F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.align d✝) c i m₁

h': MeasRender F (Doc.align d✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W

this: x✝¹ F.W y✝¹ F.W


align.align.left
x✝¹ F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W

this: x✝¹ F.W y✝¹ F.W


align.align.right
i F.W y✝¹ F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.align d✝) c i m₁

h': MeasRender F (Doc.align d✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W

this: x✝¹ F.W y✝¹ F.W


x✝¹ F.W

Goals accomplished! 🐙
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.align d✝) c i m₁

h': MeasRender F (Doc.align d✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W

this: x✝¹ F.W y✝¹ F.W


i F.W y✝¹ F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W

this: x✝¹ F.W y✝¹ F.W


left
i F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W

this: x✝¹ F.W y✝¹ F.W


right
y✝¹ F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W

this: x✝¹ F.W y✝¹ F.W


i F.W y✝¹ F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W

this: x✝¹ F.W y✝¹ F.W


i F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W

this: x✝¹ F.W y✝¹ F.W


a
i ?b
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W

this: x✝¹ F.W y✝¹ F.W


a
?b F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W

this: x✝¹ F.W y✝¹ F.W


b
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W

this: x✝¹ F.W y✝¹ F.W


i F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W

this: x✝¹ F.W y✝¹ F.W


a
i ?b
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W

this: x✝¹ F.W y✝¹ F.W


a
?b F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W

this: x✝¹ F.W y✝¹ F.W


b

Goals accomplished! 🐙
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W

this: x✝¹ F.W y✝¹ F.W


i F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W

this: x✝¹ F.W y✝¹ F.W


a
i' F.W

Goals accomplished! 🐙
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W

this: x✝¹ F.W y✝¹ F.W


i F.W y✝¹ F.W
α: Type

F: Factory α

d✝: Doc

ih: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d✝ c i m₁MeasRender F d✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

last✝¹:

cost✝¹: α

x✝¹, y✝¹:

h: MeasRender F d✝ c c { last := last✝¹, cost := cost✝¹, doc := d✝, x := x✝¹, y := y✝¹ }

last✝:

cost✝: α

x✝, y✝:

h': MeasRender F d✝ c' c' { last := last✝, cost := cost✝, doc := d✝, x := x✝, y := y✝ }

h_x: x✝ F.W

h_y: i' F.W y✝ F.W

this: x✝¹ F.W y✝¹ F.W


y✝¹ F.W

Goals accomplished! 🐙
α: Type

d: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

F: Factory α

h: MeasRender F d c i m₁

h': MeasRender F d c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.concat d₁✝ d₂✝) c i m₁

h': MeasRender F (Doc.concat d₁✝ d₂✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h': MeasRender F (Doc.concat d₁✝ d₂✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W

m₁✝, m₂✝: Meas

h₂✝: MeasRender F d₂✝ m₁✝.last i m₂✝

h₁✝: MeasRender F d₁✝ c i m₁✝

h✝: m₁ = Meas.concat F m₁✝ m₂✝


concat
m₁.x F.W m₁.y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.concat d₁✝ d₂✝) c i m₁

h': MeasRender F (Doc.concat d₁✝ d₂✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h': MeasRender F (Doc.concat d₁✝ d₂✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W

m₁✝, m₂✝: Meas

h₂: MeasRender F d₂✝ m₁✝.last i m₂✝

h₁: MeasRender F d₁✝ c i m₁✝

h_eq: m₁ = Meas.concat F m₁✝ m₂✝


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

m₂: Meas

h': MeasRender F (Doc.concat d₁✝ d₂✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W

m₁✝, m₂✝: Meas

h₂: MeasRender F d₂✝ m₁✝.last i m₂✝

h₁: MeasRender F d₁✝ c i m₁✝


(Meas.concat F m₁✝ m₂✝).x F.W (Meas.concat F m₁✝ m₂✝).y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h': MeasRender F (Doc.concat d₁✝ d₂✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W

m₁✝, m₂✝: Meas

h₂: MeasRender F d₂✝ m₁✝.last i m₂✝

h₁: MeasRender F d₁✝ c i m₁✝

h_eq: m₁ = Meas.concat F m₁✝ m₂✝


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

m₂: Meas

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂✝: MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁✝: MeasRender F d₁✝ c' i' m₁✝

h✝: m₂ = Meas.concat F m₁✝ m₂✝


concat
(Meas.concat F m₁✝¹ m₂✝¹).x F.W (Meas.concat F m₁✝¹ m₂✝¹).y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h': MeasRender F (Doc.concat d₁✝ d₂✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W

m₁✝, m₂✝: Meas

h₂: MeasRender F d₂✝ m₁✝.last i m₂✝

h₁: MeasRender F d₁✝ c i m₁✝

h_eq: m₁ = Meas.concat F m₁✝ m₂✝


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

m₂: Meas

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝


(Meas.concat F m₁✝¹ m₂✝¹).x F.W (Meas.concat F m₁✝¹ m₂✝¹).y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_x: (Meas.concat F m₁✝ m₂✝).x F.W

h_y: (Meas.concat F m₁✝ m₂✝).y F.W


(Meas.concat F m₁✝¹ m₂✝¹).x F.W (Meas.concat F m₁✝¹ m₂✝¹).y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

m₂: Meas

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝


(Meas.concat F m₁✝¹ m₂✝¹).x F.W (Meas.concat F m₁✝¹ m₂✝¹).y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_x: m₁✝.x F.W m₂✝.x F.W

h_y: m₁✝.y F.W m₂✝.y F.W


(m₁✝¹.x F.W m₂✝¹.x F.W) m₁✝¹.y F.W m₂✝¹.y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

m₂: Meas

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝


(Meas.concat F m₁✝¹ m₂✝¹).x F.W (Meas.concat F m₁✝¹ m₂✝¹).y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_x: m₁✝.x F.W m₂✝.x F.W

h_y: m₁✝.y F.W m₂✝.y F.W

this: dominates F m₁✝¹ m₁✝ = true


(m₁✝¹.x F.W m₂✝¹.x F.W) m₁✝¹.y F.W m₂✝¹.y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

m₂: Meas

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝


(Meas.concat F m₁✝¹ m₂✝¹).x F.W (Meas.concat F m₁✝¹ m₂✝¹).y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_x: m₁✝.x F.W m₂✝.x F.W

h_y: m₁✝.y F.W m₂✝.y F.W

this: dominates F m₁✝¹ m₁✝ = true


(m₁✝¹.x F.W m₂✝¹.x F.W) m₁✝¹.y F.W m₂✝¹.y F.W

Goals accomplished! 🐙
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_x: m₁✝.x F.W m₂✝.x F.W

h_y: m₁✝.y F.W m₂✝.y F.W

this: dominates F m₁✝¹ m₁✝ = true


i i'

Goals accomplished! 🐙
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_x: m₁✝.x F.W m₂✝.x F.W

h_y: m₁✝.y F.W m₂✝.y F.W

this: dominates F m₁✝¹ m₁✝ = true


(m₁✝¹.x F.W m₂✝¹.x F.W) m₁✝¹.y F.W m₂✝¹.y F.W

Goals accomplished! 🐙
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_x: m₁✝.x F.W m₂✝.x F.W

h_y: m₁✝.y F.W m₂✝.y F.W

this: dominates F m₁✝¹ m₁✝ = true


m₁✝.x F.W

Goals accomplished! 🐙
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_x: m₁✝.x F.W m₂✝.x F.W

h_y: m₁✝.y F.W m₂✝.y F.W

this: dominates F m₁✝¹ m₁✝ = true


(m₁✝¹.x F.W m₂✝¹.x F.W) m₁✝¹.y F.W m₂✝¹.y F.W

Goals accomplished! 🐙
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_x: m₁✝.x F.W m₂✝.x F.W

h_y: m₁✝.y F.W m₂✝.y F.W

this: dominates F m₁✝¹ m₁✝ = true


m₁✝.y F.W

Goals accomplished! 🐙
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_x: m₁✝.x F.W m₂✝.x F.W

h_y: m₁✝.y F.W m₂✝.y F.W

this: dominates F m₁✝¹ m₁✝ = true

ih₁: m₁✝¹.x F.W m₁✝¹.y F.W


(m₁✝¹.x F.W m₂✝¹.x F.W) m₁✝¹.y F.W m₂✝¹.y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

m₂: Meas

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝


(Meas.concat F m₁✝¹ m₂✝¹).x F.W (Meas.concat F m₁✝¹ m₂✝¹).y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_x: m₁✝.x F.W m₂✝.x F.W

h_y: m₁✝.y F.W m₂✝.y F.W

this: dominates F m₁✝¹ m₁✝ = true

ih₁: m₁✝¹.x F.W m₁✝¹.y F.W


(m₁✝¹.x F.W m₂✝¹.x F.W) m₁✝¹.y F.W m₂✝¹.y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

m₂: Meas

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝


(Meas.concat F m₁✝¹ m₂✝¹).x F.W (Meas.concat F m₁✝¹ m₂✝¹).y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_x: m₁✝.x F.W m₂✝.x F.W

h_y: m₁✝.y F.W m₂✝.y F.W

this: dominates F m₁✝¹ m₁✝ = true

ih₁: m₁✝¹.x F.W m₁✝¹.y F.W


(m₁✝¹.x F.W m₂✝¹.x F.W) m₁✝¹.y F.W m₂✝¹.y F.W

Goals accomplished! 🐙
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_x: m₁✝.x F.W m₂✝.x F.W

h_y: m₁✝.y F.W m₂✝.y F.W

this: dominates F m₁✝¹ m₁✝ = true

ih₁: m₁✝¹.x F.W m₁✝¹.y F.W


m₁✝¹.last m₁✝.last
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_x: m₁✝.x F.W m₂✝.x F.W

h_y: m₁✝.y F.W m₂✝.y F.W

this: dominates F m₁✝¹ m₁✝ = true

ih₁: m₁✝¹.x F.W m₁✝¹.y F.W


m₁✝¹.last m₁✝.last
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_x: m₁✝.x F.W m₂✝.x F.W

h_y: m₁✝.y F.W m₂✝.y F.W

this: dominates F m₁✝¹ m₁✝ = true

ih₁: m₁✝¹.x F.W m₁✝¹.y F.W


m₁✝¹.last m₁✝.last
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_x: m₁✝.x F.W m₂✝.x F.W

h_y: m₁✝.y F.W m₂✝.y F.W

ih₁: m₁✝¹.x F.W m₁✝¹.y F.W

this: m₁✝¹.last m₁✝.last Factory.le F m₁✝¹.cost m₁✝.cost = true


m₁✝¹.last m₁✝.last
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_x: m₁✝.x F.W m₂✝.x F.W

h_y: m₁✝.y F.W m₂✝.y F.W

this: dominates F m₁✝¹ m₁✝ = true

ih₁: m₁✝¹.x F.W m₁✝¹.y F.W


m₁✝¹.last m₁✝.last

Goals accomplished! 🐙

Goals accomplished! 🐙
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_x: m₁✝.x F.W m₂✝.x F.W

h_y: m₁✝.y F.W m₂✝.y F.W

this: dominates F m₁✝¹ m₁✝ = true

ih₁: m₁✝¹.x F.W m₁✝¹.y F.W


(m₁✝¹.x F.W m₂✝¹.x F.W) m₁✝¹.y F.W m₂✝¹.y F.W

Goals accomplished! 🐙
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_x: m₁✝.x F.W m₂✝.x F.W

h_y: m₁✝.y F.W m₂✝.y F.W

this: dominates F m₁✝¹ m₁✝ = true

ih₁: m₁✝¹.x F.W m₁✝¹.y F.W


i i'

Goals accomplished! 🐙
α: Type

F: Factory α

d₁✝, d₂✝: Doc

c, i, c', i':

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_x: m₁✝.x F.W m₂✝.x F.W

h_y: m₁✝.y F.W m₂✝.y F.W

this: dominates F m₁✝¹ m₁✝ = true

ih₁: m₁✝¹.x F.W m₁✝¹.y F.W

ih₂: m₂✝.x F.Wm₂✝.y F.Wm₂✝¹.x F.W m₂✝¹.y F.W


(m₁✝¹.x F.W m₂✝¹.x F.W) m₁✝¹.y F.W m₂✝¹.y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

m₂: Meas

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝


(Meas.concat F m₁✝¹ m₂✝¹).x F.W (Meas.concat F m₁✝¹ m₂✝¹).y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

c, i, c', i':

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_x: m₁✝.x F.W m₂✝.x F.W

h_y: m₁✝.y F.W m₂✝.y F.W

this: dominates F m₁✝¹ m₁✝ = true

ih₁: m₁✝¹.x F.W m₁✝¹.y F.W

ih₂: m₂✝.x F.Wm₂✝.y F.Wm₂✝¹.x F.W m₂✝¹.y F.W


(m₁✝¹.x F.W m₂✝¹.x F.W) m₁✝¹.y F.W m₂✝¹.y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

m₂: Meas

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝


(Meas.concat F m₁✝¹ m₂✝¹).x F.W (Meas.concat F m₁✝¹ m₂✝¹).y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

c, i, c', i':

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_x: m₁✝.x F.W m₂✝.x F.W

h_y: m₁✝.y F.W m₂✝.y F.W

this: dominates F m₁✝¹ m₁✝ = true

ih₁: m₁✝¹.x F.W m₁✝¹.y F.W

ih₂: m₂✝.x F.Wm₂✝.y F.Wm₂✝¹.x F.W m₂✝¹.y F.W


left
m₁✝¹.x F.W m₂✝¹.x F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

c, i, c', i':

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_x: m₁✝.x F.W m₂✝.x F.W

h_y: m₁✝.y F.W m₂✝.y F.W

this: dominates F m₁✝¹ m₁✝ = true

ih₁: m₁✝¹.x F.W m₁✝¹.y F.W

ih₂: m₂✝.x F.Wm₂✝.y F.Wm₂✝¹.x F.W m₂✝¹.y F.W


right
m₁✝¹.y F.W m₂✝¹.y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

m₂: Meas

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝


(Meas.concat F m₁✝¹ m₂✝¹).x F.W (Meas.concat F m₁✝¹ m₂✝¹).y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

c, i, c', i':

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_x: m₁✝.x F.W m₂✝.x F.W

h_y: m₁✝.y F.W m₂✝.y F.W

this: dominates F m₁✝¹ m₁✝ = true

ih₁: m₁✝¹.x F.W m₁✝¹.y F.W

ih₂: m₂✝.x F.Wm₂✝.y F.Wm₂✝¹.x F.W m₂✝¹.y F.W


m₁✝¹.x F.W m₂✝¹.x F.W

Goals accomplished! 🐙
α: Type

F: Factory α

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

ih₂: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i, c', i':

m₂: Meas

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_eq': m₂ = Meas.concat F m₁✝ m₂✝


(Meas.concat F m₁✝¹ m₂✝¹).x F.W (Meas.concat F m₁✝¹ m₂✝¹).y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

c, i, c', i':

h_c: c c'

h_i: i i'

m₁✝¹, m₂✝¹: Meas

h₂: MeasRender F d₂✝ m₁✝¹.last i m₂✝¹

h₁: MeasRender F d₁✝ c i m₁✝¹

m₁✝, m₂✝: Meas

h₂': MeasRender F d₂✝ m₁✝.last i' m₂✝

h₁': MeasRender F d₁✝ c' i' m₁✝

h_x: m₁✝.x F.W m₂✝.x F.W

h_y: m₁✝.y F.W m₂✝.y F.W

this: dominates F m₁✝¹ m₁✝ = true

ih₁: m₁✝¹.x F.W m₁✝¹.y F.W

ih₂: m₂✝.x F.Wm₂✝.y F.Wm₂✝¹.x F.W m₂✝¹.y F.W


m₁✝¹.y F.W m₂✝¹.y F.W

Goals accomplished! 🐙
α: Type

d: Doc

c, i:

m₁: Meas

c', i':

m₂: Meas

F: Factory α

h: MeasRender F d c i m₁

h': MeasRender F d c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W
α: Type

F: Factory α

d₁✝, d₂✝: Doc

d₁_ih✝: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₁✝ c i m₁MeasRender F d₁✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

d₂_ih✝: ∀ {c i : } {m₁ : Meas} {c' i' : } {m₂ : Meas}, MeasRender F d₂✝ c i m₁MeasRender F d₂✝ c' i' m₂c c'i i'm₂.x F.Wm₂.y F.Wm₁.x F.W m₁.y F.W

c, i:

m₁: Meas

c', i':

m₂: Meas

h: MeasRender F (Doc.choice d₁✝ d₂✝) c i m₁

h': MeasRender F (Doc.choice d₁✝ d₂✝) c' i' m₂

h_c: c c'

h_i: i i'

h_x: m₂.x F.W

h_y: m₂.y F.W


m₁.x F.W m₁.y F.W

Goals accomplished! 🐙

Goals accomplished! 🐙