import Pretty.Defs.Basic
import Pretty.Tactic

/-!
## Theorems about the widening relation
-/

/--
Determinism of the widening relation (Section 3.3)
-/
theorem 
Widen_deterministic: ∀ {d : Doc} {L₁ L₂ : List Doc}, Widen d L₁ → Widen d L₂ → L₁ = L₂
Widen_deterministic (
h₁: Widen d L₁
h₁ : 
Widen: Doc → List Doc → Prop
Widen 
d: ?m.3
d 
L₁: ?m.7
L₁) (
h₂: Widen d L₂
h₂ : 
Widen: Doc → List Doc → Prop
Widen 
d: ?m.3
d 
L₂: ?m.13
L₂) : 
L₁: ?m.7
L₁ = 
L₂: ?m.13
L₂ := by
Goals accomplished! 🐙 
  
d: Doc

L₁, L₂: List Doc

h₁: Widen d L₁

h₂: Widen d L₂

L₁ = L₂induction 
d: Doc
d generalizing 
L₁: List Doc
L₁ 
L₂: List Doc
L₂
s✝: String

L₁, L₂: List Doc

h₁: Widen (Doc.text s✝) L₁

h₂: Widen (Doc.text s✝) L₂

text
L₁ = L₂
L₁, L₂: List Doc

h₁: Widen Doc.nl L₁

h₂: Widen Doc.nl L₂

nl
L₁ = L₂
d₁✝, d₂✝: Doc

d₁_ih✝: ∀ {L₁ L₂ : List Doc}, Widen d₁✝ L₁ → Widen d₁✝ L₂ → L₁ = L₂

d₂_ih✝: ∀ {L₁ L₂ : List Doc}, Widen d₂✝ L₁ → Widen d₂✝ L₂ → L₁ = L₂

L₁, L₂: List Doc

h₁: Widen (Doc.concat d₁✝ d₂✝) L₁

h₂: Widen (Doc.concat d₁✝ d₂✝) L₂

concat
L₁ = L₂
n✝: ℕ

d✝: Doc

d_ih✝: ∀ {L₁ L₂ : List Doc}, Widen d✝ L₁ → Widen d✝ L₂ → L₁ = L₂

L₁, L₂: List Doc

h₁: Widen (Doc.nest n✝ d✝) L₁

h₂: Widen (Doc.nest n✝ d✝) L₂

nest
L₁ = L₂
d✝: Doc

d_ih✝: ∀ {L₁ L₂ : List Doc}, Widen d✝ L₁ → Widen d✝ L₂ → L₁ = L₂

L₁, L₂: List Doc

h₁: Widen (Doc.align d✝) L₁

h₂: Widen (Doc.align d✝) L₂

align
L₁ = L₂
d₁✝, d₂✝: Doc

d₁_ih✝: ∀ {L₁ L₂ : List Doc}, Widen d₁✝ L₁ → Widen d₁✝ L₂ → L₁ = L₂

d₂_ih✝: ∀ {L₁ L₂ : List Doc}, Widen d₂✝ L₁ → Widen d₂✝ L₂ → L₁ = L₂

L₁, L₂: List Doc

h₁: Widen (Doc.choice d₁✝ d₂✝) L₁

h₂: Widen (Doc.choice d₁✝ d₂✝) L₂

choice
L₁ = L₂
  
d: Doc

L₁, L₂: List Doc

h₁: Widen d L₁

h₂: Widen d L₂

L₁ = L₂case text | nl => 
    
s✝: String

L₁, L₂: List Doc

h₁: Widen (Doc.text s✝) L₁

h₂: Widen (Doc.text s✝) L₂

L₁ = L₂cases 
h₁: Widen (Doc.text s✝) L₁
h₁
s✝: String

L₂: List Doc

h₂: Widen (Doc.text s✝) L₂

text
[Doc.text s✝] = L₂ 
    
s✝: String

L₁, L₂: List Doc

h₁: Widen (Doc.text s✝) L₁

h₂: Widen (Doc.text s✝) L₂

L₁ = L₂cases 
h₂: Widen (Doc.text s✝) L₂
h₂
nl.nl
[Doc.nl] = [Doc.nl]
    
s✝: String

L₁, L₂: List Doc

h₁: Widen (Doc.text s✝) L₁

h₂: Widen (Doc.text s✝) L₂

L₁ = L₂simp
Goals accomplished! 🐙
  
d: Doc

L₁, L₂: List Doc

h₁: Widen d L₁

h₂: Widen d L₂

L₁ = L₂case nest 
ih: ?m.63 d✝
ih | align 
ih: ?m.63 d✝
ih => 
    
d✝: Doc

ih: ∀ {L₁ L₂ : List Doc}, Widen d✝ L₁ → Widen d✝ L₂ → L₁ = L₂

L₁, L₂: List Doc

h₁: Widen (Doc.align d✝) L₁

h₂: Widen (Doc.align d✝) L₂

L₁ = L₂cases 
h₁: Widen (Doc.nest n✝ d✝) L₁
h₁
d✝: Doc

ih: ∀ {L₁ L₂ : List Doc}, Widen d✝ L₁ → Widen d✝ L₂ → L₁ = L₂

L₂: List Doc

h₂: Widen (Doc.align d✝) L₂

L✝: List Doc

h✝: Widen d✝ L✝

align
List.map (fun d => Doc.align d) L✝ = L₂ 
    
d✝: Doc

ih: ∀ {L₁ L₂ : List Doc}, Widen d✝ L₁ → Widen d✝ L₂ → L₁ = L₂

L₁, L₂: List Doc

h₁: Widen (Doc.align d✝) L₁

h₂: Widen (Doc.align d✝) L₂

L₁ = L₂rename_i 
h₁: Widen d✝ L✝
h₁
n✝: ℕ

d✝: Doc

ih: ∀ {L₁ L₂ : List Doc}, Widen d✝ L₁ → Widen d✝ L₂ → L₁ = L₂

L₂: List Doc

h₂: Widen (Doc.nest n✝ d✝) L₂

L✝: List Doc

h₁: Widen d✝ L✝

nest
List.map (fun d => Doc.nest n✝ d) L✝ = L₂ 
    
d✝: Doc

ih: ∀ {L₁ L₂ : List Doc}, Widen d✝ L₁ → Widen d✝ L₂ → L₁ = L₂

L₁, L₂: List Doc

h₁: Widen (Doc.align d✝) L₁

h₂: Widen (Doc.align d✝) L₂

L₁ = L₂cases 
h₂: Widen (Doc.align d✝) L₂
h₂
d✝: Doc

ih: ∀ {L₁ L₂ : List Doc}, Widen d✝ L₁ → Widen d✝ L₂ → L₁ = L₂

L✝¹: List Doc

h₁: Widen d✝ L✝¹

L✝: List Doc

h✝: Widen d✝ L✝

align.align
List.map (fun d => Doc.align d) L✝¹ = List.map (fun d => Doc.align d) L✝
    
d✝: Doc

ih: ∀ {L₁ L₂ : List Doc}, Widen d✝ L₁ → Widen d✝ L₂ → L₁ = L₂

L₁, L₂: List Doc

h₁: Widen (Doc.align d✝) L₁

h₂: Widen (Doc.align d✝) L₂

L₁ = L₂rename_i 
h₂: Widen d✝ L✝
h₂
n✝: ℕ

d✝: Doc

ih: ∀ {L₁ L₂ : List Doc}, Widen d✝ L₁ → Widen d✝ L₂ → L₁ = L₂

