1/1: Building SparseWith (SparseWith.idr)