proposition: Lemma eval_0' : forall P, P =? 0 = true -> forall vs, eval vs P = 0.
proof: Proof. induction P;simpl;intros E vs. - change eqb with Peqb in E;simpl in E. apply decide_eqb_ok in E. rewrite E. apply preserves_0. - change eqb with Peqb in E;simpl in E. destruct (false_ne_true E). Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.additional_operations HoTT.Classes.tactics.ring_quote HoTT.Classes.theory.rings