L✝¹: List Doc

h₁: Widen d✝ L✝¹

L✝: List Doc

h₂: Widen d✝ L✝

nest.nest
List.map (fun d => Doc.nest n✝ d) L✝¹ = List.map (fun d => Doc.nest n✝ d) L✝ 
    
d✝: Doc

ih: ∀ {L₁ L₂ : List Doc}, Widen d✝ L₁ → Widen d✝ L₂ → L₁ = L₂

L₁, L₂: List Doc

h₁: Widen (Doc.align d✝) L₁

h₂: Widen (Doc.align d✝) L₂

L₁ = L₂simp [
ih: ?m.63 d✝
ih 
h₁: Widen d✝ L✝¹
h₁ 
h₂: Widen d✝ L✝
h₂]
Goals accomplished! 🐙
  
d: Doc

L₁, L₂: List Doc

h₁: Widen d L₁

h₂: Widen d L₂

L₁ = L₂case choice 
ih_left: ?m.63 d₁✝
ih_left 
ih_right: ?m.63 d₂✝
ih_right | concat 
ih_left: ?m.63 d₁✝
ih_left 
ih_right: ?m.63 d₂✝
ih_right =>
    
d₁✝, d₂✝: Doc

ih_left: ∀ {L₁ L₂ : List Doc}, Widen d₁✝ L₁ → Widen d₁✝ L₂ → L₁ = L₂

ih_right: ∀ {L₁ L₂ : List Doc}, Widen d₂✝ L₁ → Widen d₂✝ L₂ → L₁ = L₂

L₁, L₂: List Doc

h₁: Widen (Doc.concat d₁✝ d₂✝) L₁

h₂: Widen (Doc.concat d₁✝ d₂✝) L₂

L₁ = L₂cases 
h₁: Widen (Doc.concat d₁✝ d₂✝) L₁
h₁
d₁✝, d₂✝: Doc

ih_left: ∀ {L₁ L₂ : List Doc}, Widen d₁✝ L₁ → Widen d₁✝ L₂ → L₁ = L₂

ih_right: ∀ {L₁ L₂ : List Doc}, Widen d₂✝ L₁ → Widen d₂✝ L₂ → L₁ = L₂

L₂: List Doc

h₂: Widen (Doc.concat d₁✝ d₂✝) L₂

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

concat
List.join (List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝) = L₂ 
    
d₁✝, d₂✝: Doc

ih_left: ∀ {L₁ L₂ : List Doc}, Widen d₁✝ L₁ → Widen d₁✝ L₂ → L₁ = L₂

ih_right: ∀ {L₁ L₂ : List Doc}, Widen d₂✝ L₁ → Widen d₂✝ L₂ → L₁ = L₂

L₁, L₂: List Doc

h₁: Widen (Doc.concat d₁✝ d₂✝) L₁

h₂: Widen (Doc.concat d₁✝ d₂✝) L₂

L₁ = L₂rename_i 
h_left₁: Widen d₁✝ L₁✝
h_left₁ 
h_right₁: Widen d₂✝ L₂✝
h_right₁
d₁✝, d₂✝: Doc

ih_left: ∀ {L₁ L₂ : List Doc}, Widen d₁✝ L₁ → Widen d₁✝ L₂ → L₁ = L₂

ih_right: ∀ {L₁ L₂ : List Doc}, Widen d₂✝ L₁ → Widen d₂✝ L₂ → L₁ = L₂

L₂: List Doc

h₂: Widen (Doc.choice d₁✝ d₂✝) L₂

L₁✝, L₂✝: List Doc

h_left₁: Widen d₁✝ L₁✝

h_right₁: Widen d₂✝ L₂✝

choice
L₁✝ ++ L₂✝ = L₂
    
d₁✝, d₂✝: Doc

ih_left: ∀ {L₁ L₂ : List Doc}, Widen d₁✝ L₁ → Widen d₁✝ L₂ → L₁ = L₂

ih_right: ∀ {L₁ L₂ : List Doc}, Widen d₂✝ L₁ → Widen d₂✝ L₂ → L₁ = L₂

L₁, L₂: List Doc

h₁: Widen (Doc.concat d₁✝ d₂✝) L₁

h₂: Widen (Doc.concat d₁✝ d₂✝) L₂

L₁ = L₂cases 
h₂: Widen (Doc.concat d₁✝ d₂✝) L₂
h₂
d₁✝, d₂✝: Doc

ih_left: ∀ {L₁ L₂ : List Doc}, Widen d₁✝ L₁ → Widen d₁✝ L₂ → L₁ = L₂

ih_right: ∀ {L₁ L₂ : List Doc}, Widen d₂✝ L₁ → Widen d₂✝ L₂ → L₁ = L₂

L₁✝¹, L₂✝¹: List Doc

h_left₁: Widen d₁✝ L₁✝¹

h_right₁: Widen d₂✝ L₂✝¹

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

concat.concat
List.join (List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝¹) L₁✝¹) =   List.join (List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝)
    
d₁✝, d₂✝: Doc

ih_left: ∀ {L₁ L₂ : List Doc}, Widen d₁✝ L₁ → Widen d₁✝ L₂ → L₁ = L₂

ih_right: ∀ {L₁ L₂ : List Doc}, Widen d₂✝ L₁ → Widen d₂✝ L₂ → L₁ = L₂

L₁, L₂: List Doc

h₁: Widen (Doc.concat d₁✝ d₂✝) L₁

h₂: Widen (Doc.concat d₁✝ d₂✝) L₂

L₁ = L₂rename_i 
h_left₂: Widen d₁✝ L₁✝
h_left₂ 
h_right₂: Widen d₂✝ L₂✝
h_right₂
d₁✝, d₂✝: Doc

ih_left: ∀ {L₁ L₂ : List Doc}, Widen d₁✝ L₁ → Widen d₁✝ L₂ → L₁ = L₂

ih_right: ∀ {L₁ L₂ : List Doc}, Widen d₂✝ L₁ → Widen d₂✝ L₂ → L₁ = L₂

L₁✝¹, L₂✝¹: List Doc

h_left₁: Widen d₁✝ L₁✝¹

h_right₁: Widen d₂✝ L₂✝¹

L₁✝, L₂✝: List Doc

h_left₂: Widen d₁✝ L₁✝

h_right₂: Widen d₂✝ L₂✝

choice.choice
L₁✝¹ ++ L₂✝¹ = L₁✝ ++ L₂✝
    
d₁✝, d₂✝: Doc

ih_left: ∀ {L₁ L₂ : List Doc}, Widen d₁✝ L₁ → Widen d₁✝ L₂ → L₁ = L₂

ih_right: ∀ {L₁ L₂ : List Doc}, Widen d₂✝ L₁ → Widen d₂✝ L₂ → L₁ = L₂

L₁, L₂: List Doc

h₁: Widen (Doc.concat d₁✝ d₂✝) L₁

h₂: Widen (Doc.concat d₁✝ d₂✝) L₂

L₁ = L₂simp [
ih_left: ?m.63 d₁✝
ih_left 
h_left₁: Widen d₁✝ L₁✝¹
h_left₁ 
h_left₂: Widen d₁✝ L₁✝
h_left₂, 
ih_right: ?m.63 d₂✝
ih_right 
h_right₁: Widen d₂✝ L₂✝¹
h_right₁ 
h_right₂: Widen d₂✝ L₂✝
h_right₂]
Goals accomplished! 🐙

