fact: Definition return_sum u n := match is_sum u with | Is_nothing => right (nil (u,n)) | Is_op l' => right (copy_mset n l') | Is_unit j => left j end.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)