proposition: Lemma eval_formula_dec : forall m f, has_form m f -> is_dec f = true -> eval_formula f.(elt) \/ ~ eval_formula f.(elt).
proof: Proof. intros m f IND. remember (f.(elt)) as f' eqn:EQ. revert f EQ IND. induction f' using form_ind. - simpl. intros. inv IND ; simpl in EQ ; subst ; simpl in *; try congruence. inv EQ. auto. - intros. destruct f ; simpl in EQ ; inv EQ. inv IND. simpl in *. apply eval_op_list_dec. rewrite Forall_forall in H6. apply Forall_forall. intros. apply H with (f:=x); auto. rewrite forallb_forall in H0. apply H0; auto. - intros. destruct f ; simpl in EQ ; inv EQ. inv IND. simpl in *. rewrite andb_true_iff in H0. destruct H0 as (H1L & H1R). apply eval_impl_list_dec. rewrite Forall_forall in H6. apply Forall_forall. intros. apply H with (f:=x); auto. rewrite forallb_forall in H1L. auto. eapply IHf';eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause