proposition: Lemma length_zero_inv : forall l, length l = 0 -> l = nil.
proof: Proof. Proof using. intros. unfolds length. applys~ LibList.length_zero_inv. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)