add iSplitWith tactic for convenient conjunction monotonicity
When dealing with logically atomic triples, a common situation is to have some hypothesis which is a conjunction, and a goal which is a conjunction, and one wants to prove the left-hand side of the goal using the left-hand side of the assumption and vice versa.
This adds a tactic to make that convenient.