Theorem: ThunkOrdering.lex_left_identity (Katydid/Std/ThunkOrdering.lean)

State before:
a : Thunk Ordering
⊢ lex { fn := fun x => Ordering.eq } a = a
Tactic:
cases a <;> rfl
State after:
no goals