fact: Definition norm_lists norm i l := let is_unit := is_unit_of i in run_list (norm_lists_ i is_unit norm l).
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)