Skip to content

add big_sepS_elem_of_acc_impl

Ralf Jung requested to merge ralf/big_sepS_elem_of_acc_impl into master

This lemma encapsulates the useful pattern of getting access to a single element in the big-op, and at the same time changing the big-op statement but in a way that is trivial to adjust for all the other elements.

We should probably have this as well for the other big-ops, but I think I will need some help for the "2" versions... this one was already kind of nasty to figure out.^^

Merge request reports