proposition: Lemma eval_nform : forall (REC : forall f : LForm, eval_formula f <-> eval_formula (lform f)), forall f : HFormula, eval_hformula (nform lform f) <-> eval_hformula f.
proof: Proof. intro REC. intro. unfold eval_hformula. rewrite (REC (elt f)). unfold nform. destruct (lform (elt f)). - simpl. tauto. - simpl. destruct l. simpl. rewrite eval_and_list_eq. + destruct l0. * simpl. tauto. * destruct l0. simpl. tauto. unfold elt. rewrite eval_formula_rew. unfold eval_op_list. rewrite eval_and_list_eq. tauto. + destruct l0. * simpl. tauto. * destruct l0. simpl. tauto. unfold elt. rewrite eval_formula_rew. tauto. - destruct l. simpl. tauto. unfold elt. tauto. Defined.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause