proposition: Lemma get_polarity_rec_all_pos : forall p cl, Forall (fun l : t => pol l = true) cl -> forall b cl', Elim.get_polarity_rec p cl = Some (b, cl') -> b = true /\ Forall (fun l : t => pol l = true) cl'.
proof: Proof. intros p cl ALL. induction ALL. - simpl. discriminate. - intros. simpl in H0. destruct (get_pol p x) eqn:GP. + inv H0. apply get_pol_inv in GP. subst. destruct b; try discriminate. tauto. + destruct (Elim.get_polarity_rec p l) eqn:GP'; try discriminate. destruct p0. inv H0. specialize (IHALL _ _ eq_refl). intuition. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause