proposition: Lemma length_neq_inv : forall l1 l2, length l1 <> length l2 -> (l1 <> l2).
proof: Proof. Proof using. introv N E. subst*. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)