What is the purpose of this refactoring? The hypotheses don’t seem to change and the number of lines of code seem to increase.
I guess the main point is to prove it without destructing the schedule
Also helps in removing the seq_taks hypothesis later since now you can see it is only needed in one of the lemmas
Also I guess these lemmas I created can be used in other proofs already. For example one of the proofs above this one can use on of the lemmas in one of its goals. I will make this change and commit shortly.
added 1 commit
Compare with previous version
closed
mentioned in issue #128
