proposition: Lemma Forall_rev_iff : forall {A: Type} (P: A -> Prop) l, Forall P (rev l) <-> Forall P l.
proof: Proof. intros. induction l. - simpl. tauto. - simpl. rewrite Forall_app. rewrite (Forall_rew (a::nil)). rewrite (Forall_rew (a::l)). rewrite (Forall_rew nil). tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause