theorem CordialMiners.found_08_prefix_refl {α : Type u_1} (l : List α) : l <+: l

FOUND-08 (reflexivity): every sequence is a prefix of itself.

theorem CordialMiners.found_08_prefix_trans {α : Type u_1} {l₁ l₂ l₃ : List α} (h₁ : l₁ <+: l₂) (h₂ : l₂ <+: l₃) : l₁ <+: l₃

FOUND-08 (transitivity): prefix composes.

theorem CordialMiners.found_08_prefix_antisymm {α : Type u_1} {l₁ l₂ : List α} (h₁ : l₁ <+: l₂) (h₂ : l₂ <+: l₁) : l₁ = l₂

FOUND-08 (antisymmetry up to equality): mutual prefixes are equal. Proved from lengths so it does not depend on the exact name of a core antisymmetry lemma.

theorem CordialMiners.found_08_prefix_comparable {α : Type u_1} {l₁ l₂ l : List α} (h₁ : l₁ <+: l) (h₂ : l₂ <+: l) : l₁ <+: l₂ ∨ l₂ <+: l₁

FOUND-08 (comparability): two prefixes of a common sequence are themselves prefix-comparable. This is the core of output stability: if two correct miners' ordered outputs are each a prefix of the same limit ordering, then one output is a prefix of the other, so they never disagree on a published position.