proposition: Lemma eval_prd_nil x: eval (prd i (nil x)) == eval x.
proof: Proof. rewrite <- prd'_prd. simpl. reflexivity. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)