# Strange stuff

Fixpoint can_var (n : nat) : list Atom :=
match n with
| O[]
| S nget_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 ltransfer_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, pa qa 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 aconv_lst_perm [a] ((conv_lst_perm [a])⋆ vat a)
| var xconv_lst_perm (τ x) ((conv_lst_perm (τ x))⋆ var x)
| ν a eν a (convert e)
| ω a eω a (convert e)
| e + fconvert e + convert f
| e · fconvert 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_ueq_permeq_perm_fresh
eq_ν_smpleq_nom_untyped_peq_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: lm 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 · fnice e nice f
| e^* | ν _ e | ω _ e | _ enice 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 xx) ((fst Nice)^2,snd Nice) ((fst NKAspu)^2,snd NKAspu) .

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