Inversion lemma for formulas

[Janis-Bai]

In the current version of the library, inversion on formulas is not working as expected. In some cases, for instance, congruence falls short of closing a goal s = t given the assumption q → s = q → t with s,t,q: form.

@yforster suggested to fix this by adding the following lemma to the library (formulation and proof are due to him):

Inductive aand (P Q R : Prop) :=
      cconj : P -> Q -> R -> aand P Q R.

Lemma form_inv {Σ_funcs : funcs_signature} {Σ_preds : preds_signature} {ops : operators} {flag : falsity_flag} phi1 phi2 :
      phi1 = phi2 ->
      match phi1, phi2 with
      | falsity, falsity => True
      | atom _ P1 args1, atom _ P2 args2 => True
      | bin falsity_on o1 phi1' phi2', bin falsity_on o2 phi1'' phi2'' =>
            aand (o1 = o2) (phi1' = phi1'') (phi2' = phi2'')
      | bin falsity_off o1 phi1' phi2', bin falsity_off o2 phi1'' phi2'' =>
          aand (o1 = o2) (phi1' = phi1'') (phi2' = phi2'')
      | quant falsity_on o1 phi, quant falsity_on o2 phi' =>
            o1 = o2 /\ phi = phi'
      | quant falsity_off o1 phi, quant falsity_off o2 phi' =>
          o1 = o2 /\ phi = phi'
      | _, _ => False
      end.
Proof.
      intros H. destruct phi1; subst; eauto.
      all: destruct b; econstructor; eauto.
Qed.