fact: Definition add_to_prd u (l : @m idx (nelist T)) := match is_prd u with | Is_nothing => comp (@appne T) (nil (u)) l | Is_op l' => comp (@appne T) (l') l | Is_unit _ => l end.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)