Determinism of resolving theorems

ink

theorem Resolve_deterministic : ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {ms₁ ms₂ : MeasureSet}, Resolve F d c i ms₁ → Resolve F d c i ms₂ → ms₁ = ms₂

The determinism of resolving (Page 19, Section 5.6)

ink

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

ink

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