fact: Definition is_sum (u: T) : @discr (mset T) := match u with | sum j l => if eq_idx_bool j i then Is_op l else Is_nothing | unit j => if is_unit j then Is_unit j else Is_nothing | _ => Is_nothing end.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)