Utilize dependent pairs more

[Engreyight]

Practically every lemma and theorem is only defined for well-formed patterns, so it would make sense to represent these patterns specifically using sig well_formed. Then wrappers may be defined for pattern operators, like this example for patt_and:

Definition patt_and_wrapper : forall (a b : sig well_formed), sig well_formed.
Proof.
  intros [a wfa] [b wfb].
  exists (a and b).
  now apply well_formed_and.
Defined.

Building the well-formedness proofs into the patterns themselves would significantly reduce, or in simpler cases possibly even eliminate, the need for providing these proofs manually (which are mostly trivial with auto and wf_auto2 anyway).

Another usecase of dependent pairs would be creating fresh variables, like this:

Definition get_fresh_evar (φ : Pattern) : sig (.∉ free_evars φ).
Proof.
  exists (fresh_evar φ); auto.
Defined.

A version for a list of patterns may be defined similarly. Not only would pose proofing this as [y Hy] be cleaner than the current remember (fresh_evar φ) as y. assert (y ∉ free_evars φ) as Hy by auto. method, it could also be used directly in a slightly modified version of total_phi_impl_phi, for example.