Theorems about the widening relation

ink

theorem Widen_deterministic {d : Doc} {L₁ : List Doc} {L₂ : List Doc} (h₁ : Widen d L₁) (h₂ : Widen d L₂) : L₁ = L₂

Determinism of the widening relation (Section 3.3)

ink

theorem Widen_total {d : Doc} : ∃ L, Widen d L

Totality of the widening relation (Section 3.3)

ink

theorem Widen_choiceless {d : Doc} {D : List Doc} {d_choiceless : Doc} (h : Widen d D) (h_in : d_choiceless ∈ D) : Choiceless d_choiceless

Choicelessness of widened documents (not stated in the paper)