Lemmas 6 and 9 should be formulated differently.

[afck]

Maybe I'm misreading them but in their current form they look wrong to me:

Lemma 6 states that every protocol state's messages are totally ordered.
The proof correctly shows that there is a function f : S → ℕ assigning to each message the size of its justification, and that the relation m ≼ n can be defined as f(m) ≥ f(n), but that doesn't imply that ≼ is a total order itself, since f usually won't be injective, and therefore ≼ isn't necessarily antisymmetric.
Maybe the intention of the lemma is to say that (S, ≼) is a total order whenever S is a set of messages that are all from the same, non-equivocating validator?

The proof of Lemma 9 states that due to the "Well-Ordering Principle, a non-empty countable total order always has a minimal element". That's not true (e.g. (ℤ, ≤)), but it's also unneeded: Every finite, partially ordered non-empty set has at least one minimal element, which is sufficient for Lemma 9.