/--
Totality of the widening relation (Section 3.3)
-/
theorem 
Widen_total: ∀ {d : Doc}, ∃ L, Widen d L
Widen_total : ∃ 
L: ?m.4755
L, 
Widen: Doc → List Doc → Prop
Widen 
d: ?m.4749
d 
L: ?m.4755
L := by
Goals accomplished! 🐙 
  
d: Doc

∃ L, Widen d Linduction 
d: Doc
d
s✝: String

text
∃ L, Widen (Doc.text s✝) L
nl
∃ L, Widen Doc.nl L
d₁✝, d₂✝: Doc

d₁_ih✝: ∃ L, Widen d₁✝ L

d₂_ih✝: ∃ L, Widen d₂✝ L

concat
∃ L, Widen (Doc.concat d₁✝ d₂✝) L
n✝: ℕ

d✝: Doc

d_ih✝: ∃ L, Widen d✝ L

nest
∃ L, Widen (Doc.nest n✝ d✝) L
d✝: Doc

d_ih✝: ∃ L, Widen d✝ L

align
∃ L, Widen (Doc.align d✝) L
d₁✝, d₂✝: Doc

d₁_ih✝: ∃ L, Widen d₁✝ L

d₂_ih✝: ∃ L, Widen d₂✝ L

choice
∃ L, Widen (Doc.choice d₁✝ d₂✝) L
  
d: Doc

∃ L, Widen d Lcase text 
s: String
s => 
    
s: String

∃ L, Widen (Doc.text s) Lexists [
Doc.text: String → Doc
Doc.text 
s: String
s]
s: String

Widen (Doc.text s) [Doc.text s]
    
s: String

∃ L, Widen (Doc.text s) Lconstructor
Goals accomplished! 🐙
  
d: Doc

∃ L, Widen d Lcase nl => 
    
∃ L, Widen Doc.nl Lexists [
Doc.nl: Doc
Doc.nl]
Widen Doc.nl [Doc.nl]
    
∃ L, Widen Doc.nl Lconstructor
Goals accomplished! 🐙
  
d: Doc

∃ L, Widen d Lcase nest 
n: ℕ
n _ 
ih: ?m.4795 d✝
ih => 
    
n: ℕ

d✝: Doc

ih: ∃ L, Widen d✝ L

∃ L, Widen (Doc.nest n d✝) Llet ⟨
L: List Doc
L, 
h: Widen d✝ L
h⟩ := 
ih: ?m.4795 d✝
ih
n: ℕ

d✝: Doc

ih: ∃ L, Widen d✝ L

L: List Doc

h: Widen d✝ L

∃ L, Widen (Doc.nest n d✝) L
    
n: ℕ

d✝: Doc

ih: ∃ L, Widen d✝ L

∃ L, Widen (Doc.nest n d✝) Lexists 
L: List Doc
L.
map: {α : Type ?u.5014} → {β : Type ?u.5013} → (α → β) → List α → List β
map (fun 
d: ?m.5023
d => 
Doc.nest: ℕ → Doc → Doc
Doc.nest 
n: ℕ
n 
d: ?m.5023
d)
n: ℕ

d✝: Doc

ih: ∃ L, Widen d✝ L

L: List Doc

h: Widen d✝ L

Widen (Doc.nest n d✝) (List.map (fun d => Doc.nest n d) L)
    
n: ℕ

d✝: Doc

ih: ∃ L, Widen d✝ L

∃ L, Widen (Doc.nest n d✝) Lconstructor
n: ℕ

d✝: Doc

ih: ∃ L, Widen d✝ L

L: List Doc

h: Widen d✝ L

h
Widen d✝ L
    
n: ℕ

d✝: Doc

ih: ∃ L, Widen d✝ L

∃ L, Widen (Doc.nest n d✝) Lassumption
Goals accomplished! 🐙
  
d: Doc

∃ L, Widen d Lcase align 
ih: ?m.4795 d✝
ih => 
    
d✝: Doc

ih: ∃ L, Widen d✝ L

∃ L, Widen (Doc.align d✝) Llet ⟨
L: List Doc
L, 
h: Widen d✝ L
h⟩ := 
ih: ?m.4795 d✝
ih
d✝: Doc

ih: ∃ L, Widen d✝ L

L: List Doc

h: Widen d✝ L

∃ L, Widen (Doc.align d✝) L
    
d✝: Doc

ih: ∃ L, Widen d✝ L

∃ L, Widen (Doc.align d✝) Lexists 
L: List Doc
L.
map: {α : Type ?u.5611} → {β : Type ?u.5610} → (α → β) → List α → List β
map (fun 
d: ?m.5619
d => 
Doc.align: Doc → Doc
Doc.align 
d: ?m.5619
d)
d✝: Doc

ih: ∃ L, Widen d✝ L

L: List Doc

h: Widen d✝ L

Widen (Doc.align d✝) (List.map (fun d => Doc.align d) L)
    
d✝: Doc

ih: ∃ L, Widen d✝ L

∃ L, Widen (Doc.align d✝) Lconstructor
d✝: Doc

ih: ∃ L, Widen d✝ L

L: List Doc

h: Widen d✝ L

h
Widen d✝ L
    
d✝: Doc

ih: ∃ L, Widen d✝ L

∃ L, Widen (Doc.align d✝) Lassumption
Goals accomplished! 🐙
  
d: Doc

∃ L, Widen d Lcase choice 
ih₁: ?m.4795 d₁✝
ih₁ 
ih₂: ?m.4795 d₂✝
ih₂ => 
    
d₁✝, d₂✝: Doc

ih₁: ∃ L, Widen d₁✝ L

ih₂: ∃ L, Widen d₂✝ L

∃ L, Widen (Doc.choice d₁✝ d₂✝) Llet ⟨
L₁: List Doc
L₁, 
h₁: Widen d₁✝ L₁
h₁⟩ := 
ih₁: ?m.4795 d₁✝
ih₁
d₁✝, d₂✝: Doc

ih₁: ∃ L, Widen d₁✝ L

ih₂: ∃ L, Widen d₂✝ L

L₁: List Doc

h₁: Widen d₁✝ L₁

∃ L, Widen (Doc.choice d₁✝ d₂✝) L
    
d₁✝, d₂✝: Doc

ih₁: ∃ L, Widen d₁✝ L

ih₂: ∃ L, Widen d₂✝ L

∃ L, Widen (Doc.choice d₁✝ d₂✝) Llet ⟨
L₂: List Doc
L₂, 
h₂: Widen d₂✝ L₂
h₂⟩ := 
ih₂: ?m.4795 d₂✝
ih₂
d₁✝, d₂✝: Doc

ih₁: ∃ L, Widen d₁✝ L

ih₂: ∃ L, Widen d₂✝ L

L₁: List Doc

h₁: Widen d₁✝ L₁

L₂: List Doc

h₂: Widen d₂✝ L₂

∃ L, Widen (Doc.choice d₁✝ d₂✝) L
    
d₁✝, d₂✝: Doc

ih₁: ∃ L, Widen d₁✝ L

ih₂: ∃ L, Widen d₂✝ L

∃ L, Widen (Doc.choice d₁✝ d₂✝) Lexists (
L₁: List Doc
L₁ ++ 
L₂: List Doc
L₂)
d₁✝, d₂✝: Doc

ih₁: ∃ L, Widen d₁✝ L

ih₂: ∃ L, Widen d₂✝ L

L₁: List Doc

h₁: Widen d₁✝ L₁

L₂: List Doc

h₂: Widen d₂✝ L₂

