proposition: Lemma count_rev : forall P l, count P (rev l) = count P l.
proof: Proof. Proof using. gowith LibList.count_rev. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)