proposition: Lemma remove_eq : forall A (cmp:A->A->bool) (a:A) (l:list A), is_beq cmp -> remove cmp a l = LibList.remove a l.
proof: Proof. Proof using. Local Transparent LibList.remove. introv E. unfold remove, LibList.remove. rewrites* (>> filter_eq (<> a)). { intros x. rewrite E. rew_isTrue. fequals. rew_bool_eq*. } Qed.
imports: TLC(LibTactics LibReflect)