proposition: Lemma reduce_eval_compat : forall k p var, valid k p -> eval var (reduce p) = eval var p.
proof: Proof. intros k p var H; induction H; simpl; auto. case_decide; try_rewrite; simpl. + rewrite <- reduce_aux_eval_compat; auto; inversion H3; simpl; ring. + repeat rewrite reduce_aux_eval_compat; try_rewrite; now auto. Qed.
imports: Bool PArith DecidableClass Ring Lia