fact: Fixpoint norm u {struct u}:= match u with | sum i l => if is_commutative i then if is_idempotent i then sum' i (reduce_mset (norm_msets norm i l)) else sum' i (norm_msets norm i l) else u | prd i l => prd' i (norm_lists norm i l) | sym i l => sym i (vnorm l) | unit i => unit i end with vnorm i (l: vT i): vT i := match l with | vnil => vnil | vcons _ u l => vcons (norm u) (vnorm l) end.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)