proposition: Lemma eval_extensional_eq_compat : forall p var1 var2, (forall x, list_nth x var1 false = list_nth x var2 false) -> eval var1 p = eval var2 p.
proof: Proof. intros p var1 var2 H; induction p; simpl; try_rewrite; auto. Qed.
imports: Bool PArith DecidableClass Ring Lia