Library removetype

Lemma ka_eq_erase: Proper (ka_eq ==> ka_eq) erase.
Lemma ka_eq_tu_erase: Proper (ka_eq_t ==> ka_eq_u) erase.
Lemma eq_nom_erase:
  Proper (ty'∧ eq_nom_typed ==>
             eq eq_nom_untyped) erase.
Lemma eq_nom_p_erase:
  Proper (ty'∧ eq_nom_typed_p ==>
             eq (eq_perm∨eq_perm_elim∨eq_nom_untyped_p)) erase.
Lemma eq_nom_untyped_np_no_perm:
  Proper (eq_nom_untyped_np ==> iff) no_perm.

Lemma eq_nom_np_erase:
  Proper ( np ∧ eq_nom_typed_np ==>
              eq (np ∧ eq_nom_untyped_np)) erase.
Lemma eq_perm_elim_erase: Proper (eq_perm_elim ==> eq_perm_elim) erase.
Lemma eq_perm_erase: Proper (eq_perm ==> eq_perm) erase.
Lemma eq_perm_ω_erase: Proper (eq_perm_ω ==> Logic.eq) erase.
Lemma eq_ν_smpl_erase: Proper (eq_ν_smpl ==> eq_ν_smpl) erase.
Lemma eq_ω_smpl_erase :
   Proper (eq_ω_smpl ==> Logic.eq) erase.
