Library perm

Lemma apply_perm_equiv_perm p q e :
  p≌q → FFalse ⊢ p•e ≡ q•e.
Lemma eq_rm_perm : Proper (eq FFalse ==> eq FFalse) rm_perm.
Lemma eq_rm_perm_bis :
  ∀ e p, (eq_perm ∨ eq_perm_elim)
              ∨ zero_perm_u ⊢rm_perm (p•e) ≡ p•e.

Lemma zero_perm_u_apply_perm :
  ∀ p, Proper (zero_perm_u ==> (eq FFalse))
                   (rm_perm ∘ (apply_perm p)).
Lemma zero_perm_t_apply_perm :
  ∀ p, Proper (zero_perm_t ==> (eq FFalse))
                   (rm_perm ∘ (apply_perm p)).

Lemma eq_perm_apply_perm :
  ∀ p, Proper (eq_perm ==> (eq FFalse))
                   (rm_perm ∘ (apply_perm p)).
Lemma eq_perm_ω_apply_perm :
  ∀ p, Proper (eq_perm_ω ==> (eq FFalse))
                   (rm_perm ∘ (apply_perm p)).
Lemma eq_perm_elim_apply_perm :
  ∀ p, Proper (eq_perm_elim ==> (eq FFalse))
                   (rm_perm ∘ (apply_perm p)).

Lemma eq_nom_untyped_p_apply_perm :
  ∀ p, Proper (eq_nom_untyped_p ==> (eq eq_nom_untyped_np))
                   (rm_perm ∘ (apply_perm p)).
Lemma eq_nom_typed_p_apply_perm :
  ∀ p, Proper (eq_nom_typed_p ==> (eq eq_nom_typed_np))
                   (rm_perm ∘ (apply_perm p)).

Lemma apply_perm_θ_t e p :
  (∃ A, A ⊨ e) →
  eq_perm∨eq_perm_elim∨eq_perm_ω∨zero_perm_t ⊢ ‹ p › e ≡ p • e.
Lemma apply_perm_θ_u e p :
  untyped e →
  eq_perm∨eq_perm_elim∨zero_perm_u ⊢ ‹ p › e ≡ p • e.

Lemma eq_nom_untyped_np_apply_perm :
  ∀ e f , (ut ∧ eq_nom_untyped_np) e f →
                 (eq_perm∨eq_perm_elim∨zero_perm_u∨
                  eq_nom_untyped_p) ⊢ e ≡ f.

Lemma eq_nom_typed_np_apply_perm :
  ∀ e f , (eq_nom_typed_np) e f →
               (eq_perm∨eq_perm_elim∨ eq_perm_ω∨zero_perm_t∨
                         (eq_nom_typed_p)) ⊢ e ≡ f.

Lemma eq_apply_perm a b :
  (∀ p, Proper (a ==> eq b) (rm_perm ∘ (apply_perm p))) →
  Proper (equiv_perm ==> eq a ==> eq b)
         (fun p e ⇒ rm_perm (p • e)).

Lemma eq_rm_perm_ut_pos :
  ∀ (e : expr) (p : perm),
    untyped e → positive (‹ p › e) →
    eq_perm ∨ eq_perm_elim⊢ ‹ p › e ≡ rm_perm (p • e).

Lemma eq_rm_perm_pos :
  ∀ (e : expr) (p : perm),
     positive (‹ p › e) →
    eq_perm_ω∨eq_perm ∨ eq_perm_elim⊢ ‹ p › e ≡ rm_perm (p • e).

Lemma eq_apply_perm_ut_pos :
  ∀ (e : expr) (p : perm),
    untyped e → positive (‹ p › e) →
    eq_perm ∨ eq_perm_elim⊢ ‹ p › e ≡ (p • e).

Lemma eq_apply_perm_pos :
  ∀ (e : expr) (p : perm),
    positive (‹ p › e) →
    eq_perm_ω∨eq_perm ∨ eq_perm_elim⊢ ‹ p › e ≡ (p • e).

Lemma eq_nom_untyped_np_rm_perm_pos :
  ∀ e f : expr, str_positive e → str_positive f →
                    (ut ∧ eq_nom_untyped_np) e f →
                    eq_perm ∨ eq_perm_elim
                            ∨ eq_nom_untyped_p ⊢ e ≡ f.