Push negations in the goal of some assumption. For instance, given h : ¬ ∀ x, ∃ y, x ≤ y, will be transformed by push_neg at h into h : ∃ x, ∀ y, y < x. Variables names are conserved.

Matches either an identifier "h" or a pair of identifiers "h with k"

Transforms the goal into its contrapositive. contrapose turns a goal P → Q into ¬ Q → ¬ P contrapose! turns a goal P → Q into ¬ Q → ¬ P and pushes negations inside P and Q using push_neg contrapose h first reverts the local assumption h, and then uses contrapose and intro h contrapose! h first reverts the local assumption h, and then uses contrapose! and intro h contrapose h with new_h uses the name new_h for the introduced hypothesis.