proposition: Lemma eval_prd_app : forall (h k: nelist T), eval (prd i (h++k)) == @Bin.value _ _ (e_bin i) (eval (prd i h)) (eval (prd i k)).
proof: Proof. induction h; intro k. simpl; try reflexivity. simpl appne. rewrite 2 eval_prd_cons, IHh, law_assoc. reflexivity. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)