proposition: Lemma has_find_arrows : forall m st l (WF : Forall (has_literal m) l), Forall (has_literal m) (find_arrows st l).
proof: Proof. induction l ; simpl. - constructor. - intros. inv WF. destruct (progress_arrow a st); auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause