proposition: Lemma length_rev : forall l, length (rev l) = length l.
proof: Proof. Proof using. intros. unfold length. rew_list~. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)