Commit 2020-09-11 15:53 a1cbe88a

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*.

modified theorem apply_dite2

modified theorem apply_dite

modified theorem apply_ite2

modified theorem apply_ite

modified theorem dite_apply

added theorem dite_not

modified theorem ite_apply

added theorem ite_not