proposition: Lemma eval_prd_cons a : forall (l: nelist T), eval (prd i (a::l)) == @Bin.value _ _ (e_bin i) (eval a) (eval (prd i l)).
proof: Proof. intros [|b l]; simpl; reflexivity. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)