proposition: Lemma eval_norm_lists i (Hnorm: forall u, eval (norm u) == eval u) : forall h, eval (prd i (norm_lists norm i h)) == eval (prd i h).
proof: Proof. unfold norm_lists. assert (H : forall h : nelist T, eval (prd i (run_list (norm_lists_ i (is_unit_of i) norm h))) == eval (prd i h) /\ compat_prd_unit (is_unit_of i) (norm_lists_ i (is_unit_of i) norm h)). { induction h as [a | a h [IHh IHh']]; simpl norm_lists_; split. rewrite z1'. simpl. apply Hnorm. apply compat_prd_unit_return. rewrite z2'. rewrite IHh. rewrite eval_prd_cons. rewrite Hnorm. reflexivity. apply is_unit_of_Unit. auto. apply compat_prd_unit_add. auto. } apply H. Defined.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)