proposition: Lemma eval_sum_nil x : eval (sum i (nil (x,xH))) == (eval x).
proof: Proof. rewrite <- sum'_sum. reflexivity. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)