ink

theorem Resolve_optimal_text : ∀ {α : Type} {F : Factory α} {s : String} {c i : ℕ} {ml : MeasureSet} {D : List Doc} {d_choiceless : Doc} {m : Meas}, Resolve F (Doc.text s) c i ml → Widen (Doc.text s) D → d_choiceless ∈ D → MeasRender F d_choiceless c i m → m.y ≤ F.W → m.x ≤ F.W → ∃ ms h, ml = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = true

ink

theorem Resolve_optimal_nl : ∀ {α : Type} {F : Factory α} {c i : ℕ} {ml : MeasureSet} {D : List Doc} {d_choiceless : Doc} {m : Meas}, Resolve F Doc.nl c i ml → Widen Doc.nl D → d_choiceless ∈ D → MeasRender F d_choiceless c i m → m.y ≤ F.W → m.x ≤ F.W → ∃ ms h, ml = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = true