Skip to content

add iSplitWith tactic for convenient conjunction monotonicity

Ralf Jung requested to merge ralf/split_with into gen_proofmode

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.

Merge request reports