Widen (Doc.choice d₁✝ d₂✝) (L₁ ++ L₂)
    
d₁✝, d₂✝: Doc

ih₁: ∃ L, Widen d₁✝ L

ih₂: ∃ L, Widen d₂✝ L

∃ L, Widen (Doc.choice d₁✝ d₂✝) Ldwi { 
d₁✝, d₂✝: Doc

ih₁: ∃ L, Widen d₁✝ L

ih₂: ∃ L, Widen d₂✝ L

L₁: List Doc

h₁: Widen d₁✝ L₁

L₂: List Doc

h₂: Widen d₂✝ L₂

Widen (Doc.choice d₁✝ d₂✝) (L₁ ++ L₂)constructor
d₁✝, d₂✝: Doc

ih₁: ∃ L, Widen d₁✝ L

ih₂: ∃ L, Widen d₂✝ L

L₁: List Doc

h₁: Widen d₁✝ L₁

L₂: List Doc

h₂: Widen d₂✝ L₂

h₁
Widen d₁✝ L₁
d₁✝, d₂✝: Doc

ih₁: ∃ L, Widen d₁✝ L

ih₂: ∃ L, Widen d₂✝ L

L₁: List Doc

h₁: Widen d₁✝ L₁

L₂: List Doc

h₂: Widen d₂✝ L₂

h₂
Widen d₂✝ L₂ }
Goals accomplished! 🐙
  
d: Doc

∃ L, Widen d Lcase concat 
ih₁: ?m.4795 d₁✝
ih₁ 
ih₂: ?m.4795 d₂✝
ih₂ => 
    
d₁✝, d₂✝: Doc

ih₁: ∃ L, Widen d₁✝ L

ih₂: ∃ L, Widen d₂✝ L

∃ L, Widen (Doc.concat d₁✝ d₂✝) Llet ⟨
L₁: List Doc
L₁, 
h₁: Widen d₁✝ L₁
h₁⟩ := 
ih₁: ?m.4795 d₁✝
ih₁
d₁✝, d₂✝: Doc

ih₁: ∃ L, Widen d₁✝ L

ih₂: ∃ L, Widen d₂✝ L

L₁: List Doc

h₁: Widen d₁✝ L₁

∃ L, Widen (Doc.concat d₁✝ d₂✝) L
    
d₁✝, d₂✝: Doc

ih₁: ∃ L, Widen d₁✝ L

ih₂: ∃ L, Widen d₂✝ L

∃ L, Widen (Doc.concat d₁✝ d₂✝) Llet ⟨
L₂: List Doc
L₂, 
h₂: Widen d₂✝ L₂
h₂⟩ := 
ih₂: ?m.4795 d₂✝
ih₂
d₁✝, d₂✝: Doc

ih₁: ∃ L, Widen d₁✝ L

ih₂: ∃ L, Widen d₂✝ L

L₁: List Doc

h₁: Widen d₁✝ L₁

L₂: List Doc

h₂: Widen d₂✝ L₂

∃ L, Widen (Doc.concat d₁✝ d₂✝) L
    
d₁✝, d₂✝: Doc

ih₁: ∃ L, Widen d₁✝ L

ih₂: ∃ L, Widen d₂✝ L

∃ L, Widen (Doc.concat d₁✝ d₂✝) Lexists (
L₁: List Doc
L₁.
map: {α : Type ?u.9159} → {β : Type ?u.9158} → (α → β) → List α → List β
map (fun 
d₁: ?m.9167
d₁ => 
L₂: List Doc
L₂.
map: {α : Type ?u.9170} → {β : Type ?u.9169} → (α → β) → List α → List β
map (fun 
d₂: ?m.9179
d₂ => 
Doc.concat: Doc → Doc → Doc
Doc.concat 
d₁: ?m.9167
d₁ 
d₂: ?m.9179
d₂))).
join: {α : Type ?u.9185} → List (List α) → List α
join
d₁✝, d₂✝: Doc

ih₁: ∃ L, Widen d₁✝ L

ih₂: ∃ L, Widen d₂✝ L

L₁: List Doc

h₁: Widen d₁✝ L₁

L₂: List Doc

h₂: Widen d₂✝ L₂

Widen (Doc.concat d₁✝ d₂✝) (List.join (List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂) L₁))
    
d₁✝, d₂✝: Doc

ih₁: ∃ L, Widen d₁✝ L

ih₂: ∃ L, Widen d₂✝ L

∃ L, Widen (Doc.concat d₁✝ d₂✝) Ldwi { 
d₁✝, d₂✝: Doc

ih₁: ∃ L, Widen d₁✝ L

ih₂: ∃ L, Widen d₂✝ L

L₁: List Doc

h₁: Widen d₁✝ L₁

L₂: List Doc

h₂: Widen d₂✝ L₂

Widen (Doc.concat d₁✝ d₂✝) (List.join (List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂) L₁))constructor
d₁✝, d₂✝: Doc

ih₁: ∃ L, Widen d₁✝ L

ih₂: ∃ L, Widen d₂✝ L

L₁: List Doc

h₁: Widen d₁✝ L₁

L₂: List Doc

h₂: Widen d₂✝ L₂

h₁
Widen d₁✝ L₁
d₁✝, d₂✝: Doc

ih₁: ∃ L, Widen d₁✝ L

ih₂: ∃ L, Widen d₂✝ L

L₁: List Doc

h₁: Widen d₁✝ L₁

L₂: List Doc

h₂: Widen d₂✝ L₂

h₂
Widen d₂✝ L₂ }
Goals accomplished! 🐙

/--
Choicelessness of widened documents (not stated in the paper)
-/
-- This lemma can be made more general by not requiring `d` to be supplied,
-- but this current form suffices for our purposes.
lemma 
Widen_choiceless: ∀ {d : Doc} {D : List Doc} {d_choiceless : Doc}, Widen d D → d_choiceless ∈ D → Choiceless d_choiceless
Widen_choiceless (
h: Widen d D
h : 
Widen: Doc → List Doc → Prop
Widen 
d: ?m.11859
d 
D: ?m.11863
D) (
h_in: d_choiceless ∈ D
h_in : 
d_choiceless: ?m.11884
d_choiceless ∈ 
D: ?m.11863
D) : 
Choiceless: Doc → Prop
Choiceless 
d_choiceless: ?m.11884
d_choiceless := by
Goals accomplished! 🐙 
  
d: Doc

D: List Doc

d_choiceless: Doc

h: Widen d D

h_in: d_choiceless ∈ D

Choiceless d_choicelessinduction 
d: Doc
d generalizing 
D: List Doc
D 
d_choiceless: Doc
d_choiceless
s✝: String

D: List Doc

d_choiceless: Doc

h: Widen (Doc.text s✝) D

h_in: d_choiceless ∈ D

text
Choiceless d_choiceless
D: List Doc

d_choiceless: Doc

h: Widen Doc.nl D

h_in: d_choiceless ∈ D

nl
Choiceless d_choiceless
d₁✝, d₂✝: Doc

d₁_ih✝: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d₂_ih✝: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

D: List Doc

d_choiceless: Doc

h: Widen (Doc.concat d₁✝ d₂✝) D

h_in: d_choiceless ∈ D

concat
Choiceless d_choiceless
n✝: ℕ

d✝: Doc

d_ih✝: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d✝ D → d_choiceless ∈ D → Choiceless d_choiceless

D: List Doc

d_choiceless: Doc

h: Widen (Doc.nest n✝ d✝) D

