proposition: Lemma filter_true : forall [A: Type] (l:list A), filter (fun _ => true) l = l.
proof: Proof. induction l ; simpl ; auto. congruence. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause