proposition: Lemma wf_intro_impl : forall m f acc hf l o (WF: has_form m hf) (ACC: Forall (has_literal m) acc) (EQ: hf.(elt) = f), intro_impl acc f hf = (l, o) -> Forall (has_literal m) l /\ has_oform m o.
proof: Proof. destruct f. - simpl in *. intros. destruct (is_dec hf); inv H; auto. simpl ; split ; auto. - simpl in *. intros. assert (HF: Forall (has_form m) l0). { destruct hf ; simpl in *. subst. inv WF ; auto. } destruct (is_dec hf) ; inv H; auto. rewrite Forall_rew. simpl. tauto. - simpl in *. intros. assert (HF: Forall (has_form m) l). { destruct hf ; simpl in *. subst. inv WF ; auto. } assert (HT: (has_form m) t0). { destruct hf ; simpl in *. subst. inv WF ; auto. } rewrite !xmap_rev in H. rewrite! map_rev in H. destruct (is_dec t0) ; inv H; auto. + rewrite Forall_rew. rewrite Forall_app. rewrite Forall_rev_iff. simpl. rewrite Forall_has_literal_POS. tauto. + rewrite Forall_app. rewrite Forall_rev_iff. simpl. rewrite Forall_has_literal_POS. tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause