proposition: Lemma in_xrev_map_filter_iff: forall [A B : Type] (p: A -> bool) (f : A -> B) (l : list A) (acc: list B) (y : B), In y (xrev_map_filter p f acc l) <-> (In y acc \/ (exists x : A, p x = true /\ f x = y /\ In x l)).
proof: Proof. induction l; simpl. - intuition. destruct H0. tauto. - intros. rewrite IHl. clear IHl. destruct (p a) eqn:Pa. + simpl. intuition subst. * firstorder. * firstorder. * firstorder congruence. apply 0%uint63. + simpl. intuition subst. firstorder. firstorder. firstorder congruence. apply 0%uint63. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause