First-Order Logic

Definition of first-order syntax, semantics, and deduction from the Library of Undecidability Proofs

Require Import Coq.Vectors.Vector.
Local Notation vec := t.

Require Import Equations.Equations Equations.Prop.DepElim.

(* Some preliminary definitions for substitions  *)
Definition scons {X: Type} (x : X) (xi : X) :=
   n match n with
        | 0 x
        | S n n
        end.

Definition funcomp {X Y Z} (g : Y Z) (f : X Y) :=
   x g (f x).

(* Signatures are a record to allow for easier definitions of general transformations on signatures *)

Class funcs_signature :=
  { syms : Type; ar_syms : syms }.

Coercion syms : funcs_signature >-> Sortclass.

Class preds_signature :=
  { preds : Type; ar_preds : preds }.

Coercion preds : preds_signature >-> Sortclass.

Section fix_signature.

  Context {Σ_funcs : funcs_signature}.

  (* We use the stdlib definition of vectors to be maximally compatible  *)

  Unset Elimination Schemes.

  Inductive term : Type :=
  | var : term
  | func : (f : syms), vec term (ar_syms f) term.

  Set Elimination Schemes.

  Fixpoint subst_term (σ : term) (t : term) : term :=
    match t with
    | var t σ t
    | func f v func f (map (subst_term σ) v)
    end.

  Context {Σ_preds : preds_signature}.

  (* We use a flag to switch on and off a constant for falisity *)

  Inductive falsity_flag := falsity_off | falsity_on.
  Existing Class falsity_flag.
  Existing Instance falsity_on | 1.
  Existing Instance falsity_off | 0.

  (* Syntax is parametrised in binary operators and quantifiers.
      Most developments will fix these types in the beginning and never change them.
   *)

  Class operators := {binop : Type ; quantop : Type}.
  Context {ops : operators}.

  Inductive form : falsity_flag Type :=
  | falsity : form falsity_on
  | atom {b} : (P : preds), vec term (ar_preds P) form b
  | bin {b} : binop form b form b form b
  | quant {b} : quantop form b form b.
  Arguments form {_}.

  Definition up (σ : term) := scons (var 0) (funcomp (subst_term (funcomp var S)) σ).

  Fixpoint subst_form `{falsity_flag} (σ : term) (phi : form) : form :=
    match with
    | falsity falsity
    | atom P v atom P (map (subst_term σ) v)
    | bin op bin op (subst_form σ ) (subst_form σ )
    | quant op quant op (subst_form (up σ) )
    end.

End fix_signature.

(* Setting implicit arguments is crucial  *)
(* We can write term both with and without arguments, but printing is without. *)
Arguments term _, {_}.
Arguments var _ _, {_} _.
Arguments func _ _ _, {_} _ _.
Arguments subst_term {_} _ _.

(* Formulas can be written with the signatures explicit or not.
    If the operations are explicit, the signatures are too.
 *)

Arguments form _ _ _ _, _ _ {_ _}, {_ _ _ _}, {_ _ _} _.
Arguments atom _ _ _ _, _ _ {_ _}, {_ _ _ _}.
Arguments bin _ _ _ _, _ _ {_ _}, {_ _ _ _}.
Arguments quant _ _ _ _, _ _ {_ _}, {_ _ _ _}.

Arguments up _, {_}.
Arguments subst_form _ _ _ _, _ _ {_ _}, {_ _ _ _}.

Section fix_signature.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.
  Context {ops : operators}.

  Inductive Forall {A : Type} (P : A Type) : {n}, t A n Type :=
  | Forall_nil : Forall P (@Vector.nil A)
  | Forall_cons : n (x : A) (l : t A n), P x Forall P l Forall P (@Vector.cons A x n l).

  Inductive vec_in {A : Type} (a : A) : {n}, t A n Type :=
    | vec_inB {n} (v : t A n) : vec_in a (cons A a n v)
    | vec_inS a' {n} (v : t A n) : vec_in a v vec_in a (cons A a' n v).
  Hint Constructors vec_in : core.

  Lemma term_rect' (p : term Type) :
    ( x, p (var x)) ( F v, (Forall p v) p (func F v)) (t : term), p t.
  Proof.
    intros . fix strong_term_ind' 1. destruct t as [n|F v].
    - apply .
    - apply . induction v.
      + econstructor.
      + econstructor. now eapply strong_term_ind'. eauto.
  Qed.


  Lemma term_rect (p : term Type) :
    ( x, p (var x)) ( F v, ( t, vec_in t v p t) p (func F v)) (t : term), p t.
  Proof.
    intros . eapply term_rect'.
    - apply .
    - intros. apply . intros t. induction 1; inversion X; subst; eauto.
      apply Eqdep_dec.inj_pair2_eq_dec in ; subst; eauto. decide equality.
  Qed.


  Lemma term_ind (p : term Prop) :
    ( x, p (var x)) ( F v (IH : t, In t v p t), p (func F v)) (t : term), p t.
  Proof.
    intros . eapply term_rect'.
    - apply .
    - intros. apply . intros t. induction 1; inversion X; subst; eauto.
      apply Eqdep_dec.inj_pair2_eq_dec in ; subst; eauto. decide equality.
  Qed.


End fix_signature.

Section Subst.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.
  Context {ops : operators}.

  Notation "$ x" := (var x) (at level 3, format "$ '/' x").
  Notation "t `[ sigma ]" := (subst_term t) (at level 7, left associativity, format "t '/' `[ sigma ]").
  Notation "phi [ sigma ]" := (subst_form ) (at level 7, left associativity, format "phi '/' [ sigma ]").
  Notation "s .: sigma" := (scons s ) (at level 70, right associativity).
  Notation "f >> g" := (funcomp g f) (at level 50).
  Notation "s '..'" := (scons s var) (at level 4, format "s ..").
  Notation "↑" := (S >> var).

  Lemma subst_term_ext (t : term) sigma tau :
    ( n, n = n) t`[] = t`[].
  Proof.
    intros H. induction t; cbn.
    - now apply H.
    - f_equal. now apply map_ext_in.
  Qed.


  Lemma subst_term_id (t : term) sigma :
    ( n, n = var n) t`[] = t.
  Proof.
    intros H. induction t; cbn.
    - now apply H.
    - f_equal. now erewrite map_ext_in, map_id.
  Qed.


  Lemma subst_term_var (t : term) :
    t`[var] = t.
  Proof.
    now apply subst_term_id.
  Qed.


  Lemma subst_term_comp (t : term) sigma tau :
    t`[]`[] = t`[ >> subst_term ].
  Proof.
    induction t; cbn.
    - reflexivity.
    - f_equal. rewrite map_map. now apply map_ext_in.
  Qed.


  Lemma subst_term_shift (t : term) s :
    t`[]`[s..] = t.
  Proof.
    rewrite subst_term_comp. apply subst_term_id. now intros [|].
  Qed.


  Lemma up_term (t : term) xi :
    t`[]`[up ] = t`[]`[].
  Proof.
    rewrite !subst_term_comp. apply subst_term_ext. reflexivity.
  Qed.


  Lemma up_ext sigma tau :
    ( n, n = n) n, up n = up n.
  Proof.
    destruct n; cbn; trivial.
    unfold funcomp. now rewrite H.
  Qed.


  Lemma up_var sigma :
    ( n, n = var n) n, up n = var n.
  Proof.
    destruct n; cbn; trivial.
    unfold funcomp. now rewrite H.
  Qed.


  Lemma up_funcomp sigma tau :
     n, (up >> subst_term (up )) n = up ( >> subst_term ) n.
  Proof.
    intros [|]; cbn; trivial.
    setoid_rewrite subst_term_comp.
    apply subst_term_ext. now intros [|].
  Qed.


  Lemma subst_ext {ff : falsity_flag} (phi : form) sigma tau :
    ( n, n = n) [] = [].
  Proof.
    induction in , |- *; cbn; intros H.
    - reflexivity.
    - f_equal. apply map_ext. intros s. now apply subst_term_ext.
    - now erewrite , .
    - erewrite IHphi; trivial. now apply up_ext.
  Qed.


  Lemma subst_id {ff : falsity_flag} (phi : form) sigma :
    ( n, n = var n) [] = .
  Proof.
    induction in |- *; cbn; intros H.
    - reflexivity.
    - f_equal. erewrite map_ext; try apply map_id. intros s. now apply subst_term_id.
    - now erewrite , .
    - erewrite IHphi; trivial. now apply up_var.
  Qed.


  Lemma subst_var {ff : falsity_flag} (phi : form) :
    [var] = .
  Proof.
    now apply subst_id.
  Qed.


  Lemma subst_comp {ff : falsity_flag} (phi : form) sigma tau :
    [][] = [ >> subst_term ].
  Proof.
    induction in , |- *; cbn.
    - reflexivity.
    - f_equal. rewrite map_map. apply map_ext. intros s. apply subst_term_comp.
    - now rewrite , .
    - rewrite IHphi. f_equal. now apply subst_ext, up_funcomp.
  Qed.


  Lemma subst_shift {ff : falsity_flag} (phi : form) s :
    [][s..] = .
  Proof.
    rewrite subst_comp. apply subst_id. now intros [|].
  Qed.


  Lemma up_form {ff : falsity_flag} xi psi :
    [][up ] = [][].
  Proof.
    rewrite !subst_comp. apply subst_ext. reflexivity.
  Qed.


  Lemma up_decompose {ff : falsity_flag} sigma phi :
    [up (S >> )][( 0)..] = [].
  Proof.
    rewrite subst_comp. apply subst_ext.
    intros [].
    - reflexivity.
    - apply subst_term_shift.
  Qed.


End Subst.

Require Import ListLib Lia.

Section Bounded.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.
  Context {ops : operators}.

  Inductive bounded_t n : term Prop :=
  | bounded_var x : n > x bounded_t n (var x)
  | bouded_func f v : ( t, Vector.In t v bounded_t n t) bounded_t n (func f v).

  Inductive bounded : {ff}, form ff Prop :=
  | bounded_atom ff n P v : ( t, Vector.In t v bounded_t n t) @bounded ff n (atom P v)
  | bounded_bin binop ff n phi psi : @bounded ff n @bounded ff n @bounded ff n (bin binop )
  | bounded_quant quantop ff n phi : @bounded ff (S n) @bounded ff n (quant quantop )
  | bounded_falsity n : @bounded falsity_on n falsity.

  Arguments bounded {_} _ _.

  Definition bounded_L {ff : falsity_flag} n A :=
     phi, A bounded n .

  Lemma bounded_subst_t n t sigma tau :
    ( k, n > k k = k) bounded_t n t subst_term t = subst_term t.
  Proof.
    intros H. induction 1; cbn; auto.
    f_equal. now apply Vector.map_ext_in.
  Qed.


  Lemma bounded_subst {ff : falsity_flag} {n phi sigma tau} :
    bounded n ( k, n > k k = k) subst_form = subst_form .
  Proof.
    induction 1 in , |- *; cbn; intros HN; trivial.
    - f_equal. apply Vector.map_ext_in. intros t Ht.
      eapply bounded_subst_t; try apply HN. now apply H.
    - now rewrite ( ), ( ).
    - f_equal. apply IHbounded. intros [|k] Hk; cbn; trivial.
      unfold funcomp. rewrite HN; trivial. lia.
  Qed.


  Lemma bounded_up_t {n t k} :
    bounded_t n t k n bounded_t k t.
  Proof.
    induction 1; intros Hk; constructor; try lia. firstorder.
  Qed.


  Lemma bounded_up {ff : falsity_flag} {n phi k} :
    bounded n k n bounded k .
  Proof.
    induction 1 in k |- *; intros Hk; constructor; eauto.
    - intros t Ht. eapply bounded_up_t; eauto.
    - apply IHbounded. lia.
  Qed.


  (* Derive Signature for In. *)

  Lemma find_bounded_step n (v : vec term n) :
    ( t : term, vec_in t v {n : | bounded_t n t}) { n | t, In t v bounded_t n t }.
  Proof.
    induction v; cbn; intros HV.
    - exists 0. intros t. inversion 1.
    - destruct IHv as [k Hk], (HV h) as [l Hl]; try left.
      + intros t Ht. apply HV. now right.
      + exists (k + l). intros t H. depelim H; cbn in *.
        * injection H. intros _ . apply (bounded_up_t Hl). lia.
        * injection . intros % Eqdep_dec.inj_pair2_eq_dec _; try decide equality.
          apply (bounded_up_t (Hk t H)). lia.
  Qed.


  Lemma find_bounded_t t :
    { n | bounded_t n t }.
  Proof.
    induction t using term_rect.
    - exists (S x). constructor. lia.
    - apply find_bounded_step in X as [n H]. exists n. now constructor.
  Qed.


  Lemma find_bounded {ff : falsity_flag} phi :
    { n | bounded n }.
  Proof.
    induction .
    - exists 0. constructor.
    - destruct (find_bounded_step _ t) as [n Hn].
      + eauto using find_bounded_t.
      + exists n. now constructor.
    - destruct as [n Hn], as [k Hk]. exists (n + k).
      constructor; eapply bounded_up; try eassumption; lia.
    - destruct IHphi as [n Hn]. exists n. constructor. apply (bounded_up Hn). lia.
  Qed.


  Lemma find_bounded_L {ff : falsity_flag} A :
    { n | bounded_L n A }.
  Proof.
    induction A; cbn.
    - exists 0. intros . inversion 1.
    - destruct IHA as [k Hk], (find_bounded a) as [l Hl].
      exists (k + l). intros t [|H]; eapply bounded_up; try eassumption; try (now apply Hk); lia.
  Qed.


  Fixpoint iter {X: Type} f n (x : X) :=
    match n with
      0 x
    | S m f (iter f m x)
    end.

  Fact iter_switch {X} f n x :
    f (@iter X f n x) = iter f n (f x).
  Proof.
    induction n; cbn; now try rewrite IHn.
  Qed.


  (* Lemma subst_up_var k x sigma :
    x < k -> (var x)`iter up k  = var x.
  Proof.
    induction k in x, sigma |-*.
    - now intros ?*)


End Bounded.

Inductive full_logic_sym : Type :=
| Conj : full_logic_sym
| Disj : full_logic_sym
| Impl : full_logic_sym.

Inductive full_logic_quant : Type :=
| All : full_logic_quant
| Ex : full_logic_quant.

Instance full_operators : operators :=
{| binop := full_logic_sym ; quantop := full_logic_quant |}.

Require Import List.
Require Import ListLib.

Section Deduction.

  Context {Σf : funcs_signature}.
  Context {Σp : preds_signature}.

  Notation "⊥" := falsity.
  Notation "A ∧ B" := (bin Conj A B) (at level 41).
  Notation "A ∨ B" := (FOL.bin Disj A B) (at level 42).
  Notation "A '-' B" := (FOL.bin Impl A B) (at level 43, right associativity).
  Notation "∀ Phi" := (FOL.quant All Phi) (at level 50).
  Notation "∃ Phi" := (FOL.quant Ex Phi) (at level 50).

  Notation "$ x" := (var x) (at level 3, format "$ '/' x").
  Notation "t `[ sigma ]" := (subst_term t) (at level 7, left associativity, format "t '/' `[ sigma ]").
  Notation "phi [ sigma ]" := (subst_form ) (at level 7, left associativity, format "phi '/' [ sigma ]").
  Notation "s .: sigma" := (scons s ) (at level 70, right associativity).
  Notation "f >> g" := (funcomp g f) (at level 50).
  Notation "s '..'" := (scons s var) (at level 4, format "s ..").
  Notation "↑" := (S >> var).

  Reserved Notation "A ⊢ phi" (at level 61).
  Implicit Type ff : falsity_flag.
  Inductive prv : (ff : falsity_flag), list form form Prop :=
    | II {ff} A phi psi : ::A A -->
    | IE {ff} A phi psi : A --> A A
    | AllI {ff} A phi : List.map (subst_form ) A A
    | AllE {ff} A t phi : A A [t..]
    | ExI {ff} A t phi : A [t..] A
    | ExE {ff} A phi psi : A ::(List.map (subst_form ) A) [] A
    | Exp A phi : A A
    | Ctx {ff} A phi : List.In A A
    | CI {ff} A phi psi : A A A
    | CE1 {ff} A phi psi : A A
    | CE2 {ff} A phi psi : A A
    | DI1 {ff} A phi psi : A A
    | DI2 {ff} A phi psi : A A
    | DE {ff} A phi psi theta : A ::A ::A A
  where "A ⊢ phi" := (prv _ A ).
  Notation "A ⊢ phi" := (prv _ A ).

  Context {p : falsity_flag}.

  Definition tprv T phi := A, ( psi, List.In A T ) A .

  Theorem Weak A B phi :
    A A B B .
  Proof.
    intros H. revert B.
    induction H; intros B HB; try unshelve (solve [econstructor; intuition]); try now econstructor.
  Qed.


  Hint Constructors prv : core.

  Ltac comp := repeat (progress (cbn in *; autounfold in *)).

  Theorem subst_Weak A phi xi :
    A [[] | phi A] [].
  Proof.
    induction 1 in |-*; comp.
    1-2,7-14: eauto using List.in_map.
    - apply AllI. setoid_rewrite map_map in IHprv. erewrite map_map, map_ext.
      apply IHprv. intros ?. cbn. now rewrite up_form.
    - specialize (IHprv ). apply AllE with ( := t`[]) in IHprv. rewrite subst_comp in *.
      erewrite subst_ext; try apply IHprv. intros [|]; cbn; trivial.
      unfold funcomp. now setoid_rewrite subst_term_shift.
    - specialize (IHprv ). eapply ExI with ( := t`[]). rewrite subst_comp in *.
      erewrite subst_ext; try apply IHprv. intros [|]; cbn; trivial.
      unfold funcomp. now setoid_rewrite subst_term_shift.
    - eapply ExE in . eassumption. rewrite map_map.
      specialize ( (up )). setoid_rewrite up_form in .
      erewrite map_map, map_ext in ; try apply . apply up_form.
  Qed.


  Definition cycle_shift n x :=
    if PeanoNat.Nat.eq_dec n x then $0 else $(S x).

  Lemma cycle_shift_shift n phi :
    bounded n [cycle_shift n] = [].
  Proof.
    intros H. apply (bounded_subst H). intros k. unfold cycle_shift. destruct PeanoNat.Nat.eq_dec; trivial; lia.
  Qed.


  Lemma cycle_shift_subject n phi :
    bounded (S n) [$n..][cycle_shift n] = .
  Proof.
    intros H. erewrite subst_comp, (bounded_subst H), subst_id; trivial.
    intros []; cbn; unfold cycle_shift; destruct PeanoNat.Nat.eq_dec; trivial; lia.
  Qed.


  Lemma nameless_equiv_all' A phi n :
    bounded_L n A bounded (S n) [p[] | p A] A [$n..].
  Proof.
    intros . split; intros H.
    - apply (subst_Weak _ _ ($n..)) in H. rewrite map_map in *.
      erewrite map_ext, map_id in H; try apply H. intros. apply subst_shift.
    - apply (subst_Weak _ _ (cycle_shift n)) in H. rewrite (map_ext_in _ (subst_form )) in H.
      + now rewrite cycle_shift_subject in H.
      + intros HP. now apply cycle_shift_shift, .
  Qed.


  Lemma nameless_equiv_ex' A phi psi n :
    bounded_L n A bounded n bounded (S n) (::[[] | p0 A]) [] ([$n..]::A) .
  Proof.
    intros HL Hphi Hpsi. split.
    - intros H % (subst_Weak _ _ ($n..)). cbn in *.
      rewrite map_map, (map_ext _ id), map_id in H.
      + now rewrite subst_shift in H.
      + intros. apply subst_shift.
    - intros H % (subst_Weak _ _ (cycle_shift n)). cbn in *.
      rewrite (map_ext_in _ (subst_form )) in H.
      + now rewrite cycle_shift_subject, cycle_shift_shift in H.
      + intros HT. now apply cycle_shift_shift, HL.
  Qed.


  Lemma nameless_equiv_all A phi :
    { t : term | map (subst_form ) A A [t..] }.
  Proof.
    destruct (find_bounded_L (::A)) as [n H].
    exists $n. apply nameless_equiv_all'.
    - intros ? ?. apply H. auto.
    - eapply bounded_up; try apply H; auto.
  Qed.


  Lemma nameless_equiv_ex A phi psi :
    { t : term | ( :: map (subst_form ) A) [] ([t..]::A) }.
  Proof.
    destruct (find_bounded_L (::::A)) as [n H].
    exists $n. apply nameless_equiv_ex'.
    - intros ? ?. apply H. auto.
    - apply H. auto.
    - eapply bounded_up; try apply H; auto.
  Qed.


End Deduction.

Tarski Semantics

Local Set Implicit Arguments.
Local Unset Strict Implicit.

Section Tarski.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.

  (* Semantic notions *)

  Section Semantics.

    Variable domain : Type.

    Class interp := B_I
      {
        i_func : f : syms, vec domain (ar_syms f) domain ;
        i_atom : P : preds, vec domain (ar_preds P) Prop ;
      }.

    Definition env := domain.

    Context {I : interp}.

    Fixpoint eval (rho : env) (t : term) : domain :=
      match t with
      | var s s
      | func f v i_func (Vector.map (eval ) v)
      end.

    Fixpoint sat {ff : falsity_flag} (rho : env) (phi : form) : Prop :=
      match with
      | atom P v i_atom (Vector.map (eval ) v)
      | falsity False
      | bin Impl sat sat
      | bin Conj sat sat
      | bin Disj sat sat
      | quant All d : domain, sat (scons d )
      | quant Ex d : domain, sat (scons d )
      end.

  End Semantics.

End Tarski.

Arguments sat {_ _ _ _ _} _ _, {_ _ _} _ {_} _ _.
Arguments interp {_ _} _, _ _ _.

Notation "p ⊨ phi" := (sat _ p ) (at level 20).

(* ** Discreteness *)

Require Import EqdepFacts.
Require Import Decidable.

Lemma inj_pair2_eq_dec' A :
  eq_dec A (P : A Type) (p : A) (x y : P p), existT P p x = existT P p y x = y.
Proof.
  apply Eqdep_dec.inj_pair2_eq_dec.
Qed.


Ltac resolve_existT := try
  match goal with
     | [ : @existT ?X _ _ _ = existT _ _ _ |- _ ] eapply Eqdep_dec.inj_pair2_eq_dec in ;
                                                      [subst | try (eauto || now intros; decide equality)]
  end.

Lemma dec_vec_in X n (v : vec X n) :
  ( x, vec_in x v y, dec (x = y)) v', dec (v = v').
Proof with subst; try (now left + (right; intros[=])).
  intros Hv. induction v; intros v'; dependent elimination v'...
  destruct (Hv h (vec_inB h v) )... edestruct IHv.
  - intros x H. apply Hv. now right.
  - left. f_equal. apply e.
  - right. intros H. inversion H. resolve_existT. tauto.
Qed.


Instance dec_vec X {HX : eq_dec X} n : eq_dec (vec X n).
Proof.
  intros v. now apply dec_vec_in.
Qed.


Section EqDec.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.
  Context {ops : operators}.

  Hypothesis eq_dec_Funcs : eq_dec syms.
  Hypothesis eq_dec_Preds : eq_dec preds.
  Hypothesis eq_dec_binop : eq_dec binop.
  Hypothesis eq_dec_quantop : eq_dec quantop.

  Global Instance dec_term : eq_dec term.
  Proof with subst; try (now left + (right; intros[=]; resolve_existT; congruence)).
    intros t. induction t as [ | ]; intros [|? v']...
    - decide (x = n)...
    - decide (F = f)... destruct (dec_vec_in X v')...
  Qed.


  Instance dec_falsity : eq_dec falsity_flag.
  Proof.
    intros b b'. unfold dec. decide equality.
  Qed.


  Lemma eq_dep_falsity b phi psi :
    eq_dep falsity_flag (@form Σ_funcs Σ_preds ops) b b = .
  Proof.
    rewrite eq_sigT_iff_eq_dep. split.
    - intros H. resolve_existT. reflexivity.
    - intros . reflexivity.
  Qed.


  Lemma dec_form_dep {b1 b2} phi1 phi2 : dec (eq_dep falsity_flag (@form _ _ _) ).
  Proof with subst; try (now left + (right; intros ? % eq_sigT_iff_eq_dep; resolve_existT; congruence)).
    unfold dec. revert ; induction ; intros; try destruct .
    all: try now right; inversion 1. now left.
    - decide (b = )... decide (P = )... decide (t = )... right.
      intros [=] % eq_dep_falsity. resolve_existT. tauto.
    - decide (b = )... decide ( = )... destruct (IHphi1_1 phi2_1).
      + apply eq_dep_falsity in e as . destruct (IHphi1_2 phi2_2).
        * apply eq_dep_falsity in e as . now left.
        * right. rewrite eq_dep_falsity in *. intros [=]. now resolve_existT.
      + right. rewrite eq_dep_falsity in *. intros [=]. now repeat resolve_existT.
    - decide (b = )... decide (q = )... destruct ( ).
      + apply eq_dep_falsity in e as . now left.
      + right. rewrite eq_dep_falsity in *. intros [=]. now resolve_existT.
  Qed.


  Global Instance dec_form {ff : falsity_flag} : eq_dec form.
  Proof.
    intros . destruct (dec_form_dep ); rewrite eq_dep_falsity in *; firstorder.
  Qed.


End EqDec.