proposition: Lemma intro_impl_aux : forall m f hf acc l o (WF: has_form m hf) (EQ: hf.(elt) = f), intro_impl acc f hf = (l,o) -> (Forall eval_literal l -> eval_ohformula o) <-> (Forall eval_literal acc -> eval_formula f).
proof: Proof. destruct f. - simpl; intros. destruct (is_dec hf)eqn:D. + inv H. rewrite Forall_rew. simpl. apply eval_formula_dec in WF ; auto. rewrite EQ in *. simpl in *. tauto. + inv H. simpl. unfold eval_hformula. rewrite EQ in *; simpl in *; tauto. - simpl. intros. destruct (is_dec hf)eqn:D. * assert (WF':= WF). apply eval_formula_dec in WF ; auto. rewrite EQ in WF ; simpl in WF. inv H. rewrite Forall_rew. simpl. rewrite EQ. simpl. tauto. * inv H. simpl. unfold eval_hformula. rewrite EQ. simpl. tauto. - intros. simpl in H. destruct (is_dec t0)eqn:D. + inv H. assert (HFr : has_form m t0). { inv WF; simpl in EQ ; try congruence; auto. } apply eval_formula_dec in HFr ; auto. rewrite Forall_rew. simpl. rewrite xmap_rev. rewrite Forall_app. rewrite map_rev. rewrite Forall_rev_iff. rewrite <- eval_impl_list_eq. rewrite eval_and_list_eq. rewrite eval_and_list'_Forall. rewrite Forall_eval_literal_POS. change ((fun f : t LForm => eval_formula (elt f))) with eval_hformula. tauto. + inv H. simpl. rewrite xmap_rev. rewrite Forall_app. rewrite map_rev. rewrite Forall_rev_iff. rewrite <- eval_impl_list_eq. rewrite eval_and_list_eq. rewrite eval_and_list'_Forall. rewrite Forall_eval_literal_POS. change ((fun f : t LForm => eval_formula (elt f))) with eval_hformula. tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause