proposition: Lemma eval_op_list_lform_app : forall (REC : forall f : LForm, eval_formula f <-> eval_formula (lform f)) (o:lop) (l: list (t LForm)), eval_op_list (fun f : t LForm => eval_formula (elt f)) o l <-> eval_op_list (fun f : t LForm => eval_formula (elt f)) o (lform_app o nil (List.map (nform lform) l)).
proof: Proof. intros. replace l with (l++nil) at 1 by (rewrite app_nil_r; reflexivity). generalize (nil (A:= HCons.t LForm)). assert (forall f, eval_hformula (nform lform f) <-> eval_hformula f). { apply eval_nform; auto. } unfold eval_hformula in H. induction l. - simpl. tauto. - rewrite List.map_cons. simpl. destruct (elt (nform lform a)) eqn:EQ. + intros. rewrite! eval_op_list_cons. rewrite <- IHl. rewrite !eval_op_list_app. rewrite eval_op_list_cons. rewrite <- (H a). rewrite EQ. destruct o ; simpl; tauto. + destruct (lop_eqb o l0) eqn:OP. * apply lop_eqb_true in OP. subst. intros. rewrite <- IHl. rewrite eval_op_list_cons. rewrite! eval_op_list_app. rewrite eval_op_list_rev_append. rewrite <- (H a). rewrite EQ. simpl. destruct l0; simpl; tauto. * intros. rewrite <- IHl. rewrite eval_op_list_cons. rewrite! eval_op_list_app. rewrite eval_op_list_cons. rewrite <- (H a). rewrite EQ. simpl. destruct o; simpl; tauto. + intros. rewrite <- IHl. rewrite eval_op_list_cons. rewrite! eval_op_list_app. rewrite eval_op_list_cons. rewrite <- (H a). rewrite EQ. simpl. destruct o; simpl; tauto. Defined.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause