Provide an implementation for B.sum
This is needed to prove B.Sum_def_empty and B.Sum_def_non_empty
This diff is collapsed.
No preview for this file type
Please register or sign in to comment
This is needed to prove B.Sum_def_empty and B.Sum_def_non_empty