Fixpoint can_var (n : nat) : list Atom :=
  match n with
  | O ⇒ []
  | S n ⇒ get_new (can_var n)::(can_var n)
  end.
Lemma can_var_NoDup: ∀ n, NoDup (can_var n).
Lemma can_var_length : ∀ n, length (can_var n) = n.

Definition conv_lst_perm : list Atom → perm :=
  fun l ⇒ transfer_perm (can_var (length l)) l.
Lemma conv_lst : ∀ l, NoDup l →
                           conv_lst_perm l ⧓ (can_var (length l)) = l.
Lemma conv_can_var : ∀ n, conv_lst_perm (can_var n) ≌ nil.

Lemma conv_lst_inv l :
  NoDup l → (conv_lst_perm l)⋆ ⧓ l = (can_var (length l)).

Inductive eq_perm_fresh : relation expr :=
| eq_θ_fresh p q e : (∀ a, p⋈a ≠ q⋈a → a # e) →
                     eq_perm_fresh (‹ p ›e) (‹ q ›e)
| eq_θ_fr_nil e : eq_perm_fresh (‹[]›e) e
| eq_θ_fr_id : ∀ (A B : list Atom) (p : perm),
    B ≈ p ⧓ A → eq_perm_fresh (‹ p › id A) (id B).

Fixpoint convert e :=
  match e with
  
  
  
  
  | vat a ⇒ ‹conv_lst_perm [a]› ((conv_lst_perm [a])⋆ • vat a)
  | var x ⇒ ‹conv_lst_perm (τ x)› ((conv_lst_perm (τ x))⋆ • var x)
  | ν a e ⇒ ν a (convert e)
  | ω a e ⇒ ω a (convert e)
  | e + f ⇒ convert e + convert f
  | e · f ⇒ convert e · convert f
  | e^* ⇒ convert e^*
  | ‹ p › e ⇒ ‹ p › convert e
  | _ ⇒ e
  end.
Lemma convert_involutive e :
  eq_perm_fresh ⊢ convert (convert e) ≡ (convert e).



Lemma convert_eq_perm e :
  eq_perm_elim ∨ eq_perm ⊢ e ≡ convert e.

Lemma convert_untyped e : untyped e ↔ untyped (convert e).
Lemma convert_str_positive e :
  str_positive e ↔ str_positive (convert e).
Lemma convert_single e : single e ↔ single (convert e).
Lemma convert_multi e : multi e ↔ multi (convert e).

Definition NKA_nice :=
  (ka_eq_u∨eq_perm∨eq_perm_fresh
   ∨eq_ν_smpl∨eq_nom_untyped_p∨eq_nom_untyped).

Lemma convert_fresh a e : a # e ↔ a # convert e.

Lemma untyped_NKA_nice e f :
  NKA_nice ⊢ e ≡ f → untyped e ↔ untyped f.
Lemma str_positive_NKA_nice e f :
  NKA_nice ⊢ e ≡ f → str_positive e ↔ str_positive f.

Lemma NKA_nice_stronger_NKA_θp e f : str_positive e → untyped e →
                       str_positive f → untyped f →
                       NKA_nice ⊢ e ≡ f → NKA_θp ⊢ e ≡ f.
Lemma equiv_lst_length_undup l m: l≈m → length 〈l〉 = length 〈m〉.
Lemma mact_eq_act_eq p1 p2 l:
  p1 ⧓ l = p2 ⧓ l → ∀ x,In x l → p1 ⋈ x = p2 ⋈ x.
Lemma eq_perm_elim_convert e f:
  eq_perm_elim e f → NKA_nice ⊢ convert e ≡ convert f.


Lemma convert_eq e f : str_positive e → untyped e →
                       str_positive f → untyped f →
                       NKA_θp ⊢ e ≡ f ↔ NKA_nice ⊢ convert e ≡ convert f.

Fixpoint nice e : Prop :=
  match e with
  | 0 | 1 | ⊥ _ | id _ ⇒ True
  | var l ⇒ τ l = can_var (length (τ l))
  | vat a ⇒ [a] = can_var 1
  | e + f | e · f ⇒ nice e ∧ nice f
  | e^* | ν _ e | ω _ e | ‹ _ › e ⇒ nice e
  end.
Lemma nice_convert e : nice (convert e).

Lemma nice_NKA_nice e f : NKA_nice e f → nice e ↔ nice f.
Lemma nice_eq ax : Proper (ax ==> iff) nice →
                   Proper (eq ax ==> iff) nice.
Lemma nice_convert_eq e : nice e → eq_perm_fresh ⊢ convert e ≡ e.
Lemma convert_eq2 e f : str_positive e → untyped e → nice e →
                        str_positive f → untyped f → nice f →
                       NKA_nice ⊢ convert e ≡ convert f ↔ NKA_nice ⊢ e ≡ f.

Definition Nice := (nice ⊗ single ⊗ str_positive ⊗ untyped,NKA_nice).

Lemma convert_morph : convert ⊩ ((fst NKAspu)^2,snd NKAspu) →((fst Nice)^2,snd Nice).
Lemma id_morph : (fun x ⇒ x) ⊩ ((fst Nice)^2,snd Nice) → ((fst NKAspu)^2,snd NKAspu) .

Lemma NKAspu_Nice : NKAspu ⊲ Nice.
Lemma Nice_NKAspu : Nice ⊲ NKAspu.