feat(logic/basic, logic/function/basic): involute ite (#4074)
Some lemmas about `ite`:
- `(d)ite_not`: exchanges the branches of an `(d)ite`
when negating the given prop.
- `involutive.ite_not`: applying an involutive function to an `ite`
negates the prop
Other changes:
Generalize the arguments for `(d)ite_apply` and `apply_(d)ite(2)`
to `Sort*` over `Type*`.
Co-authored-by: Alex J Best <alex.j.best@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
