From Coq Require Import Btauto.

From MatchingLogic Require Export
    DerivedOperators_Syntax
    IndexManipulation
.

Import MatchingLogic.Substitution.Notations.


Section with_signature.
  Context {Σ : Signature}.

  Record SpecificSubst {A : Type} : Type := {
      increase_ex : A → A;
      increase_mu : A → A;
      on_fevar : A → evar → Pattern;
      on_fsvar : A → svar → Pattern;
      on_bevar : A → db_index → Pattern;
      on_bsvar : A → db_index → Pattern;
  }.

  Fixpoint apply_subst {A : Type} (s : SpecificSubst) (st : A) (phi : Pattern) :=
    match phi with
    | patt_free_evar x ⇒ on_fevar s st x
    | patt_free_svar X ⇒ on_fsvar s st X
    | patt_bound_evar n ⇒ on_bevar s st n
    | patt_bound_svar N ⇒ on_bsvar s st N
    | patt_sym sm ⇒ patt_sym sm
    | patt_app phi1 phi2 ⇒ patt_app (apply_subst s st phi1) (apply_subst s st phi2)
    | patt_bott ⇒ patt_bott
    | patt_imp phi1 phi2 ⇒ patt_imp (apply_subst s st phi1) (apply_subst s st phi2)
    | patt_exists phi' ⇒ patt_exists (apply_subst s (increase_ex s st) phi')
    | patt_mu phi' ⇒ patt_mu (apply_subst s (increase_mu s st) phi')
    end.

  Class PatternMorphism {A : Type} (f : A → Pattern → Pattern) := {
      pm_spec_data : SpecificSubst ;
      pm_ezero_increase : ∀ a,
        on_bevar pm_spec_data (increase_ex pm_spec_data a) 0 = patt_bound_evar 0 ;
      pm_szero_increase : ∀ a,
        on_bsvar pm_spec_data (increase_mu pm_spec_data a) 0 = patt_bound_svar 0 ;
      pm_correctness : ∀ a (phi : Pattern), f a phi = apply_subst pm_spec_data a phi
  }.

  #[global]
  Program Instance Evar_quantify_morphism (x' : evar) :
     PatternMorphism (evar_quantify x') := {
    pm_spec_data := {|
      increase_ex := fun x ⇒ S x ;
      increase_mu := id ;
      on_fevar := fun level x ⇒ if decide (x' = x)
                                 then patt_bound_evar level
                                 else patt_free_evar x;
      on_fsvar := fun _ X ⇒ patt_free_svar X;
      on_bevar := fun _ n ⇒ patt_bound_evar n;
      on_bsvar := fun _ N ⇒ patt_bound_svar N;
    |}
  }.

  #[global]
  Program Instance Svar_quantify_morphism (x' : svar) :
     PatternMorphism (svar_quantify x') := {
    pm_spec_data := {|
      increase_ex := id;
      increase_mu := fun x ⇒ S x ;
      on_fevar := fun _ X ⇒ patt_free_evar X;
      on_fsvar := fun level x ⇒ if decide (x' = x)
                                 then patt_bound_svar level
                                 else patt_free_svar x;
      on_bevar := fun _ n ⇒ patt_bound_evar n;
      on_bsvar := fun _ N ⇒ patt_bound_svar N;
    |}
  }.

  #[global]
  Program Instance Bevar_subst_morphism (ψ : Pattern) :
     PatternMorphism (bevar_subst ψ) := {
    pm_spec_data := {|
      increase_ex := fun x ⇒ S x ;
      increase_mu := id ;
      on_fevar := fun _ x ⇒ patt_free_evar x;
      on_fsvar := fun _ X ⇒ patt_free_svar X;
      on_bevar := fun x n ⇒
        match compare_nat n x with
        | Nat_less _ _ _ ⇒ patt_bound_evar n
        | Nat_equal _ _ _ ⇒ ψ
        | Nat_greater _ _ _ ⇒ patt_bound_evar (Nat.pred n)
        end;
      on_bsvar := fun _ N ⇒ patt_bound_svar N;
    |}
  }.

  #[global]
  Program Instance Bsvar_subst_morphism (ψ : Pattern) :
     PatternMorphism (bsvar_subst ψ) := {
    pm_spec_data := {|
      increase_ex := id ;
      increase_mu := fun x ⇒ S x ;
      on_fevar := fun _ x ⇒ patt_free_evar x;
      on_fsvar := fun _ X ⇒ patt_free_svar X;
      on_bevar := fun _ n ⇒ patt_bound_evar n;
      on_bsvar := fun X N ⇒
        match compare_nat N X with
        | Nat_less _ _ _ ⇒ patt_bound_svar N
        | Nat_equal _ _ _ ⇒ ψ
        | Nat_greater _ _ _ ⇒ patt_bound_svar (Nat.pred N)
        end;
    |}
  }.

  #[global]
  Program Instance Evar_open_morphism (x : evar) :
     PatternMorphism (evar_open x) := {
    pm_spec_data := {|
      increase_ex := fun x ⇒ S x ;
      increase_mu := id ;
      on_fevar := fun _ x ⇒ patt_free_evar x;
      on_fsvar := fun _ X ⇒ patt_free_svar X;
      on_bevar := fun dbi n ⇒
        match compare_nat n dbi with
        | Nat_less _ _ _ ⇒ patt_bound_evar n
        | Nat_equal _ _ _ ⇒ patt_free_evar x
        | Nat_greater _ _ _ ⇒ patt_bound_evar (Nat.pred n)
        end;
      on_bsvar := fun _ N ⇒ patt_bound_svar N;
    |}
  }.

  #[global]
  Program Instance Svar_open_morphism (X : svar) :
     PatternMorphism (svar_open X) := {
    pm_spec_data := {|
      increase_ex := id ;
      increase_mu := fun x ⇒ S x ;
      on_fevar := fun _ x ⇒ patt_free_evar x;
      on_fsvar := fun _ X ⇒ patt_free_svar X;
      on_bevar := fun _ n ⇒ patt_bound_evar n;
      on_bsvar := fun Dbi N ⇒
        match compare_nat N Dbi with
        | Nat_less _ _ _ ⇒ patt_bound_svar N
        | Nat_equal _ _ _ ⇒ patt_free_svar X
        | Nat_greater _ _ _ ⇒ patt_bound_svar (Nat.pred N)
        end;
    |}
  }.

  #[global]
  Program Instance Free_evar_subst_morphism (ψ : Pattern) :
     PatternMorphism (free_evar_subst ψ) := {
    pm_spec_data := {|
      increase_ex := id ;
      increase_mu := id ;
      on_fevar := fun x x' ⇒ if decide (x = x') then ψ else patt_free_evar x';
      on_fsvar := fun _ X ⇒ patt_free_svar X;
      on_bevar := fun _ n ⇒ patt_bound_evar n;
      on_bsvar := fun _ N ⇒ patt_bound_svar N;
    |}
  }.

  #[global]
  Program Instance Free_svar_subst_morphism (ψ : Pattern) :
     PatternMorphism (free_svar_subst ψ) := {
    pm_spec_data := {|
      increase_ex := id ;
      increase_mu := id ;
      on_fevar := fun _ x ⇒ patt_free_evar x ;
      on_fsvar := fun X X' ⇒ if decide (X = X') then ψ else patt_free_svar X';
      on_bevar := fun _ n ⇒ patt_bound_evar n;
      on_bsvar := fun _ N ⇒ patt_bound_svar N;
    |}
  }.

Class Binary (binary : Pattern → Pattern → Pattern) := {
    binary_morphism :
      ∀ {A : Type} (f : A → Pattern → Pattern) (f_morph : PatternMorphism f) (phi1 phi2 : Pattern) a,
        f a (binary phi1 phi2) = binary (f a phi1) (f a phi2) ;
    binary_wfp :
      ∀ (ψ1 ψ2 : Pattern),
        well_formed_positive (binary ψ1 ψ2)
        = well_formed_positive ψ1 && well_formed_positive ψ2 ;
    binary_wfcex :
      ∀ (n : nat) (ψ1 ψ2 : Pattern),
            well_formed_closed_ex_aux (binary ψ1 ψ2) n
            = well_formed_closed_ex_aux ψ1 n && well_formed_closed_ex_aux ψ2 n ;
    binary_wfcmu :
      ∀ (n : nat) (ψ1 ψ2 : Pattern),
            well_formed_closed_mu_aux (binary ψ1 ψ2) n
            = well_formed_closed_mu_aux ψ1 n && well_formed_closed_mu_aux ψ2 n ;
}.

Lemma binary_wfxy
  (binary : Pattern → Pattern → Pattern)
  {_b : Binary binary}
:
∀ (x y : nat) (ψ1 ψ2 : Pattern),
  well_formed_xy x y (binary ψ1 ψ2)
  = well_formed_xy x y ψ1 && well_formed_xy x y ψ2.

Lemma binary_wfxy_compose
  (binary : Pattern → Pattern → Pattern)
  {_b : Binary binary}
:
∀ (x y : nat) (ψ1 ψ2 : Pattern),
  well_formed_xy x y ψ1 = true ∧ well_formed_xy x y ψ2 = true →
  well_formed_xy x y (binary ψ1 ψ2) = true
.

Lemma binary_wfxy_decompose
  (binary : Pattern → Pattern → Pattern)
  {_b : Binary binary}
:
∀ (x y : nat) (ψ1 ψ2 : Pattern),
  well_formed_xy x y (binary ψ1 ψ2) = true →
  well_formed_xy x y ψ1 = true ∧ well_formed_xy x y ψ2 = true
.

Class Ternary (ternary : Pattern → Pattern → Pattern → Pattern) := {
    ternary_morphism :
      ∀ {A : Type} (f : A → Pattern → Pattern) (f_morph : PatternMorphism f) (phi1 phi2 phi3 : Pattern) a,
        f a (ternary phi1 phi2 phi3) =
          ternary (f a phi1) (f a phi2) (f a phi3);
    ternary_wfp :
      ∀ (ψ1 ψ2 ψ3: Pattern),
        well_formed_positive (ternary ψ1 ψ2 ψ3)
        = well_formed_positive ψ1 &&
          well_formed_positive ψ2 &&
          well_formed_positive ψ3 ;
    ternary_wfcex :
      ∀ (n : nat) (ψ1 ψ2 ψ3 : Pattern),
            well_formed_closed_ex_aux (ternary ψ1 ψ2 ψ3) n
            = well_formed_closed_ex_aux ψ1 n &&
              well_formed_closed_ex_aux ψ2 n &&
              well_formed_closed_ex_aux ψ3 n ;
    ternary_wfcmu :
      ∀ (n : nat) (ψ1 ψ2 ψ3 : Pattern),
            well_formed_closed_mu_aux (ternary ψ1 ψ2 ψ3) n
            = well_formed_closed_mu_aux ψ1 n &&
              well_formed_closed_mu_aux ψ2 n &&
              well_formed_closed_mu_aux ψ3 n;
}.

Lemma ternary_wfxy
  (ternary : Pattern → Pattern → Pattern → Pattern)
  {_b : Ternary ternary}
:
∀ (x y : nat) (ψ1 ψ2 ψ3 : Pattern),
  well_formed_xy x y (ternary ψ1 ψ2 ψ3)
  = well_formed_xy x y ψ1 && well_formed_xy x y ψ2 && well_formed_xy x y ψ3.

Lemma ternary_wfxy_compose
  (ternary : Pattern → Pattern → Pattern → Pattern)
  {_b : Ternary ternary}
:
∀ (x y : nat) (ψ1 ψ2 ψ3 : Pattern),
  well_formed_xy x y ψ1 = true ∧
  well_formed_xy x y ψ2 = true ∧
  well_formed_xy x y ψ3 = true →
  well_formed_xy x y (ternary ψ1 ψ2 ψ3) = true
.

Lemma ternary_wfxy_decompose
  (ternary : Pattern → Pattern → Pattern → Pattern)
  {_b : Ternary ternary}
:
∀ (x y : nat) (ψ1 ψ2 ψ3 : Pattern),
  well_formed_xy x y (ternary ψ1 ψ2 ψ3) = true →
  well_formed_xy x y ψ1 = true ∧ well_formed_xy x y ψ2 = true ∧ well_formed_xy x y ψ3 = true
.

Class Quaternary (quaternary : Pattern → Pattern → Pattern → Pattern → Pattern) := {
    quaternary_morphism :
      ∀ {A : Type} (f : A → Pattern → Pattern) (f_morph : PatternMorphism f) (phi1 phi2 phi3 phi4 : Pattern) a,
        f a (quaternary phi1 phi2 phi3 phi4) =
          quaternary (f a phi1) (f a phi2) (f a phi3) (f a phi4);
    quaternary_wfp :
      ∀ (ψ1 ψ2 ψ3 ψ4: Pattern),
        well_formed_positive (quaternary ψ1 ψ2 ψ3 ψ4)
        = well_formed_positive ψ1 &&
          well_formed_positive ψ2 &&
          well_formed_positive ψ3 &&
          well_formed_positive ψ4 ;
    quaternary_wfcex :
      ∀ (n : nat) (ψ1 ψ2 ψ3 ψ4 : Pattern),
            well_formed_closed_ex_aux (quaternary ψ1 ψ2 ψ3 ψ4) n
            = well_formed_closed_ex_aux ψ1 n &&
              well_formed_closed_ex_aux ψ2 n &&
              well_formed_closed_ex_aux ψ3 n &&
              well_formed_closed_ex_aux ψ4 n ;
    quaternary_wfcmu :
      ∀ (n : nat) (ψ1 ψ2 ψ3 ψ4 : Pattern),
            well_formed_closed_mu_aux (quaternary ψ1 ψ2 ψ3 ψ4) n
            = well_formed_closed_mu_aux ψ1 n &&
              well_formed_closed_mu_aux ψ2 n &&
              well_formed_closed_mu_aux ψ3 n &&
              well_formed_closed_mu_aux ψ4 n;
}.

Lemma quaternary_wfxy
  (quaternary : Pattern → Pattern → Pattern → Pattern → Pattern)
  {_b : Quaternary quaternary}
:
∀ (x y : nat) (ψ1 ψ2 ψ3 ψ4 : Pattern),
  well_formed_xy x y (quaternary ψ1 ψ2 ψ3 ψ4)
  = well_formed_xy x y ψ1 && well_formed_xy x y ψ2 && well_formed_xy x y ψ3 && well_formed_xy x y ψ4.

Lemma quaternary_wfxy_compose
  (quaternary : Pattern → Pattern → Pattern → Pattern → Pattern)
  {_b : Quaternary quaternary}
:
∀ (x y : nat) (ψ1 ψ2 ψ3 ψ4 : Pattern),
  well_formed_xy x y ψ1 = true ∧
  well_formed_xy x y ψ2 = true ∧
  well_formed_xy x y ψ3 = true ∧
  well_formed_xy x y ψ4 = true →
  well_formed_xy x y (quaternary ψ1 ψ2 ψ3 ψ4) = true
.

Lemma quaternary_wfxy_decompose
  (quaternary : Pattern → Pattern → Pattern → Pattern → Pattern)
  {_b : Quaternary quaternary}
:
∀ (x y : nat) (ψ1 ψ2 ψ3 ψ4 : Pattern),
  well_formed_xy x y (quaternary ψ1 ψ2 ψ3 ψ4) = true →
  well_formed_xy x y ψ1 = true ∧ well_formed_xy x y ψ2 = true ∧ well_formed_xy x y ψ3 = true ∧ well_formed_xy x y ψ4 = true
.

Class Unary (unary : Pattern → Pattern) := {
    unary_morphism :
      ∀ {A : Type} (f : A → Pattern → Pattern) (f_morph : PatternMorphism f) (phi : Pattern) a,
        f a (unary phi) = unary (f a phi) ;
    unary_wfp :
      ∀ (ψ : Pattern),
        well_formed_positive (unary ψ) = well_formed_positive ψ ;
    unary_wfcex :
      ∀ (n : nat) (ψ : Pattern),
        well_formed_closed_ex_aux (unary ψ) n = well_formed_closed_ex_aux ψ n ;
    unary_wfcmu :
      ∀ (n : nat) (ψ : Pattern),
        well_formed_closed_mu_aux (unary ψ) n = well_formed_closed_mu_aux ψ n ;
}.

Lemma unary_wfxy (unary : Pattern → Pattern) {_ : Unary unary} :
∀ (x y : nat) (ψ : Pattern),
  well_formed_xy x y (unary ψ) = well_formed_xy x y ψ
.

Lemma unary_wfxy_compose (unary : Pattern → Pattern) {_uu : Unary unary} :
∀ (x y : nat) (ψ : Pattern),
  well_formed_xy x y ψ = true →
  well_formed_xy x y (unary ψ) = true
.

Lemma unary_wfxy_decompose (unary : Pattern → Pattern) {_ : Unary unary} :
∀ (x y : nat) (ψ : Pattern),
  well_formed_xy x y (unary ψ) = true →
  well_formed_xy x y ψ = true
.

Class Nullary (nullary : Pattern) := {
    nullary_morphism :
      ∀ {A : Type} (f : A → Pattern → Pattern) (f_morph : PatternMorphism f) a,
        f a nullary = nullary ;
    nullary_wfp : well_formed_positive nullary = true;
    nullary_wfcex : ∀ (n : nat), well_formed_closed_ex_aux nullary n = true;
    nullary_wfcmu : ∀ (n : nat), well_formed_closed_mu_aux nullary n = true;
}.

Lemma nullary_wfxy (nullary : Pattern) {_ : Nullary nullary} :
  ∀ (x y : nat), well_formed_xy x y nullary = true
.

Lemma well_formed_positive_foldr_binary
  (binary : Pattern → Pattern → Pattern)
  {_bin : Binary binary}
  (g : Pattern)
  (xs : list Pattern)
  :
  well_formed_positive (foldr binary g xs)
  = (well_formed_positive g && lwf_positive xs).

Lemma well_formed_cex_foldr_binary
  (binary : Pattern → Pattern → Pattern)
  {_bin : Binary binary}
  (n : nat)
  (g : Pattern)
  (xs : list Pattern)
  :
  well_formed_closed_ex_aux (foldr binary g xs) n
  = (well_formed_closed_ex_aux g n && lwf_cex n xs).

Lemma well_formed_cmu_foldr_binary
  (binary : Pattern → Pattern → Pattern)
  {_bin : Binary binary}
  (n : nat)
  (g : Pattern)
  (xs : list Pattern)
  :
  well_formed_closed_mu_aux (foldr binary g xs) n
  = (well_formed_closed_mu_aux g n && lwf_cmu n xs).

Lemma well_formed_xy_foldr_binary
  (binary : Pattern → Pattern → Pattern)
  {_bin : Binary binary}
  (m n : nat)
  (g : Pattern)
  (xs : list Pattern)
  :
  well_formed_xy m n (foldr binary g xs)
  = (well_formed_xy m n g && lwf_xy m n xs)
.

Lemma well_formed_xy_foldr_binary_compose
  (binary : Pattern → Pattern → Pattern)
  {_bin : Binary binary}
  (m n : nat)
  (g : Pattern)
  (xs : list Pattern)
  :
  (well_formed_xy m n g = true ∧ lwf_xy m n xs = true) →
  well_formed_xy m n (foldr binary g xs) = true
.

Lemma well_formed_xy_foldr_binary_decompose
  (binary : Pattern → Pattern → Pattern)
  {_bin : Binary binary}
  (m n : nat)
  (g : Pattern)
  (xs : list Pattern)
  :
  well_formed_xy m n (foldr binary g xs) = true →
  (well_formed_xy m n g = true ∧ lwf_xy m n xs = true)
.

Class EBinder (binder : Pattern → Pattern) := {
    ebinder_morphism :
      ∀ {A : Type} (f : A → Pattern → Pattern) (f_morph : PatternMorphism f) (phi : Pattern) a,
        f a (binder phi) = binder (f (increase_ex pm_spec_data a) phi) ;
    ebinder_wfp :
      ∀ φ, well_formed_positive (binder φ) = well_formed_positive φ;
    ebinder_wfcex :
      ∀ φ n, well_formed_closed_ex_aux (binder φ) n =
        well_formed_closed_ex_aux φ (S n);
    ebinder_wfcmu :
      ∀ φ n, well_formed_closed_mu_aux (binder φ) n =
        well_formed_closed_mu_aux φ n;
}.

Lemma ebinder_wfxy
  (ebinder : Pattern → Pattern)
  {_b : EBinder ebinder}
:
∀ (x y : nat) (ψ : Pattern),
  well_formed_xy x y (ebinder ψ)
  = well_formed_xy (S x) y ψ.

Lemma ebinder_wfxy_compose
  (ebinder : Pattern → Pattern)
  {_b : EBinder ebinder}
:
∀ (x y : nat) (ψ : Pattern),
  well_formed_xy (S x) y ψ →
  well_formed_xy x y (ebinder ψ) = true
.

Lemma ebinder_wfxy_decompose
  (ebinder : Pattern → Pattern)
  {_b : EBinder ebinder}
:
∀ (x y : nat) (ψ : Pattern),
  well_formed_xy x y (ebinder ψ) = true →
  well_formed_xy (S x) y ψ = true.

Class SBinder (binder : Pattern → Pattern) := {
    sbinder_morphism :
      ∀ {A : Type} (f : A → Pattern → Pattern) (f_morph : PatternMorphism f) (phi : Pattern) a,
        f a (binder phi) = binder (f (increase_mu pm_spec_data a) phi) ;
    sbinder_wfp :
      ∀ φ, well_formed_positive (binder φ) =
                well_formed_positive φ &&
                no_negative_occurrence_db_b 0 φ;
    sbinder_wfcex :
      ∀ φ n, well_formed_closed_ex_aux (binder φ) n =
        well_formed_closed_ex_aux φ n;
    sbinder_wfcmu :
      ∀ φ n, well_formed_closed_mu_aux (binder φ) n =
        well_formed_closed_mu_aux φ (S n);
}.

Lemma sbinder_wfxy
  (sbinder : Pattern → Pattern)
  {_b : SBinder sbinder}
:
∀ (x y : nat) (ψ : Pattern),
  well_formed_xy x y (sbinder ψ)
  = well_formed_xy x (S y) ψ && no_negative_occurrence_db_b 0 ψ.

Lemma sbinder_wfxy_compose
  (sbinder : Pattern → Pattern)
  {_b : SBinder sbinder}
:
∀ (x y : nat) (ψ : Pattern),
  well_formed_xy x (S y) ψ ∧
  no_negative_occurrence_db_b 0 ψ →
  well_formed_xy x y (sbinder ψ) = true
.

Lemma sbinder_wfxy_decompose
  (sbinder : Pattern → Pattern)
  {_b : SBinder sbinder}
:
∀ (x y : nat) (ψ : Pattern),
  well_formed_xy x y (sbinder ψ) = true →
  no_negative_occurrence_db_b 0 ψ ∧ well_formed_xy x (S y) ψ = true.

#[global]
Program Instance EBinder_exists : EBinder patt_exists := {}.

#[global]
Program Instance SBinder_mu : SBinder patt_mu := {}.

#[global]
Program Instance Binary_imp : Binary patt_imp := {}.

#[global]
Program Instance Binary_app : Binary patt_app := {}.

#[global]
Program Instance Nullary_bott : Nullary patt_bott := {}.

#[global]
Program Instance Nullary_sym s : Nullary (patt_sym s) := {}.

#[global]
Program Instance Unary_not : Unary patt_not := {}.

#[global]
Program Instance NVNullary_top : Nullary patt_top := {}.

#[global]
Program Instance Binary_or : Binary patt_or := {}.

#[global]
Program Instance Binary_and : Binary patt_and := {}.

#[global]
Program Instance Binary_iff : Binary patt_iff := {}.

#[global]
Program Instance EBinder_forall : EBinder patt_forall := {}.

Class SwappableEx {A : Type} (f : A → Pattern → Pattern) (g : Pattern → Pattern)
  (m : PatternMorphism f) :=
{
  eswap : ∀ phi a,
    apply_subst pm_spec_data (increase_ex pm_spec_data a) (g phi) =
    g (apply_subst pm_spec_data a phi) ;
}.

#[global]
Program Instance Bevar_subst_swaps_ex_nesting (ψ : Pattern) (p : well_formed_closed ψ) :
  SwappableEx _ nest_ex (Bevar_subst_morphism ψ).

#[global]
Program Instance Bsvar_subst_swaps_ex_nesting (ψ : Pattern) (p : well_formed_closed ψ) :
  SwappableEx _ nest_ex (Bsvar_subst_morphism ψ).

#[global]
Program Instance Fevar_subst_swaps_ex_nesting (ψ : Pattern) (p : well_formed_closed ψ) :
  SwappableEx _ nest_ex (Free_evar_subst_morphism ψ).

#[global]
Program Instance Fsvar_subst_swaps_ex_nesting (ψ : Pattern) (p : well_formed_closed ψ) :
  SwappableEx _ nest_ex (Free_svar_subst_morphism ψ).

#[global]
Program Instance Evar_quantify_swaps_ex_nesting (x : evar) :
  SwappableEx _ nest_ex (Evar_quantify_morphism x).

#[global]
Program Instance Svar_quantify_swaps_ex_nesting (X : svar) :
  SwappableEx _ nest_ex (Svar_quantify_morphism X).

#[global]
Program Instance Evar_open_swaps_ex_nesting (x : evar) :
  SwappableEx _ nest_ex (Evar_open_morphism x).

#[global]
Program Instance Svar_open_swaps_ex_nesting (X : svar) :
  SwappableEx _ nest_ex (Svar_open_morphism X).

Definition mlSimpl' :=
(
  @binary_morphism,
  @unary_morphism,
  @nullary_morphism,
  @ebinder_morphism,
  @sbinder_morphism
).

End with_signature.

#[export]
Hint Resolve Bevar_subst_swaps_ex_nesting : core.
#[export]
Hint Resolve Bsvar_subst_swaps_ex_nesting : core.
#[export]
Hint Resolve Fevar_subst_swaps_ex_nesting : core.
#[export]
Hint Resolve Fsvar_subst_swaps_ex_nesting : core.
#[export]
Hint Resolve Evar_quantify_swaps_ex_nesting : core.
#[export]
Hint Resolve Svar_quantify_swaps_ex_nesting : core.
#[export]
Hint Resolve Evar_open_swaps_ex_nesting : core.
#[export]
Hint Resolve Svar_open_swaps_ex_nesting : core.