proposition: Lemma prd'_prd : forall (l: nelist T), eval (prd' i l) == eval (prd i l).
proof: Proof. intros [?|? [|? ?]]; simpl; reflexivity. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)