h_in: d_choiceless ∈ D

nest
Choiceless d_choiceless
d✝: Doc

d_ih✝: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d✝ D → d_choiceless ∈ D → Choiceless d_choiceless

D: List Doc

d_choiceless: Doc

h: Widen (Doc.align d✝) D

h_in: d_choiceless ∈ D

align
Choiceless d_choiceless
d₁✝, d₂✝: Doc

d₁_ih✝: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d₂_ih✝: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

D: List Doc

d_choiceless: Doc

h: Widen (Doc.choice d₁✝ d₂✝) D

h_in: d_choiceless ∈ D

choice
Choiceless d_choiceless
  
d: Doc

D: List Doc

d_choiceless: Doc

h: Widen d D

h_in: d_choiceless ∈ D

Choiceless d_choicelesscase text | nl => 
    
s✝: String

D: List Doc

d_choiceless: Doc

h: Widen (Doc.text s✝) D

h_in: d_choiceless ∈ D

Choiceless d_choicelesscases 
h: Widen (Doc.text s✝) D
h
s✝: String

d_choiceless: Doc

h_in: d_choiceless ∈ [Doc.text s✝]

text
Choiceless d_choiceless 
    
s✝: String

D: List Doc

d_choiceless: Doc

h: Widen (Doc.text s✝) D

h_in: d_choiceless ∈ D

Choiceless d_choicelesscases 
List.eq_of_mem_singleton: ∀ {α : Type ?u.12482} {a b : α}, a ∈ [b] → a = b
List.eq_of_mem_singleton 
h_in: d_choiceless ∈ [Doc.nl]
h_in
h_in: Doc.nl ∈ [Doc.nl]

nl.refl
Choiceless Doc.nl
    
s✝: String

D: List Doc

d_choiceless: Doc

h: Widen (Doc.text s✝) D

h_in: d_choiceless ∈ D

Choiceless d_choicelessconstructor
Goals accomplished! 🐙 
  
d: Doc

D: List Doc

d_choiceless: Doc

h: Widen d D

h_in: d_choiceless ∈ D

Choiceless d_choicelesscase nest 
ih: ?m.11958 d✝
ih | align 
ih: ?m.11958 d✝
ih => 
    
d✝: Doc

ih: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d✝ D → d_choiceless ∈ D → Choiceless d_choiceless

D: List Doc

d_choiceless: Doc

h: Widen (Doc.align d✝) D

h_in: d_choiceless ∈ D

Choiceless d_choicelesscases 
h: Widen (Doc.nest n✝ d✝) D
h
d✝: Doc

ih: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L✝: List Doc

h✝: Widen d✝ L✝

h_in: d_choiceless ∈ List.map (fun d => Doc.align d) L✝

align
Choiceless d_choiceless 
    
n✝: ℕ

d✝: Doc

ih: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d✝ D → d_choiceless ∈ D → Choiceless d_choiceless

D: List Doc

d_choiceless: Doc

h: Widen (Doc.nest n✝ d✝) D

h_in: d_choiceless ∈ D

Choiceless d_choicelessrw [
n✝: ℕ

d✝: Doc

ih: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L✝: List Doc

h✝: Widen d✝ L✝

h_in: d_choiceless ∈ List.map (fun d => Doc.nest n✝ d) L✝

nest
Choiceless d_choiceless
List.mem_map: ∀ {α : Type ?u.14405} {β : Type ?u.14406} {b : β} {f : α → β} {l : List α}, b ∈ List.map f l ↔ ∃ a, a ∈ l ∧ b = f a
List.mem_map
n✝: ℕ

d✝: Doc

ih: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L✝: List Doc

h✝: Widen d✝ L✝

h_in: ∃ a, a ∈ L✝ ∧ d_choiceless = Doc.nest n✝ a

nest
Choiceless d_choiceless]
d✝: Doc

ih: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L✝: List Doc

h✝: Widen d✝ L✝

h_in: ∃ a, a ∈ L✝ ∧ d_choiceless = Doc.align a

align
Choiceless d_choiceless at 
h_in: d_choiceless ∈ List.map (fun d => Doc.nest n✝ d) L✝
h_in
n✝: ℕ

d✝: Doc

ih: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L✝: List Doc

h✝: Widen d✝ L✝

h_in: ∃ a, a ∈ L✝ ∧ d_choiceless = Doc.nest n✝ a

nest
Choiceless d_choiceless
    
n✝: ℕ

d✝: Doc

ih: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d✝ D → d_choiceless ∈ D → Choiceless d_choiceless

D: List Doc

d_choiceless: Doc

h: Widen (Doc.nest n✝ d✝) D

h_in: d_choiceless ∈ D

Choiceless d_choicelesslet ⟨
_: Doc
_, _, 
h_right: d_choiceless = Doc.align w✝
h_right⟩ := 
h_in: ∃ a, a ∈ L✝ ∧ d_choiceless = Doc.align a
h_in
d✝: Doc

ih: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L✝: List Doc

h✝: Widen d✝ L✝

h_in: ∃ a, a ∈ L✝ ∧ d_choiceless = Doc.align a

w✝: Doc

left✝: w✝ ∈ L✝

h_right: d_choiceless = Doc.align w✝

align
Choiceless d_choiceless
    
n✝: ℕ

d✝: Doc

ih: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d✝ D → d_choiceless ∈ D → Choiceless d_choiceless

D: List Doc

d_choiceless: Doc

h: Widen (Doc.nest n✝ d✝) D

h_in: d_choiceless ∈ D

Choiceless d_choicelesssubst 
h_right: d_choiceless = Doc.align w✝
h_right
d✝: Doc

ih: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L✝: List Doc

h✝: Widen d✝ L✝

w✝: Doc

left✝: w✝ ∈ L✝

h_in: ∃ a, a ∈ L✝ ∧ Doc.align w✝ = Doc.align a

align
Choiceless (Doc.align w✝) 
    
n✝: ℕ

d✝: Doc

ih: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d✝ D → d_choiceless ∈ D → Choiceless d_choiceless

D: List Doc

d_choiceless: Doc

h: Widen (Doc.nest n✝ d✝) D

h_in: d_choiceless ∈ D

Choiceless d_choicelessconstructor
n✝: ℕ

d✝: Doc

ih: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L✝: List Doc

h✝: Widen d✝ L✝

w✝: Doc

left✝: w✝ ∈ L✝

h_in: ∃ a, a ∈ L✝ ∧ Doc.nest n✝ w✝ = Doc.nest n✝ a

nest.h
Choiceless w✝ 
    
n✝: ℕ

d✝: Doc

ih: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d✝ D → d_choiceless ∈ D → Choiceless d_choiceless

D: List Doc

d_choiceless: Doc

h: Widen (Doc.nest n✝ d✝) D

h_in: d_choiceless ∈ D

