proposition: Lemma build_correct: forall a A i f s t, belong i A -> belong f A -> belong s A -> belong t A -> eval i f (build a s t A) == eval i f (add a s t A).
proof: Proof. induction a; intros A i f s t Hi Hf Hs Ht; cbn - [eval]; trivial. rewrite add_zero; trivial. rewrite IHa1; auto. rewrite <- build_add; auto. rewrite IHa2; auto. apply eval_dot; trivial. rewrite IHa1; auto. rewrite <- build_add; auto. rewrite IHa2; auto. rewrite add_plus, add_comm. reflexivity. unfold add_one. rewrite <- build_add; auto. rewrite IHa; auto. apply eval_star; trivial. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing) ATBR(MxKleeneAlgebra) ATBR(DKA_Definitions) ATBR(DKA_CheckLabels) ATBR(StrictStarForm) ATBR(Utils_WF) Coq(Relations)