# Library Copland.Preamble

Tactics that provide useful automation.

Ltac inv H := inversion H; clear H; subst.

Expand let expressions in both the antecedent and the
conclusion.

Ltac expand_let_pairs :=

match goal with

| |- context [let (_,_) := ?e in _] ⇒

rewrite (surjective_pairing e)

| [ H: context [let (_,_) := ?e in _] |- _ ] ⇒

rewrite (surjective_pairing e) in H

end.

Destruct disjuncts in the antecedent without naming them.