Choiceless d_choicelessdwi { 
d✝: Doc

ih: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L✝: List Doc

h✝: Widen d✝ L✝

w✝: Doc

left✝: w✝ ∈ L✝

h_in: ∃ a, a ∈ L✝ ∧ Doc.align w✝ = Doc.align a

align.h
Choiceless w✝apply 
ih: ?m.11958 d✝
ih
n✝: ℕ

d✝: Doc

ih: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L✝: List Doc

h✝: Widen d✝ L✝

w✝: Doc

left✝: w✝ ∈ L✝

h_in: ∃ a, a ∈ L✝ ∧ Doc.nest n✝ w✝ = Doc.nest n✝ a

nest.h.h
Widen d✝ ?nest.h.D
n✝: ℕ

d✝: Doc

ih: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L✝: List Doc

h✝: Widen d✝ L✝

w✝: Doc

left✝: w✝ ∈ L✝

h_in: ∃ a, a ∈ L✝ ∧ Doc.nest n✝ w✝ = Doc.nest n✝ a

nest.h.h_in
w✝ ∈ ?nest.h.D
n✝: ℕ

d✝: Doc

ih: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L✝: List Doc

h✝: Widen d✝ L✝

w✝: Doc

left✝: w✝ ∈ L✝

h_in: ∃ a, a ∈ L✝ ∧ Doc.nest n✝ w✝ = Doc.nest n✝ a

nest.h.D
List Doc }
Goals accomplished! 🐙
  
d: Doc

D: List Doc

d_choiceless: Doc

h: Widen d D

h_in: d_choiceless ∈ D

Choiceless d_choicelesscase choice 
ih₁: ?m.11958 d₁✝
ih₁ 
ih₂: ?m.11958 d₂✝
ih₂ => 
    
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

D: List Doc

d_choiceless: Doc

h: Widen (Doc.choice d₁✝ d₂✝) D

h_in: d_choiceless ∈ D

Choiceless d_choicelesscases 
h: Widen (Doc.choice d₁✝ d₂✝) D
h
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: d_choiceless ∈ L₁✝ ++ L₂✝

choice
Choiceless d_choiceless 
    
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

D: List Doc

d_choiceless: Doc

h: Widen (Doc.choice d₁✝ d₂✝) D

h_in: d_choiceless ∈ D

Choiceless d_choicelessrw [
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: d_choiceless ∈ L₁✝ ++ L₂✝

choice
Choiceless d_choiceless
List.mem_append: ∀ {α : Type ?u.16059} {a : α} {s t : List α}, a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t
List.mem_append
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: d_choiceless ∈ L₁✝ ∨ d_choiceless ∈ L₂✝

choice
Choiceless d_choiceless]
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: d_choiceless ∈ L₁✝ ∨ d_choiceless ∈ L₂✝

choice
Choiceless d_choiceless at 
h_in: d_choiceless ∈ L₁✝ ++ L₂✝
h_in
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: d_choiceless ∈ L₁✝ ∨ d_choiceless ∈ L₂✝

choice
Choiceless d_choiceless
    
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

D: List Doc

d_choiceless: Doc

h: Widen (Doc.choice d₁✝ d₂✝) D

h_in: d_choiceless ∈ D

Choiceless d_choicelesscases 
h_in: d_choiceless ∈ L₁✝ ∨ d_choiceless ∈ L₂✝
h_in
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h✝: d_choiceless ∈ L₁✝

choice.inl
Choiceless d_choiceless
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h✝: d_choiceless ∈ L₂✝

choice.inr
Choiceless d_choiceless <;> [
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: d_choiceless ∈ L₁✝ ∨ d_choiceless ∈ L₂✝

choice
Choiceless d_choicelessapply 
ih₁: ?m.11958 d₁✝
ih₁
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h✝: d_choiceless ∈ L₁✝

choice.inl.h
Widen d₁✝ ?choice.inl.D
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h✝: d_choiceless ∈ L₁✝

choice.inl.h_in
d_choiceless ∈ ?choice.inl.D
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h✝: d_choiceless ∈ L₁✝

choice.inl.D
List Doc, 
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: d_choiceless ∈ L₁✝ ∨ d_choiceless ∈ L₂✝

choice
Choiceless d_choicelessapply 
ih₂: ?m.11958 d₂✝
ih₂
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h✝: d_choiceless ∈ L₂✝

choice.inr.h
Widen d₂✝ ?choice.inr.D
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h✝: d_choiceless ∈ L₂✝

choice.inr.h_in
d_choiceless ∈ ?choice.inr.D
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h✝: d_choiceless ∈ L₂✝

choice.inr.D
List Doc]
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h✝: d_choiceless ∈ L₁✝

choice.inl.h
Widen d₁✝ ?choice.inl.D
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h✝: d_choiceless ∈ L₁✝

choice.inl.h_in
d_choiceless ∈ ?choice.inl.D
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h✝: d_choiceless ∈ L₁✝

choice.inl.D
List Doc
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h✝: d_choiceless ∈ L₂✝

choice.inr.h
Widen d₂✝ ?choice.inr.D
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h✝: d_choiceless ∈ L₂✝

choice.inr.h_in
d_choiceless ∈ ?choice.inr.D
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h✝: d_choiceless ∈ L₂✝

choice.inr.D
List Doc 
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: d_choiceless ∈ L₁✝ ∨ d_choiceless ∈ L₂✝

choice
Choiceless d_choiceless<;>
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h✝: d_choiceless ∈ L₁✝

choice.inl.h
Widen d₁✝ ?choice.inl.D
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h✝: d_choiceless ∈ L₁✝

choice.inl.h_in
d_choiceless ∈ ?choice.inl.D
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h✝: d_choiceless ∈ L₁✝

choice.inl.D
List Doc
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h✝: d_choiceless ∈ L₂✝

choice.inr.h
Widen d₂✝ ?choice.inr.D
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h✝: d_choiceless ∈ L₂✝

choice.inr.h_in
d_choiceless ∈ ?choice.inr.D
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h✝: d_choiceless ∈ L₂✝

choice.inr.D
List Doc 
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: d_choiceless ∈ L₁✝ ∨ d_choiceless ∈ L₂✝

choice
Choiceless d_choicelessassumption
Goals accomplished! 🐙 
  
d: Doc

D: List Doc

d_choiceless: Doc

h: Widen d D

h_in: d_choiceless ∈ D

Choiceless d_choicelesscase concat 
ih₁: ?m.11958 d₁✝
ih₁ 
ih₂: ?m.11958 d₂✝
ih₂ => 
    
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

D: List Doc

d_choiceless: Doc

h: Widen (Doc.concat d₁✝ d₂✝) D

h_in: d_choiceless ∈ D

Choiceless d_choicelesscases 
h: Widen (Doc.concat d₁✝ d₂✝) D
h
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: d_choiceless ∈ List.join (List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝)

concat
Choiceless d_choiceless 
    
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

D: List Doc

d_choiceless: Doc

h: Widen (Doc.concat d₁✝ d₂✝) D

h_in: d_choiceless ∈ D

Choiceless d_choicelesscase concat => 
      
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: d_choiceless ∈ List.join (List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝)

Choiceless d_choicelessrw [
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: d_choiceless ∈ List.join (List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝)

Choiceless d_choiceless
List.mem_join: ∀ {α : Type ?u.16376} {a : α} {L : List (List α)}, a ∈ List.join L ↔ ∃ l, l ∈ L ∧ a ∈ l
List.mem_join
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ d_choiceless ∈ l

Choiceless d_choiceless]
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ d_choiceless ∈ l

Choiceless d_choiceless at 
h_in: d_choiceless ∈ List.join (List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝)
h_in
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ d_choiceless ∈ l

Choiceless d_choiceless
      
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: d_choiceless ∈ List.join (List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝)

Choiceless d_choicelesslet ⟨
_: List Doc
_, 
h_left: w✝ ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝
h_left, 
h_right: d_choiceless ∈ w✝
h_right⟩ := 
h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ d_choiceless ∈ l
h_in
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ d_choiceless ∈ l

w✝: List Doc

h_left: w✝ ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝

h_right: d_choiceless ∈ w✝