Lemma eq_erase (ax1 ax2 : relation expr) :
  Proper (ty'∧ ax1 ==> eq ax2) erase →
  (∀ A, Proper (ax1 ==> iff) ( has_type A)) →
  Proper (ty'∧ (eq ax1) ==> eq ax2) erase.

Lemma ka_eq_support :
  Proper (ka_eq ==> equiv_lst) support.
Lemma ka_eq_u_support :
  Proper (ka_eq_u ==> equiv_lst) support.

Lemma eq_nom_untyped_support :
  Proper (eq_nom_untyped ==> equiv_lst) support.
Lemma eq_nom_untyped_p_support :
  Proper (eq_nom_untyped_p ==> equiv_lst) support.
Lemma eq_nom_untyped_np_support :
  Proper (eq_nom_untyped_np ==> equiv_lst) support.

Lemma eq_perm_elim_support :
  Proper (eq_perm_elim ==> equiv_lst) support.
Lemma eq_perm_support :
  Proper (eq_perm ==> equiv_lst) support.
Lemma eq_ν_smpl_support :
  Proper (eq_ν_smpl ==> equiv_lst) support.

Lemma eq_support ax :
  Proper (ax ==> equiv_lst) support →
  Proper (eq ax ==> equiv_lst) support.
Inductive eq_perm_W : relation expr :=
| eq_θ_W p a e : eq_perm_W (‹ p › (W a e)) (W (p⧓a) (‹ p › e)).
Inductive eq_W_smpl : expr → expr → Prop :=
| eq_W_id a A : NoDup a → a∩A = [] →
                eq_W_smpl (W a (id A)) (id (a++A))
| eq_W_p e f a : eq_W_smpl (W a (e + f)) (W a e + W a f)
| eq_W_t e f a : eq_W_smpl (W a (e · f)) (W a e · W a f)
| eq_W_s e a : eq_W_smpl (W a (e^* )) ((W a e)^* )
| eq_WW e a b : eq_W_smpl (W a (W b e)) (W b (W a e)).
Lemma eq_perm_ω_W :
  eq_perm_W ⇒ eq eq_perm_ω.
Lemma Ty_eq_perm_ω_W :
   (ty' ∧ eq_perm_W) ⇒ eq eq_perm_ω.
Global Instance W_eq ax a : Proper (eq ax ==> eq ax) (W a).

Lemma W_ω_exchange :
  ∀ a b e, eq_ω_smpl ⊢ ω a (W b e) ≡ W b (ω a e).

Lemma eq_smpl_ω_W :
  ∀ e f, eq_W_smpl e f → eq_ω_smpl ⊢ e ≡ f.

Lemma W_equiv_lst l m e : NoDup l → NoDup m → l ≈ m →
                          eq_ω_smpl ⊢ W l e ≡ W m e.
Lemma eq_νW2 :
  ∀ e a l, ¬ In a l → NoDup l →
                 eq_nom_typed ⊢ ν a (W l e) ≡ W l (ν a e).

Lemma W_ω_extract :
  ∀ a l e, NoDup l → In a l →
                ∃ m, NoDup m ∧ rm a l ≈ m
                          ∧ eq_ω_smpl ⊢ W l e ≡ ω a (W m e).
Lemma ka_eq_typed_vers:
  Proper (ut ∧ ka_eq ==> eq eq_ω_smpl) typed_vers.
Lemma ka_eq_tu_typed_vers:
  Proper (ut ∧ ka_eq_u ==> eq (ka_eq_t∨eq_ω_smpl)) typed_vers.
Lemma eq_nom_typed_vers:
  Proper (ut ∧ eq_nom_untyped ==>
             eq (eq_ω_smpl∨eq_nom_typed))
         typed_vers.
Lemma eq_nom_typed_p_vers:
  Proper (ut ∧ eq_nom_untyped_p ==>
             eq (eq_perm_ω∨eq_perm
                          ∨eq_perm_elim∨eq_nom_typed_p))
         typed_vers.
Lemma eq_nom_typed_np_vers:
  Proper (np ∧ (ut ∧ eq_nom_untyped_np) ==>
             eq (np ∧ (eq_nom_typed_np∨eq_nom_typed)))
         typed_vers.

Lemma eq_perm_elim_typed_vers:
  Proper (eq_perm_elim ==> eq_perm_elim) typed_vers.
Lemma eq_perm_typed_vers:
  Proper (ut ∧ eq_perm ==> eq (eq_nom_typed∨eq_perm_ω∨eq_perm))
         typed_vers.
Lemma eq_ν_smpl_typed_vers:
  Proper (ut ∧ eq_ν_smpl ==> eq (eq_nom_typed∨eq_ω_smpl∨eq_ν_smpl))
         typed_vers.
Lemma eq_typed_vers (ax1 ax2 : relation expr) :
  Proper (ut ∧ ax1 ==> eq ax2) typed_vers →
  Proper (ax1 ==> iff) untyped →
  Proper (ax1 ==> equiv_lst) support →
  eq_ω_smpl ⇒ ax2 →
  Proper (ut ∧ (eq ax1) ==> eq ax2) typed_vers.

Lemma erase_typed_vers :
  ∀ e A, str_positive e → A ⊨ e →
              eq_perm_ω∨eq_nom_typed∨eq_ω_smpl ⊢
                          W (〈A〉 -- support ⎣e⎦) ⎡⎣e⎦⎤ ≡ e.
Lemma erase_typed_vers_np :
  ∀ e A, str_positive e → no_perm e → A ⊨ e →
              eq_nom_typed∨eq_ω_smpl ⊢
                          W (〈A〉 -- support ⎣e⎦) ⎡⎣e⎦⎤ ≡ e.
Theorem incl_ut_ty :
  ∀ ax1 ax2 : relation expr,
    Proper (ty'∧ ax2 ==> eq ax1) erase →
    Proper (ut ∧ ax1 ==> eq ax2) typed_vers →
    (∀ A : list Atom, Proper (ax2 ==> iff)
                                  ( has_type A)) →
    Proper (ax1 ==> iff) untyped →
    Proper (ax1 ==> equiv_lst) support →
    eq_ω_smpl ⇒ ax2 →
    ∀ e f, untyped e→untyped f→
                (ax1 ⊢ e ≡ f ↔ ax2 ⊢ ⎡e⎤ ≡ ⎡f⎤).
Lemma str_positive_eq0 e : str_positive e → eq0 e = false.
Lemma eq0_erase e : eq0 ⎣e⎦ = eq0 e.
Theorem incl_ty_ut :
  ∀ ax1 ax2 : relation expr,
    Proper (ax2 ==> Logic.eq) eq0 →
    Proper (ty'∧ ax1 ==> eq ax2) erase →
    Proper (ut ∧ ax2 ==> eq ax1) typed_vers →
    (∀ A : list Atom, Proper (ax1 ==> iff)
                                  ( has_type A)) →
    Proper (ax2 ==> iff) untyped →
    Proper (ax2 ==> equiv_lst) support →
     eq_perm_ω∨eq_nom_typed∨eq_ω_smpl ⇒ ax1 →
    ∀ e f, (∃ A, A⊨e ∧ A⊨f) → positive e → positive f →
                (ax1 ⊢ e ≡ f ↔ ax2 ⊢ ⎣e⎦ ≡ ⎣f⎦).

Theorem incl_ty_ut_np :
  ∀ ax1 ax2 : relation expr,
    Proper (ax2 ==> Logic.eq) eq0 →
    Proper (ty'∧ ax1 ==> eq ax2) erase →
    Proper (ut ∧ ax2 ==> eq ax1) typed_vers →
    (∀ A : list Atom, Proper (ax1 ==> iff)
                                  ( has_type A)) →
    Proper (ax2 ==> iff) untyped →
    Proper (ax2 ==> equiv_lst) support →
    eq_nom_typed∨eq_ω_smpl ⇒ ax1 →
     ∀ e f, (∃ A, A⊨e ∧ A⊨f) → positive e → positive f →
                 no_perm e → no_perm f →
                (ax1 ⊢ e ≡ f ↔ ax2 ⊢ ⎣e⎦ ≡ ⎣f⎦).