Theorem: LoVe.list.length.Preorder_example (LoVe/Lectures/LoVe13_BasicMathematicalStructures_Demo.lean)

State before:
⊢ [1] > []
Tactic:
decide
State after:
no goals