Choiceless d_choiceless
      
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: d_choiceless ∈ List.join (List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝)

Choiceless d_choicelessrw [
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ d_choiceless ∈ l

w✝: List Doc

h_left: w✝ ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝

h_right: d_choiceless ∈ w✝

Choiceless d_choiceless
List.mem_map: ∀ {α : Type ?u.16566} {β : Type ?u.16567} {b : β} {f : α → β} {l : List α}, b ∈ List.map f l ↔ ∃ a, a ∈ l ∧ b = f a
List.mem_map
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ d_choiceless ∈ l

w✝: List Doc

h_left: ∃ a, a ∈ L₁✝ ∧ w✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

h_right: d_choiceless ∈ w✝

Choiceless d_choiceless]
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ d_choiceless ∈ l

w✝: List Doc

h_left: ∃ a, a ∈ L₁✝ ∧ w✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

h_right: d_choiceless ∈ w✝

Choiceless d_choiceless at 
h_left: w✝ ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝
h_left
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ d_choiceless ∈ l

w✝: List Doc

h_left: ∃ a, a ∈ L₁✝ ∧ w✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

h_right: d_choiceless ∈ w✝

Choiceless d_choiceless 
      
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: d_choiceless ∈ List.join (List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝)

Choiceless d_choicelesslet ⟨
_: Doc
_, _, 
h_left_right: w✝¹ = List.map (fun d₂ => Doc.concat w✝ d₂) L₂✝
h_left_right⟩ := 
h_left: ∃ a, a ∈ L₁✝ ∧ w✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝
h_left
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ d_choiceless ∈ l

w✝¹: List Doc

h_left: ∃ a, a ∈ L₁✝ ∧ w✝¹ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

h_right: d_choiceless ∈ w✝¹

w✝: Doc

left✝: w✝ ∈ L₁✝

h_left_right: w✝¹ = List.map (fun d₂ => Doc.concat w✝ d₂) L₂✝

Choiceless d_choiceless 
      
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: d_choiceless ∈ List.join (List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝)

Choiceless d_choicelesssubst 
h_left_right: w✝¹ = List.map (fun d₂ => Doc.concat w✝ d₂) L₂✝
h_left_right
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ d_choiceless ∈ l

w✝: Doc

left✝: w✝ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

h_right: d_choiceless ∈ List.map (fun d₂ => Doc.concat w✝ d₂) L₂✝

Choiceless d_choiceless
      
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: d_choiceless ∈ List.join (List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝)

Choiceless d_choicelessrw [
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ d_choiceless ∈ l

w✝: Doc

left✝: w✝ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

h_right: d_choiceless ∈ List.map (fun d₂ => Doc.concat w✝ d₂) L₂✝

Choiceless d_choiceless
List.mem_map: ∀ {α : Type ?u.16818} {β : Type ?u.16819} {b : β} {f : α → β} {l : List α}, b ∈ List.map f l ↔ ∃ a, a ∈ l ∧ b = f a
List.mem_map
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ d_choiceless ∈ l

w✝: Doc

left✝: w✝ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

h_right: ∃ a, a ∈ L₂✝ ∧ d_choiceless = Doc.concat w✝ a

Choiceless d_choiceless]
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ d_choiceless ∈ l

w✝: Doc

left✝: w✝ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

h_right: ∃ a, a ∈ L₂✝ ∧ d_choiceless = Doc.concat w✝ a

Choiceless d_choiceless at 
h_right: d_choiceless ∈ List.map (fun d₂ => Doc.concat w✝ d₂) L₂✝
h_right
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ d_choiceless ∈ l

w✝: Doc

left✝: w✝ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

h_right: ∃ a, a ∈ L₂✝ ∧ d_choiceless = Doc.concat w✝ a

Choiceless d_choiceless 
      
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: d_choiceless ∈ List.join (List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝)

Choiceless d_choicelesslet ⟨
_: Doc
_, _, 
h_right_right: d_choiceless = Doc.concat w✝¹ w✝
h_right_right⟩ := 
h_right: ∃ a, a ∈ L₂✝ ∧ d_choiceless = Doc.concat w✝ a
h_right
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ d_choiceless ∈ l

w✝¹: Doc

left✝¹: w✝¹ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝¹ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

h_right: ∃ a, a ∈ L₂✝ ∧ d_choiceless = Doc.concat w✝¹ a

w✝: Doc

left✝: w✝ ∈ L₂✝

h_right_right: d_choiceless = Doc.concat w✝¹ w✝

Choiceless d_choiceless 
      
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: d_choiceless ∈ List.join (List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝)

Choiceless d_choicelesssubst 
h_right_right: d_choiceless = Doc.concat w✝¹ w✝
h_right_right
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

w✝¹: Doc

left✝¹: w✝¹ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝¹ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

w✝: Doc

left✝: w✝ ∈ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ Doc.concat w✝¹ w✝ ∈ l

h_right: ∃ a, a ∈ L₂✝ ∧ Doc.concat w✝¹ w✝ = Doc.concat w✝¹ a

Choiceless (Doc.concat w✝¹ w✝) 
      
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

d_choiceless: Doc

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

h_in: d_choiceless ∈ List.join (List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝)

Choiceless d_choicelessconstructor
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

w✝¹: Doc

left✝¹: w✝¹ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝¹ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

w✝: Doc

left✝: w✝ ∈ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ Doc.concat w✝¹ w✝ ∈ l

h_right: ∃ a, a ∈ L₂✝ ∧ Doc.concat w✝¹ w✝ = Doc.concat w✝¹ a

h₁
Choiceless w✝¹
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

w✝¹: Doc

left✝¹: w✝¹ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝¹ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

w✝: Doc

left✝: w✝ ∈ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ Doc.concat w✝¹ w✝ ∈ l

h_right: ∃ a, a ∈ L₂✝ ∧ Doc.concat w✝¹ w✝ = Doc.concat w✝¹ a

h₂
Choiceless w✝ <;> [
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

w✝¹: Doc

left✝¹: w✝¹ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝¹ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

w✝: Doc

left✝: w✝ ∈ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ Doc.concat w✝¹ w✝ ∈ l

h_right: ∃ a, a ∈ L₂✝ ∧ Doc.concat w✝¹ w✝ = Doc.concat w✝¹ a

Choiceless (Doc.concat w✝¹ w✝)apply 
ih₁: ?m.11958 d₁✝
ih₁
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

w✝¹: Doc

left✝¹: w✝¹ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝¹ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

w✝: Doc

left✝: w✝ ∈ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ Doc.concat w✝¹ w✝ ∈ l

h_right: ∃ a, a ∈ L₂✝ ∧ Doc.concat w✝¹ w✝ = Doc.concat w✝¹ a

h₁.h
Widen d₁✝ ?h₁.D
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

w✝¹: Doc

left✝¹: w✝¹ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝¹ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

w✝: Doc

left✝: w✝ ∈ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ Doc.concat w✝¹ w✝ ∈ l

h_right: ∃ a, a ∈ L₂✝ ∧ Doc.concat w✝¹ w✝ = Doc.concat w✝¹ a

h₁.h_in
w✝¹ ∈ ?h₁.D
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

w✝¹: Doc

left✝¹: w✝¹ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝¹ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

w✝: Doc

left✝: w✝ ∈ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ Doc.concat w✝¹ w✝ ∈ l

h_right: ∃ a, a ∈ L₂✝ ∧ Doc.concat w✝¹ w✝ = Doc.concat w✝¹ a

h₁.D
List Doc, 
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

w✝¹: Doc

left✝¹: w✝¹ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝¹ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

w✝: Doc

left✝: w✝ ∈ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ Doc.concat w✝¹ w✝ ∈ l

h_right: ∃ a, a ∈ L₂✝ ∧ Doc.concat w✝¹ w✝ = Doc.concat w✝¹ a

Choiceless (Doc.concat w✝¹ w✝)apply 
ih₂: ?m.11958 d₂✝
ih₂
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

w✝¹: Doc

left✝¹: w✝¹ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝¹ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

w✝: Doc

left✝: w✝ ∈ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ Doc.concat w✝¹ w✝ ∈ l

h_right: ∃ a, a ∈ L₂✝ ∧ Doc.concat w✝¹ w✝ = Doc.concat w✝¹ a

h₂.h
Widen d₂✝ ?h₂.D
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

w✝¹: Doc

left✝¹: w✝¹ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝¹ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

w✝: Doc

left✝: w✝ ∈ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ Doc.concat w✝¹ w✝ ∈ l

h_right: ∃ a, a ∈ L₂✝ ∧ Doc.concat w✝¹ w✝ = Doc.concat w✝¹ a

h₂.h_in
w✝ ∈ ?h₂.D
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

w✝¹: Doc

left✝¹: w✝¹ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝¹ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

w✝: Doc

left✝: w✝ ∈ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ Doc.concat w✝¹ w✝ ∈ l

h_right: ∃ a, a ∈ L₂✝ ∧ Doc.concat w✝¹ w✝ = Doc.concat w✝¹ a

h₂.D
List Doc]
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

w✝¹: Doc

left✝¹: w✝¹ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝¹ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

w✝: Doc

left✝: w✝ ∈ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ Doc.concat w✝¹ w✝ ∈ l

h_right: ∃ a, a ∈ L₂✝ ∧ Doc.concat w✝¹ w✝ = Doc.concat w✝¹ a

h₁.h
Widen d₁✝ ?h₁.D
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

w✝¹: Doc

left✝¹: w✝¹ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝¹ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

w✝: Doc

left✝: w✝ ∈ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ Doc.concat w✝¹ w✝ ∈ l

h_right: ∃ a, a ∈ L₂✝ ∧ Doc.concat w✝¹ w✝ = Doc.concat w✝¹ a

h₁.h_in
w✝¹ ∈ ?h₁.D
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

w✝¹: Doc

left✝¹: w✝¹ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝¹ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

w✝: Doc

left✝: w✝ ∈ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ Doc.concat w✝¹ w✝ ∈ l

h_right: ∃ a, a ∈ L₂✝ ∧ Doc.concat w✝¹ w✝ = Doc.concat w✝¹ a

h₁.D
List Doc
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

w✝¹: Doc

left✝¹: w✝¹ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝¹ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

w✝: Doc

left✝: w✝ ∈ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ Doc.concat w✝¹ w✝ ∈ l

h_right: ∃ a, a ∈ L₂✝ ∧ Doc.concat w✝¹ w✝ = Doc.concat w✝¹ a

h₂.h
Widen d₂✝ ?h₂.D
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

w✝¹: Doc

left✝¹: w✝¹ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝¹ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

w✝: Doc

left✝: w✝ ∈ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ Doc.concat w✝¹ w✝ ∈ l

h_right: ∃ a, a ∈ L₂✝ ∧ Doc.concat w✝¹ w✝ = Doc.concat w✝¹ a

h₂.h_in
w✝ ∈ ?h₂.D
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

w✝¹: Doc

left✝¹: w✝¹ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝¹ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

w✝: Doc

left✝: w✝ ∈ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ Doc.concat w✝¹ w✝ ∈ l

h_right: ∃ a, a ∈ L₂✝ ∧ Doc.concat w✝¹ w✝ = Doc.concat w✝¹ a

h₂.D
List Doc 
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

w✝¹: Doc

left✝¹: w✝¹ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝¹ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

w✝: Doc

left✝: w✝ ∈ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ Doc.concat w✝¹ w✝ ∈ l

h_right: ∃ a, a ∈ L₂✝ ∧ Doc.concat w✝¹ w✝ = Doc.concat w✝¹ a

Choiceless (Doc.concat w✝¹ w✝)<;>
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

w✝¹: Doc

left✝¹: w✝¹ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝¹ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

w✝: Doc

left✝: w✝ ∈ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ Doc.concat w✝¹ w✝ ∈ l

h_right: ∃ a, a ∈ L₂✝ ∧ Doc.concat w✝¹ w✝ = Doc.concat w✝¹ a

h₁.h
Widen d₁✝ ?h₁.D
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

w✝¹: Doc

left✝¹: w✝¹ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝¹ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

w✝: Doc

left✝: w✝ ∈ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ Doc.concat w✝¹ w✝ ∈ l

h_right: ∃ a, a ∈ L₂✝ ∧ Doc.concat w✝¹ w✝ = Doc.concat w✝¹ a

h₁.h_in
w✝¹ ∈ ?h₁.D
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

w✝¹: Doc

left✝¹: w✝¹ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝¹ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

w✝: Doc

left✝: w✝ ∈ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ Doc.concat w✝¹ w✝ ∈ l

h_right: ∃ a, a ∈ L₂✝ ∧ Doc.concat w✝¹ w✝ = Doc.concat w✝¹ a

h₁.D
List Doc
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

w✝¹: Doc

left✝¹: w✝¹ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝¹ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

w✝: Doc

left✝: w✝ ∈ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ Doc.concat w✝¹ w✝ ∈ l

h_right: ∃ a, a ∈ L₂✝ ∧ Doc.concat w✝¹ w✝ = Doc.concat w✝¹ a

h₂.h
Widen d₂✝ ?h₂.D
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

w✝¹: Doc

left✝¹: w✝¹ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝¹ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

w✝: Doc

left✝: w✝ ∈ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ Doc.concat w✝¹ w✝ ∈ l

h_right: ∃ a, a ∈ L₂✝ ∧ Doc.concat w✝¹ w✝ = Doc.concat w✝¹ a

h₂.h_in
w✝ ∈ ?h₂.D
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

w✝¹: Doc

left✝¹: w✝¹ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝¹ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

w✝: Doc

left✝: w✝ ∈ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ Doc.concat w✝¹ w✝ ∈ l

h_right: ∃ a, a ∈ L₂✝ ∧ Doc.concat w✝¹ w✝ = Doc.concat w✝¹ a

h₂.D
List Doc 
d₁✝, d₂✝: Doc

ih₁: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₁✝ D → d_choiceless ∈ D → Choiceless d_choiceless

ih₂: ∀ {D : List Doc} {d_choiceless : Doc}, Widen d₂✝ D → d_choiceless ∈ D → Choiceless d_choiceless

L₁✝, L₂✝: List Doc

h₁✝: Widen d₁✝ L₁✝

h₂✝: Widen d₂✝ L₂✝

w✝¹: Doc

left✝¹: w✝¹ ∈ L₁✝

h_left: ∃ a, a ∈ L₁✝ ∧ List.map (fun d₂ => Doc.concat w✝¹ d₂) L₂✝ = List.map (fun d₂ => Doc.concat a d₂) L₂✝

w✝: Doc

left✝: w✝ ∈ L₂✝

h_in: ∃ l, l ∈ List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂✝) L₁✝ ∧ Doc.concat w✝¹ w✝ ∈ l

h_right: ∃ a, a ∈ L₂✝ ∧ Doc.concat w✝¹ w✝ = Doc.concat w✝¹ a

Choiceless (Doc.concat w✝¹ w✝)assumption
Goals accomplished! 🐙