proposition: Lemma eval_suffix_compat : forall k p var1 var2, (forall i, (i < k)%positive -> list_nth i var1 false = list_nth i var2 false) -> valid k p -> eval var1 p = eval var2 p.
proof: Proof. intros k p var1 var2 Hvar Hv; revert var1 var2 Hvar. induction Hv; intros var1 var2 Hvar; simpl; [now auto|]. rewrite Hvar; [|now auto]; erewrite (IHHv1 var1 var2). + erewrite (IHHv2 var1 var2); [ring|]. intros; apply Hvar; lia. + intros; apply Hvar; lia. Qed.
imports: Bool PArith DecidableClass Ring Lia