[helm.git] / weblib / cr / lambda.ma

include "basics/list.ma".
include "basics/types.ma".

(* LIST THEORY *)
(*theorem nil_cons:
  ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
#A;#l;#a; @; #H; ndestruct;
nqed.

ntheorem append_nil: ∀A:Type.∀l:list A.l @ □ = l.
#A;#l;nelim l;//;
#a;#l1;#IH;nnormalize;//;
nqed.

ntheorem associative_append: ∀A:Type[0].associative (list A) (append A).
#A;#x;#y;#z;nelim x
##[//
##|#a;#x1;#H;nnormalize;//]
nqed.

ntheorem cons_append_commute:
  ∀A:Type[0].∀l1,l2:list A.∀a:A.
    a :: (l1 @ l2) = (a :: l1) @ l2.
//;
nqed.

nlemma append_cons: ∀A.∀a:A.∀l,l1. l@(a::l1)=(l@[a])@l1.
#A;#a;#l;#l1;nrewrite > (associative_append ????);//;
nqed.


nlet rec nth A l d n on n ≝
  match n with
  [ O ⇒ match l with
        [ nil ⇒ d
        | cons (x : A) _ ⇒ x ]
  | S n' ⇒ nth A (tail ? l) d n'].

nlet rec map A B f l on l ≝
  match l with [ nil ⇒ nil B | cons (x:A) tl ⇒ f x :: map A B f tl ]. 

nlet rec foldr (A,B:Type[0]) (f : A → B → B) (b:B) l on l ≝ 
  match l with [ nil ⇒ b | cons (a:A) tl ⇒ f a (foldr A B f b tl) ].
   
ndefinition length ≝ λT:Type[0].λl:list T.foldr T nat (λx,c.S c) O l.

ndefinition filter ≝ 
  λT:Type[0].λl:list T.λp:T → bool.
  foldr T (list T) 
    (λx,l0.match (p x) with [ true => x::l0 | false => l0]) [] l.

ndefinition iota : nat → nat → list nat ≝
  λn,m. nat_rect_Type0 (λ_.list ?) (nil ?) (λx,acc.cons ? (n+x) acc) m.
*)  
(* ### induction principle for functions visiting 2 lists in parallel *)
lemma list_ind2 : 
  ∀T1,T2:Type[0].∀l1:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T1.∀l2:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T2.∀P:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T1 → \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T2 → Prop.
  \ 5a href="cic:/matita/basics/list/length.fix(0,1,1)"\ 6length\ 5/a\ 6 ? l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/length.fix(0,1,1)"\ 6length\ 5/a\ 6 ? l2 →
  (P (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 ?) (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 ?)) → 
  (∀hd1,hd2,tl1,tl2. P tl1 tl2 → P (hd1\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:tl1) (hd2\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:tl2)) → 
  P l1 l2.
#T1 #T2 #l1 #l2 #P #Hl #Pnil #Pcons
generalize in match Hl; generalize in match l2;
elim l1
[#l2 cases l2 //
 normalize #t2 #tl2 #H destruct
|#t1 #tl1 #IH #l2 cases l2
 [normalize #H destruct
 |#t2 #tl2 #H @Pcons @IH normalize in H;destruct //]
]
qed.

lemma eq_map : ∀A,B,f,g,l. (∀x.f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g x) → \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B g l.
#A #B #f #g #l #Efg
elim l normalize //
qed.

lemma le_length_filter : ∀A,l,p.\ 5a href="cic:/matita/basics/list/length.fix(0,1,1)"\ 6length\ 5/a\ 6 A (\ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p l) \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/length.fix(0,1,1)"\ 6length\ 5/a\ 6 A l.
#A #l #p elim l normalize
[//
|#a #tl #IH cases (p a) normalize
 [@\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"\ 6le_S_S\ 5/a\ 6 //
 |%2 //
 ]
]
qed.

lemma length_append : ∀A,l,m.\ 5a href="cic:/matita/basics/list/length.fix(0,1,1)"\ 6length\ 5/a\ 6 A (l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6m) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/length.fix(0,1,1)"\ 6length\ 5/a\ 6 A l \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/length.fix(0,1,1)"\ 6length\ 5/a\ 6 A m.
#A #l #m elim l
[//
|#H #tl #IH normalize <IH //]
qed.

inductive in_list (A:Type[0]): A → (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) → Prop ≝
| in_list_head : ∀ x,l.(in_list A x (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l))
| in_list_cons : ∀ x,y,l.(in_list A x l) → (in_list A x (y\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l)).

definition incl : ∀A.(\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) → (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) → Prop ≝
  λA,l,m.∀x.\ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x l → \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x m.
  
notation "hvbox(a break ∉ b)" non associative with precedence 45
for @{ 'notmem $a $b }. 
  
interpretation "list member" 'mem x l = (in_list ? x l).
interpretation "list not member" 'notmem x l = (Not (in_list ? x l)).
interpretation "list inclusion" 'subseteq l1 l2 = (incl ? l1 l2).
  
axiom not_in_list_nil : ∀A,x.\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6].
(*intros.unfold.intro.inversion H
  [intros;lapply (sym_eq ? ? ? H2);destruct Hletin
  |intros;destruct H4]
qed.*)

axiom in_list_cons_case : ∀A,x,a,l.\ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) →
                          x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x l.
(*intros;inversion H;intros
  [destruct H2;left;reflexivity
  |destruct H4;right;assumption]
qed.*)

axiom in_list_tail : ∀l,x,y.
      \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 x (y\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) → x \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 y → \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 x l.
(*intros 4;elim (in_list_cons_case ? ? ? ? H)
  [elim (H2 H1)
  |assumption]
qed.*)

axiom in_list_singleton_to_eq : ∀A,x,y.\ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x (y\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]) → x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y.
(*intros;elim (in_list_cons_case ? ? ? ? H)
  [assumption
  |elim (not_in_list_nil ? ? H1)]
qed.*)

axiom in_list_to_in_list_append_l: 
  ∀A.∀x:A.∀l1,l2.\ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 ? x l1 → \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 ? x (l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2).
(*intros.
elim H;simplify
  [apply in_list_head
  |apply in_list_cons;assumption
  ]
qed.*)

axiom in_list_to_in_list_append_r: 
  ∀A.∀x:A.∀l1,l2. \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 ? x l2 → \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 ? x (l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2).
(*intros 3.
elim l1;simplify
  [assumption
  |apply in_list_cons;apply H;assumption
  ]
qed.*)

lemma in_list_append_elim: 
  ∀A,x,l1,l2.\ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x (l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2) → 
  ∀P:Prop.(\ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x l1 → P) → (\ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x l2 → P) → P.
#A #x #l1 elim l1
[ #l2 #H #P #H1 #H2 @H2 @H
| #a0 #al #IH #l2 #H #P #H1 #H2 normalize in H; @(\ 5a href="cic:/matita/cr/lambda/in_list_inv_ind.def(2)"\ 6in_list_inv_ind\ 5/a\ 6 ? x … H)
  [#a1 #al1 #e0 #e1 destruct /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/cr/lambda/in_list.con(0,1,1)"\ 6in_list_head\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
  |#a1 #a2 #al1 #H3 #H4 #e1 #e2 destruct @(IH l2) /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/cr/lambda/in_list.con(0,2,1)"\ 6in_list_cons\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
  ]
]
qed.


(*
let rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝
 match l with
  [ nil ⇒ false
  | (cons a l') ⇒
    match eq x a with
     [ true ⇒ true
     | false ⇒ mem A eq x l'
     ]
  ].
  
naxiom mem_true_to_in_list :
  \forall A,equ.
  (\forall x,y.equ x y = true \to x = y) \to
  \forall x,l.mem A equ x l = true \to in_list A x l.
(* intros 5.elim l
  [simplify in H1;destruct H1
  |simplify in H2;apply (bool_elim ? (equ x a))
     [intro;rewrite > (H ? ? H3);apply in_list_head
     |intro;rewrite > H3 in H2;simplify in H2;
      apply in_list_cons;apply H1;assumption]]
qed.*)

naxiom in_list_to_mem_true :
  \forall A,equ.
  (\forall x.equ x x = true) \to
  \forall x,l.in_list A x l \to mem A equ x l = true.
(*intros 5.elim l
  [elim (not_in_list_nil ? ? H1)
  |elim H2
    [simplify;rewrite > H;reflexivity
    |simplify;rewrite > H4;apply (bool_elim ? (equ a1 a2));intro;reflexivity]].
qed.*)

naxiom in_list_filter_to_p_true : \forall A,l,x,p.
in_list A x (filter A l p) \to p x = true.
(* intros 4;elim l
  [simplify in H;elim (not_in_list_nil ? ? H)
  |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
   simplify in H1
     [elim (in_list_cons_case ? ? ? ? H1)
        [rewrite > H3;assumption
        |apply (H H3)]
     |apply (H H1)]]
qed.*)

naxiom in_list_filter : \forall A,l,p,x.in_list A x (filter A l p) \to in_list A x l.
(*intros 4;elim l
  [simplify in H;elim (not_in_list_nil ? ? H)
  |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
   simplify in H1
     [elim (in_list_cons_case ? ? ? ? H1)
        [rewrite > H3;apply in_list_head
        |apply in_list_cons;apply H;assumption]
     |apply in_list_cons;apply H;assumption]]
qed.*)

naxiom in_list_filter_r : \forall A,l,p,x.
              in_list A x l \to p x = true \to in_list A x (filter A l p).
(* intros 4;elim l
  [elim (not_in_list_nil ? ? H)
  |elim (in_list_cons_case ? ? ? ? H1)
     [rewrite < H3;simplify;rewrite > H2;simplify;apply in_list_head
     |simplify;apply (bool_elim ? (p a));intro;simplify;
        [apply in_list_cons;apply H;assumption
        |apply H;assumption]]]
qed.*)

naxiom incl_A_A: ∀T,A.incl T A A.
(*intros.unfold incl.intros.assumption.
qed.*)

naxiom incl_append_l : ∀T,A,B.incl T A (A @ B).
(*unfold incl; intros;autobatch.
qed.*)

naxiom incl_append_r : ∀T,A,B.incl T B (A @ B).
(*unfold incl; intros;autobatch.
qed.*)

naxiom incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B).
(*unfold incl; intros;elim (in_list_cons_case ? ? ? ? H1);autobatch.
qed.*)

*)


record Nset : Type[1] ≝
{
  (* carrier is specified as a coercion: when an object X of type Nset is
     given, but something of type Type is expected, Matita will insert a
     hidden coercion: the user sees "X", but really means "carrier X"     *)
  carrier :> Type[0];
  N_eqb   : carrier → carrier → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6;
  p_eqb1  : ∀x,y.N_eqb x y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y;
  p_eqb2  : ∀x,y.N_eqb x y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → x \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 y; 
  N_fresh : \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 carrier → carrier;
  p_fresh : ∀l.N_fresh l \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 l
}.

lemma bool_elim : 
∀P:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → Prop.∀b.(b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → P \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) → (b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → P \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) → P b.
#P * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
qed.

lemma p_eqb3 : ∀X,x,y.x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y → \ 5a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"\ 6N_eqb\ 5/a\ 6 X x y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
#X #x #y @(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (\ 5a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"\ 6N_eqb\ 5/a\ 6 X x y)) //
#H1 cases (\ 5a href="cic:/matita/cr/lambda/p_eqb2.fix(0,0,3)"\ 6p_eqb2\ 5/a\ 6 ??? H1) #H2 #H3 cases (H2 H3)
qed.

lemma p_eqb4 : ∀X,x,y.x \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 y → \ 5a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"\ 6N_eqb\ 5/a\ 6 X x y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6.
#X #x #y #H1 @(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (\ 5a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"\ 6N_eqb\ 5/a\ 6 X x y)) //
#H2 cases H1 #H3 cases (H3 (\ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"\ 6p_eqb1\ 5/a\ 6 ??? H2))
qed.

axiom X : \ 5a href="cic:/matita/cr/lambda/Nset.ind(1,0,0)"\ 6Nset\ 5/a\ 6.

inductive pre_tm : Type[0] ≝
| Par : \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6 → pre_tm
| Var : \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → pre_tm
| App : pre_tm → pre_tm → pre_tm
| Abs : pre_tm → pre_tm.

inductive tm_level : \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6 → Prop ≝ 
| tml_Par : ∀n,x.tm_level n (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 x)
| tml_Var : ∀n,m.n \ 5a title="natural 'greater than'" href="cic:/fakeuri.def(1)"\ 6>\ 5/a\ 6 m → tm_level n (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"\ 6Var\ 5/a\ 6 m)
| tml_App : ∀n,M1,M2.tm_level n M1 → tm_level n M2 → tm_level n (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"\ 6App\ 5/a\ 6 M1 M2)
| tml_Abs : ∀n,M0.tm_level (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n) M0 → tm_level n (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 M0).

record ext_tm (l:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) : Type[0] ≝ {
  tm_of_etm :> \ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6;
  etm_level : \ 5a href="cic:/matita/cr/lambda/tm_level.ind(1,0,0)"\ 6tm_level\ 5/a\ 6 l tm_of_etm
}.

(* 
 * we don't want to specify "N_eqb X" or "N_eqb Y" for the equality on X or Y,
 * so we use a notation "a ? b" to hide the naming structure
 * to type ?, write \equest.
 *)
notation > "hvbox(a break ≟ b)" 
  non associative with precedence 40
for @{ 'equiv ? $a $b }.
notation < "hvbox(a break maction (≟) (≟\sub t) b)" 
  non associative with precedence 40
for @{ 'equiv $t $a $b }.
interpretation "name decidable equality" 'equiv t a b = (N_eqb t a b).

(* valida solo se u è chiuso *)
let rec subst t x u on t : \ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6 ≝ 
  match t with 
  [ Par x2 ⇒ match x \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 x2 with
    [ true ⇒ u
    | false ⇒ t ]
  | Var _ ⇒ t
  | App t1 t2 ⇒ \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"\ 6App\ 5/a\ 6 (subst t1 x u) (subst t2 x u)
  | Abs t1 ⇒ \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 (subst t1 x u) ].

let rec nth A (xl:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) n on xl ≝ 
  match xl with
  [ nil ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 A
  | cons x0 xl0 ⇒ match n with
    [ O ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 A x0
    | S m ⇒ nth A xl0 m ] ].
    
(* it's necessary to specify Nset... unification hint? *)    
let rec posn (A:\ 5a href="cic:/matita/cr/lambda/Nset.ind(1,0,0)"\ 6Nset\ 5/a\ 6) (xl:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) x on xl ≝ 
  match xl with
  [ nil ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6
  | cons x0 xl0 ⇒ match x \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 x0 with
    [ true ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6
    | false ⇒ match posn A xl0 x with
      [ None ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6
      | Some n ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n) ] ] ].

let rec vopen t xl k on t ≝ 
  match t with
  [ Par _ ⇒ t
  | Var n ⇒ match \ 5a href="cic:/matita/cr/lambda/nth.fix(0,1,1)"\ 6nth\ 5/a\ 6 ? xl (n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6k) with
    [ None ⇒ t
    | Some x ⇒ \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 x ]
  | App t1 t2 ⇒ \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"\ 6App\ 5/a\ 6 (vopen t1 xl k) (vopen t2 xl k)
  | Abs t1 ⇒ \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 (vopen t1 xl (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 k)) ].

let rec vclose t xl k on t ≝ 
  match t with
  [ Par x0 ⇒ match \ 5a href="cic:/matita/cr/lambda/posn.fix(0,1,3)"\ 6posn\ 5/a\ 6 ? xl x0 with
    [ None ⇒ t
    | Some n ⇒ \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"\ 6Var\ 5/a\ 6 (n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6k) ]
  | Var n ⇒ t
  | App t1 t2 ⇒ \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"\ 6App\ 5/a\ 6 (vclose t1 xl k) (vclose t2 xl k)
  | Abs t1 ⇒ \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 (vclose t1 xl (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 k)) ].

let rec GV t ≝
  match t with
  [ Par x ⇒ x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] 
  | Var _ ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]
  | App u v ⇒ GV u \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 GV v
  | Abs u ⇒ GV u ].

(* as above, fp_perm is a coercion
 * but being a coercion to FunClass, a different syntax is required
 * I'll fix this later *)
record fp (X:\ 5a href="cic:/matita/cr/lambda/Nset.ind(1,0,0)"\ 6Nset\ 5/a\ 6) : Type[0] ≝
{ 
  fp_perm       :1> X → X;
  fp_injective  :  \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 ?? fp_perm;
  fp_surjective :  \ 5a href="cic:/matita/basics/relations/surjective.def(1)"\ 6surjective\ 5/a\ 6 ?? fp_perm;
  fp_finite     :  \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6l.∀x.x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 l → fp_perm x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 x
}.

definition Pi ≝ \ 5a href="cic:/matita/cr/lambda/fp.ind(1,0,1)"\ 6fp\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.

record fp_pre_tm : Type[0] ≝
{
  fppt_perm       :1> \ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6 → \ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6;
  fppt_injective  :  \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 ?? fppt_perm;
  fppt_surjective :  \ 5a href="cic:/matita/basics/relations/surjective.def(1)"\ 6surjective\ 5/a\ 6 ?? fppt_perm
}.

(*coercion fp_perm : ∀N:Nset.∀F:fp N.N → N ≝ fp_perm on _F:(fp N) to ? → ?.
coercion fppt_perm : ∀F:fp_pre_tm.pre_tm → pre_tm ≝ fppt_perm on _F:fp_pre_tm to ? → ?.*)

(* notation "p·x" right associative with precedence 60 for @{'middot $p $x}.
interpretation "apply fp" 'middot p x = (fp_perm ? p x).
interpretation "apply fppt" 'middot p x = (fppt_perm p x).*)

let rec mapX (p:\ 5a href="cic:/matita/cr/lambda/fp.ind(1,0,1)"\ 6fp\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6) t on t : \ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6 ≝
  match t with
  [ Par x ⇒ \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 (p x)
  | Var _ ⇒ t
  | App u v ⇒ \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"\ 6App\ 5/a\ 6 (mapX p u) (mapX p v)
  | Abs u ⇒ \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 (mapX p u) ].
  
definition swap : ∀N:\ 5a href="cic:/matita/cr/lambda/Nset.ind(1,0,0)"\ 6Nset\ 5/a\ 6.N → N → N → N ≝
  λN,u,v,x.match (x \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 u) with
    [true ⇒ v
    |false ⇒ match (x \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 v) with
       [true ⇒ u
       |false ⇒ x]].

lemma Neqb_n_n : ∀N:\ 5a href="cic:/matita/cr/lambda/Nset.ind(1,0,0)"\ 6Nset\ 5/a\ 6.∀n:N.(n \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 n) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
#N #n /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/cr/lambda/p_eqb3.def(4)"\ 6p_eqb3\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
       
lemma swap_left : ∀N,x,y.(\ 5a href="cic:/matita/cr/lambda/swap.def(3)"\ 6swap\ 5/a\ 6 N x y x) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y.
#N #x #y whd in ⊢ (??%?); >(\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"\ 6Neqb_n_n\ 5/a\ 6) //
qed.

lemma swap_right : ∀N,x,y.(\ 5a href="cic:/matita/cr/lambda/swap.def(3)"\ 6swap\ 5/a\ 6 N x y y) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 x.
#N #x #y whd in ⊢ (??%?); >(\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"\ 6Neqb_n_n\ 5/a\ 6) @(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (y \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 x)) 
normalize #H /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"\ 6p_eqb1\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.

lemma swap_other : ∀N,x,y,z.(z \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 x) → (z \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 y) → (\ 5a href="cic:/matita/cr/lambda/swap.def(3)"\ 6swap\ 5/a\ 6 N x y z) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 z.
#N #x #y #z #H1 #H2 normalize >(\ 5a href="cic:/matita/cr/lambda/p_eqb4.def(4)"\ 6p_eqb4\ 5/a\ 6 … H1) 
normalize >(\ 5a href="cic:/matita/cr/lambda/p_eqb4.def(4)"\ 6p_eqb4\ 5/a\ 6 … H2) %
qed.

lemma swap_inv : ∀N,u,v,x.(\ 5a href="cic:/matita/cr/lambda/swap.def(3)"\ 6swap\ 5/a\ 6 N u v (\ 5a href="cic:/matita/cr/lambda/swap.def(3)"\ 6swap\ 5/a\ 6 N u v x)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 x.
#N #u #v #x normalize
@(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (x \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 u)) #H1 >H1 normalize
[normalize >\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"\ 6Neqb_n_n\ 5/a\ 6 normalize
 @(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (v \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 u)) #H2 normalize
 [>(\ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"\ 6p_eqb1\ 5/a\ 6 … H2) >(\ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"\ 6p_eqb1\ 5/a\ 6 … H1) %
 |>(\ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"\ 6p_eqb1\ 5/a\ 6 … H1) %
 ]
|@(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (x \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 v)) #H2 normalize
 [>\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"\ 6Neqb_n_n\ 5/a\ 6 normalize >(\ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"\ 6p_eqb1\ 5/a\ 6 … H2) %
 |>H1 >H2 %
 ]
]
qed.

lemma swap_inj : ∀N,u,v.\ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 ?? (\ 5a href="cic:/matita/cr/lambda/swap.def(3)"\ 6swap\ 5/a\ 6 N u v).
#N #u #v #x #y normalize @(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (x \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 u)) normalize #H1
[@(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (y \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 u)) normalize #H2
 [#H3 >(\ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"\ 6p_eqb1\ 5/a\ 6 … H2) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"\ 6p_eqb1\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 |@(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (y \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 v)) normalize #H3
  [>(\ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"\ 6p_eqb1\ 5/a\ 6 ??? H3) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"\ 6p_eqb1\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
  |#H4 cases (\ 5a href="cic:/matita/cr/lambda/p_eqb2.fix(0,0,3)"\ 6p_eqb2\ 5/a\ 6 ??? H3) #H5 cases (H5 ?) //
  ]
 ]
|@(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (y \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 u)) normalize #H2
 [@(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (x \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 v)) normalize #H3 #H4
  [>H4 in H1; #H1 >H1 in H3;#H3 destruct (H3)
  |>H4 in H3; >\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"\ 6Neqb_n_n\ 5/a\ 6 #H5 destruct (H5)
  ]
 |@(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (x \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 v)) normalize #H3
  [@(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (y \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 v)) normalize #H4 #H5
   [>(\ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"\ 6p_eqb1\ 5/a\ 6 … H4) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"\ 6p_eqb1\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
   |>H5 in H2; >\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"\ 6Neqb_n_n\ 5/a\ 6 #H2 destruct (H2)
   ]
  |cases (y \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 v) normalize #H4
   [>H4 in H1; >\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"\ 6Neqb_n_n\ 5/a\ 6 #H1 destruct (H1)
   |//
   ]
  ]
 ]
]
qed.

lemma swap_surj : ∀N,u,v.\ 5a href="cic:/matita/basics/relations/surjective.def(1)"\ 6surjective\ 5/a\ 6 ?? (\ 5a href="cic:/matita/cr/lambda/swap.def(3)"\ 6swap\ 5/a\ 6 N u v).
#N #u #v #z normalize @(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (z \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 v)); #H1
  [%[@u] >\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"\ 6Neqb_n_n\ 5/a\ 6 normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"\ 6p_eqb1\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
  |@(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (z \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 u)) #H2
    [%[@v]
     >(\ 5a href="cic:/matita/cr/lambda/p_eqb4.def(4)"\ 6p_eqb4\ 5/a\ 6 ? v u)
       [>\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"\ 6Neqb_n_n\ 5/a\ 6 normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"\ 6p_eqb1\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
       |% #H3 cases (\ 5a href="cic:/matita/cr/lambda/p_eqb2.fix(0,0,3)"\ 6p_eqb2\ 5/a\ 6 ??? H1) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
       ]
    |%[@z]
     >H1 >H2 %
    ]
  ]
qed.

lemma swap_finite : ∀N,u,v.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6l.∀x.x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 l → (\ 5a href="cic:/matita/cr/lambda/swap.def(3)"\ 6swap\ 5/a\ 6 N u v) x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 x.
#N #u #v %[@ (u\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:v\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6])]
#x #H1 @\ 5a href="cic:/matita/cr/lambda/swap_other.def(5)"\ 6swap_other\ 5/a\ 6 % #H2 cases H1 #H3 @H3 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/cr/lambda/in_list.con(0,1,1)"\ 6in_list_head\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/in_list.con(0,2,1)"\ 6in_list_cons\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.

definition pi_swap : ∀N,u,v.\ 5a href="cic:/matita/cr/lambda/fp.ind(1,0,1)"\ 6fp\ 5/a\ 6 N ≝ 
λN,u,v.\ 5a href="cic:/matita/cr/lambda/fp.con(0,1,1)"\ 6mk_fp\ 5/a\ 6 ? (\ 5a href="cic:/matita/cr/lambda/swap.def(3)"\ 6swap\ 5/a\ 6 N u v) (\ 5a href="cic:/matita/cr/lambda/swap_inj.def(6)"\ 6swap_inj\ 5/a\ 6 N u v) (\ 5a href="cic:/matita/cr/lambda/swap_surj.def(6)"\ 6swap_surj\ 5/a\ 6 N u v) (\ 5a href="cic:/matita/cr/lambda/swap_finite.def(6)"\ 6swap_finite\ 5/a\ 6 N u v).

lemma eq_swap_pi : ∀N,u,v,x.\ 5a href="cic:/matita/cr/lambda/swap.def(3)"\ 6swap\ 5/a\ 6 N u v x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/pi_swap.def(7)"\ 6pi_swap\ 5/a\ 6 N u v x.
#N #u #v #x %
qed.

(* lemma subst_fp : 
  ∀s,c,x.(x ∈ GV s → x = c) → subst_X s c (Par x) = (pi_swap ? c x)·s.
intros 3;elim s 0;simplify;intros
[rewrite < eq_swap_pi;apply (bool_elim ? (c ≟ c1));simplify;intro
 [rewrite > (p_eqb1 ??? H1);autobatch
 |apply (bool_elim ? (x ≟ c1));intro
  [elim (p_eqb2 ??? H1);rewrite < H
   [autobatch
   |rewrite > (p_eqb1 ??? H2);autobatch]
  |rewrite > swap_other;autobatch]]
|reflexivity
|rewrite > H
 [rewrite > H1
  [reflexivity
  |intro;apply H2;autobatch]
 |intro;apply H2;autobatch]
|rewrite > H
 [reflexivity
 |assumption]]
qed. *)

lemma subst_x_x : ∀M,x.\ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 M x (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 x) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 M.
#M #x elim M normalize
[#x0 @(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (x \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 x0)) normalize #H1 /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"\ 6p_eqb1\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
|*:/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/]
qed.

lemma pre_tm_inv_Par : 
 ∀P:\ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6 → \ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6 → Prop.
 ∀x.(∀x0.P (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 x) (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 x0)) → ∀M.\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 M → P (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 x) M.
#P #x #H #M cases M
[//
|#n #H1 destruct (H1)
|#M1 #M2 #H1 destruct (H1)
|#M0 #H1 destruct (H1)
]
qed.
 
lemma pre_tm_inv_Var : 
 ∀P:\ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6 → \ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6 → Prop.
 ∀n.(∀n0.P (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"\ 6Var\ 5/a\ 6 n) (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"\ 6Var\ 5/a\ 6 n0)) → ∀M.\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"\ 6Var\ 5/a\ 6 n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 M → P (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"\ 6Var\ 5/a\ 6 n) M.
#P #n #H #M cases M
[2://
|#x #H1 destruct (H1)
|#M1 #M2 #H1 destruct (H1)
|#M0 #H1 destruct (H1)
]
qed.

lemma pre_tm_inv_Lam : 
 ∀P:\ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6 → \ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6 → Prop.
 ∀M.(∀N0.P (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 M) (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 N0)) → ∀N.\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 M \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 N → P (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 M) N.
#P #M #H #N cases N
[4://
|#x #H1 destruct (H1)
|#n #H1 destruct (H1)
|#M1 #M2 #H1 destruct (H1)
]
qed.

lemma pre_tm_inv_App : 
 ∀P:\ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6 → \ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6 → Prop.
 ∀M1,M2.(∀N1,N2.P (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"\ 6App\ 5/a\ 6 M1 M2) (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"\ 6App\ 5/a\ 6 N1 N2)) → 
 ∀N.\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"\ 6App\ 5/a\ 6 M1 M2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 N → P (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"\ 6App\ 5/a\ 6 M1 M2) N.
#P #M1 #M2 #H #N cases N
[3://
|#x #H1 destruct (H1)
|#n #H1 destruct (H1)
|#M0 #H1 destruct (H1)
]
qed.

interpretation "permutation of pre_tm" 'middot p M = (mapX p M).

lemma Pi_Par_elim : ∀P:Prop.∀p.∀x,y.(∀z.y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 z → P) → \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 p\ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6y → P.
#P #p #x #y cases y
[#x0 #H1 #H2 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
|#n #H1 #H2 normalize in H2; destruct (H2)
|#M1 #M2 #H1 #H2 normalize in H2; destruct (H2)
|#M0 #H1 #H2 normalize in H2; destruct (H2)
]
qed.

lemma Pi_Var_elim : ∀P:Prop.∀p,n,y.(∀n0.y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"\ 6Var\ 5/a\ 6 n0 → P) → \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"\ 6Var\ 5/a\ 6 n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 p\ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6y → P.
#P #p #n #y cases y
[#x0 #H1 #H2 normalize in H2; destruct (H2)
|#n0 #H1 #H2 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
|#M1 #M2 #H1 #H2 normalize in H2; destruct (H2)
|#M0 #H1 #H2 normalize in H2; destruct (H2)
]
qed.

lemma Pi_App_elim : 
  ∀P:Prop.∀p,M1,M2,y.(∀N1,N2.y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"\ 6App\ 5/a\ 6 N1 N2 → P) → \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"\ 6App\ 5/a\ 6 M1 M2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 p\ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6y → P.
#P #p #M1 #M2 #y cases y
[#x0 #H1 #H2 normalize in H2; destruct (H2)
|#n #H1 #H2 normalize in H2; destruct (H2)
|#M1 #M2 #H1 #H2 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
|#M0 #H1 #H2 normalize in H2; destruct (H2)
]
qed.

lemma Pi_Abs_elim : ∀P:Prop.∀p,M0,y.(∀N0.y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 N0 → P) → \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 M0 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 p\ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6y → P.
#P #p #M0 #y cases y
[#x0 #H1 #H2 normalize in H2; destruct (H2)
|#n #H1 #H2 normalize in H2; destruct (H2)
|#M1 #M2 #H1 #H2 normalize in H2; destruct (H2)
|#M0 #H1 #H2 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
]
qed.

(*lemma mapX_elim : 
  ∀P:pre_tm → Prop.∀p,x,y.(∀z.P (p·z)) → p·x = y → P y.
#P #p #x #y #H1 *)

definition fppt_of_fp : \ 5a href="cic:/matita/cr/lambda/fp.ind(1,0,1)"\ 6fp\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6 → \ 5a href="cic:/matita/cr/lambda/fp_pre_tm.ind(1,0,0)"\ 6fp_pre_tm\ 5/a\ 6.
#p @\ 5a href="cic:/matita/cr/lambda/fp_pre_tm.con(0,1,0)"\ 6mk_fp_pre_tm\ 5/a\ 6
[@(\ 5a href="cic:/matita/cr/lambda/mapX.fix(0,1,3)"\ 6mapX\ 5/a\ 6 p)
|#x elim x
 [#x0 #y #H1 @(\ 5a href="cic:/matita/cr/lambda/Pi_Par_elim.def(4)"\ 6Pi_Par_elim\ 5/a\ 6 … H1)
  #z #H2 >H2 in H1; #H1 normalize in H1; destruct (H1) /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/fp_injective.fix(0,1,3)"\ 6fp_injective\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 |#n #y #H1 @(\ 5a href="cic:/matita/cr/lambda/Pi_Var_elim.def(4)"\ 6Pi_Var_elim\ 5/a\ 6 … H1)
  #z #H2 >H2 in H1; #H1 @H1
 |#M1 #M2 #IH1 #IH2 #y #H1 @(\ 5a href="cic:/matita/cr/lambda/Pi_App_elim.def(4)"\ 6Pi_App_elim\ 5/a\ 6 … H1)
  #N1 #N2 #H2 >H2 in H1; #H1 normalize in H1; destruct (H1)
  generalize in match e1; -e1 >e0 normalize in ⊢ (??%% → ?); #e1 /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/eq_f2.def(3)"\ 6eq_f2\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 |#M0 #IH0 #y #H1 @(\ 5a href="cic:/matita/cr/lambda/Pi_Abs_elim.def(4)"\ 6Pi_Abs_elim\ 5/a\ 6 … H1)
  #N0 #H2 >H2 in H1; #H1 normalize in H1; destruct (H1) /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 ]
|#z elim z
 [#x0 cases (\ 5a href="cic:/matita/cr/lambda/fp_surjective.fix(0,1,3)"\ 6fp_surjective\ 5/a\ 6 ? p x0) #x1 #H1 %[@(\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 x1)] >H1 %
 |#n0 %[@(\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"\ 6Var\ 5/a\ 6 n0)] %
 |#M1 #M2 * #N1 #IH1 * #N2 #IH2
  %[@(\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"\ 6App\ 5/a\ 6 N1 N2)] /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/eq_f2.def(3)"\ 6eq_f2\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 |#M0 * #N0 #IH0 %[@(\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 N0)] /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
]
qed.

lemma pi_lemma1 : 
  ∀M,P,x,pi.pi \ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 M x P) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 (pi \ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 M) (pi x) (pi \ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 P).
#M #P #x #pi elim M
[#c normalize @(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (x \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 c)) normalize #H1
 [cut (pi x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 pi c);
  [/\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"\ 6p_eqb1\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
  |#H2 >\ 5a href="cic:/matita/cr/lambda/p_eqb3.def(4)"\ 6p_eqb3\ 5/a\ 6 // ]
 |cut (pi x \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 pi c)
  [% #H2 >(\ 5a href="cic:/matita/cr/lambda/fp_injective.fix(0,1,3)"\ 6fp_injective\ 5/a\ 6 … H2) in H1; >\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"\ 6Neqb_n_n\ 5/a\ 6 #H1 destruct (H1)
  |#H2 >\ 5a href="cic:/matita/cr/lambda/p_eqb4.def(4)"\ 6p_eqb4\ 5/a\ 6 // ]
 ]
|*:normalize //]
qed.

(*
lemma pi_lemma2 :
  ∀M,P,y,pi. pi · (subst_Y M y P) = subst_Y (pi · M) y (pi · P).
intros;elim M
[reflexivity
|simplify;apply (bool_elim ? (y ≟ c));simplify;intro;reflexivity
|simplify;autobatch paramodulation
|simplify;apply (bool_elim ? (y ≟ c));simplify;intro;autobatch paramodulation]
qed.
*)

definition Lam ≝ λx:\ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.λM:\ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6.\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"\ 6vclose\ 5/a\ 6 M (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]) \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6).

definition Judg ≝ λG,M.\ 5a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"\ 6vclose\ 5/a\ 6 M G \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.

definition body ≝ λx,M.match M with
 [ Abs M0 ⇒ \ 5a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"\ 6vopen\ 5/a\ 6 M (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]) \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6
 | _  ⇒ M ].

inductive dupfree (A:Type[0]) : \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A → Prop ≝
| df_nil  : dupfree A \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]
| df_cons : ∀x,xl.x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 xl → dupfree A xl → dupfree A (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:xl).

record df_list (A:Type[0]) : Type[0] ≝ {
  list_of_dfl :> \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A;
  dfl_dupfree : \ 5a href="cic:/matita/cr/lambda/dupfree.ind(1,0,1)"\ 6dupfree\ 5/a\ 6 A list_of_dfl
}.

(* ciascuno dei pre_tm utilizzati nella costruzione deve essere un ext_tm 0 *)
inductive tm : \ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6 → Prop ≝
| tm_Par : ∀xl:\ 5a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"\ 6df_list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.∀x.x \ 5a title="list member" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 xl → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 x))
| tm_App : ∀xl:\ 5a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"\ 6df_list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.∀M1,M2:\ 5a href="cic:/matita/cr/lambda/ext_tm.ind(1,0,1)"\ 6ext_tm\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl M1) → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl M2) → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"\ 6App\ 5/a\ 6 M1 M2))
| tm_Lam : ∀xl:\ 5a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"\ 6df_list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.∀x.∀M:\ 5a href="cic:/matita/cr/lambda/ext_tm.ind(1,0,1)"\ 6ext_tm\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 xl → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:xl) M) → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl (\ 5a href="cic:/matita/cr/lambda/Lam.def(5)"\ 6Lam\ 5/a\ 6 x M)).


inductive tm2 : pre_tm → Prop ≝
| tm2_Par : ∀xl:df_list X.∀x.x ∈ xl → tm2 (Judg xl (Par x))
| tm2_App : ∀xl:df_list X.∀M1,M2.tm2 (Judg xl M1) → tm2 (Judg xl M2) → tm2 (Judg xl (App M1 M2))
| tm2_Lam : ∀xl:df_list X.∀M,C.(∀x.x ∉ xl@C → tm2 (Judg (x::xl) (body x M))) → tm2 (Judg xl (Abs M)).




inductive L (F:X → S_exp → Y) : S_exp → Prop \def
| LPar : ∀x:X.L F (Par x)
| LApp : ∀M,N:S_exp. (L F M) → (L F N) → L F (App M N)
| LAbs : ∀M:S_exp. ∀x:X. (L F M) →
   L F (Abs (F x M) (subst_X M x (Var (F x M)))).
   
definition apartb : X → S_exp → bool ≝
  λx,M.notb (mem X (N_eqb X) x (GV M)).
   
let rec E (x:X) (M:S_exp) on M : list Y ≝
  match M with
    [ Par x ⇒ []
    | Var _ ⇒ []
    | App u v ⇒ E x u @ E x v
    | Abs y u ⇒ match apartb x u with
        [ true ⇒ []
        | false ⇒ y :: E x u ]].

definition apart : X → S_exp → Prop ≝ 
  λx,M.¬ x ∈ GV M.

interpretation "name apartness wrt GV" 'apart x s = (apart x s). 

lemma apartb_true_to_apart : ∀x,s.apartb x s = true → x # s.
intros;intro;
lapply (in_list_to_mem_true ? (N_eqb X) ??? H1)
[simplify;intro;generalize in match (p_eqb2 ? x1 x1);
 cases (x1 ≟ x1);intro;try autobatch;
 elim H2;reflexivity;
|unfold apartb in H;rewrite > Hletin in H;simplify in H;destruct]
qed.

lemma apart_to_apartb_true : ∀x,s.x # s → apartb x s = true.
intros;cut (¬ (mem X (N_eqb X) x (GV s)) = true)
[unfold apartb;generalize in match Hcut;
 cases (mem X (N_eqb X) x (GV s));intro;
 [elim H1;reflexivity
 |reflexivity]
|intro;apply H;autobatch]
qed.

lemma E_fresh : ∀x,M.x # M → E x M = [].
intros 2;elim M;simplify
[1,2:reflexivity
|rewrite > H
 [rewrite > H1
  [reflexivity
  |elim s1 in H2;simplify;
   [simplify in H2;intro;apply H2;autobatch
   |autobatch
   |simplify in H4;intro;apply H4;autobatch
   |simplify in H3;intro;apply H3;autobatch]]
 |elim s in H2;simplify;
   [simplify in H2;intro;apply H2;lapply (in_list_singleton_to_eq ??? H3);
    autobatch
   |autobatch
   |simplify in H4;intro;apply H4;autobatch
   |simplify in H3;intro;apply H3;autobatch]]
|rewrite > H
 [rewrite > (apart_to_apartb_true ?? H1);simplify;reflexivity
 |apply H1]]
qed.

lemma mem_false_to_not_in_list :
  ∀A,equ.(∀x,y.x = y → equ x y = true) →
  ∀x,l.mem A equ x l = false → x ∉ l.
intros 5;elim l
[autobatch
|intro;apply (bool_elim ? (equ x a));intros
 [simplify in H2;rewrite > H4 in H2;simplify in H2;destruct
 |cases (in_list_cons_case ???? H3)
  [rewrite > H in H4
   [destruct
   |assumption]
  |apply H1;
   [generalize in match H2;simplify;rewrite > H4;simplify;
    intro;assumption
   |assumption]]]]
qed.

lemma mem_append : ∀A,equ.
 (∀x,y. x = y → equ x y = true) → 
 (∀x,y. equ x y = true → x = y) →
  ∀x,l1,l2.mem A equ x (l1@l2) = orb (mem A equ x l1) (mem A equ x l2).
intros;apply (bool_elim ? (mem A equ x (l1@l2)));intro
[cut (x ∈ l1@l2)
 [cases (in_list_append_to_or_in_list ???? Hcut)
  [rewrite > in_list_to_mem_true
   [reflexivity
   |intro;apply H;reflexivity
   |assumption]
  |cases (mem A equ x l1);simplify;try reflexivity;
   rewrite > in_list_to_mem_true
   [reflexivity
   |intro;apply H;reflexivity
   |assumption]]
 |autobatch]
|lapply (mem_false_to_not_in_list ????? H2)
 [assumption
 |apply orb_elim;apply (bool_elim ? (mem A equ x l1));intro;simplify
  [lapply (mem_true_to_in_list ????? H3);try assumption;
   elim Hletin;autobatch
  |apply (bool_elim ? (mem A equ x l2));intro;simplify
   [lapply (mem_true_to_in_list ????? H4);try assumption;
    elim Hletin;autobatch
   |reflexivity]]]]
qed.
   
(* lemma apartb_App_apart1 : ∀x,M,N.apartb x (App M N) = true → apartb x M = true.
simplify;intros;unfold apartb;
apply (bool_elim ? (mem X (N_eqb X) x (GV M)));
simplify;intro
[

cut (x ∉ GV M @ GV N)
[cut (apartb x M = false → False)
 [generalize in match Hcut1;cases (apartb x M);simplify;intro;
  [reflexivity|elim H1;reflexivity]
 |intro;apply Hcut;


lemma apartb_App_apart1 : ∀x,M,N.apartb x (App M N) = true → apartb x M = true.

lemma apartb_App_apart1 : ∀x,M,N.apartb x (App M N) = true → apartb x M = true.*)

axiom daemon : False.

lemma Ep : ∀x1,x2,M,Q.x1 ≠ x2 → x1 # Q → E x1 M = E x1 (subst_X M x2 Q).
intros;elim M
[simplify;cases (x2 ≟ c);simplify;autobatch
|reflexivity
|simplify;autobatch
|whd in ⊢ (??%?);rewrite > H2;
 simplify in ⊢ (???%);
 rewrite > (? : apartb x1 s = apartb x1 (subst_X s x2 Q))
 [reflexivity
 |elim s
  [simplify;simplify in H2;apply (bool_elim ? (x1 ≟ c1));simplify;intro
   [apply (bool_elim ? (x2 ≟ c1));simplify;intro
    [lapply (p_eqb1 ??? H3);elim H;autobatch;
    |rewrite > H3;reflexivity]
   |apply (bool_elim ? (x2 ≟ c1));simplify;intro
    [autobatch
    |rewrite > H3;reflexivity]]
  |reflexivity
  |simplify;rewrite > mem_append
   [rewrite > mem_append
    [unfold apartb in H3;unfold apartb in H4;autobatch paramodulation
    |*:autobatch]
   |*:autobatch]
  |apply H3]]]
qed.

lemma pi_Abs : ∀pi,x,M.pi · Abs x M = Abs x (pi · M).
intros;reflexivity;
qed.

lemma E_Abs : ∀x,y,v,M.y ∈ E x (Abs v M) → y ∈ v::E x M.
intros 4;simplify;cases (apartb x M);simplify;intro
[elim (not_in_list_nil ?? H)
|assumption]
qed.

lemma E_all_fresh : ∀x1,x2,x3,M.
  x3 ≠ x1 → x3 ≠ x2 → E x3 M = E x3 (subst_X M x1 (Par x2)).
intros;elim M;simplify
[cases (x1 ≟ c);reflexivity
|reflexivity
|autobatch paramodulation
|rewrite > (? : apartb x3 s = apartb x3 (subst_X s x1 (Par x2)))
 [rewrite > H2;reflexivity
 |elim s
  [simplify;simplify in H2;apply (bool_elim ? (x1 ≟ c1));simplify;intro
   [lapply (p_eqb1 ??? H3);rewrite < Hletin;
    rewrite > p_eqb4 [|assumption]
    rewrite > p_eqb4 [|assumption]
     reflexivity
   |reflexivity]
  |reflexivity
  |simplify;rewrite > mem_append
   [rewrite > mem_append
    [unfold apartb in H3;unfold apartb in H4;
     autobatch paramodulation
    |*:autobatch]
   |*:autobatch]
  |apply H3]]]
qed.

lemma E_fresh_subst_Y :
  ∀x1,x2,y,S.x1 ≠ x2 → E x1 S = E x1 (subst_Y S y (Par x2)).
intros;elim S
[reflexivity
|simplify;cases (y ≟ c);simplify;reflexivity
|simplify;autobatch paramodulation
|simplify;apply (bool_elim ? (y ≟ c));intro;simplify
 [reflexivity
 |rewrite < H1;rewrite < (? : apartb x1 s = apartb x1 (subst_Y s y (Par x2)))
  [reflexivity
  |elim s;simplify
   [reflexivity
   |cases (y ≟ c1);simplify
    [rewrite > p_eqb4;autobatch
    |reflexivity]
   |rewrite > mem_append [|*:autobatch]
    rewrite > mem_append [|*:autobatch]
    unfold apartb in H3;unfold apartb in H4;
    autobatch paramodulation
   |cases (y ≟ c1); simplify
    [reflexivity
    |apply H3]]]]]
qed.

lemma subst_X_apart : ∀x,M,N. x # M → subst_X M x N = M.
intros 2;
elim M
[simplify;simplify in H;
 rewrite > p_eqb4
 [reflexivity
 |intro;apply H;autobatch]
|reflexivity
|simplify;rewrite > H
 [rewrite > H1
  [reflexivity
  |intro;apply H2;simplify;autobatch]
 |intro;apply H2;simplify;autobatch]
|simplify;rewrite >H
 [reflexivity
 |apply H1]]
qed.

lemma subst_Y_not_dangling : ∀y,M,N. y ∉ LV M → subst_Y M y N = M.
intros 2;
elim M
[reflexivity
|simplify;simplify in H;
 rewrite > p_eqb4
 [reflexivity
 |intro;apply H;autobatch]
|simplify;rewrite > H
 [rewrite > H1
  [reflexivity
  |intro;apply H2;simplify;autobatch]
 |intro;apply H2;simplify;autobatch]
|simplify;simplify in H1;apply (bool_elim ? (y ≟ c));simplify;intro
 [reflexivity
 |rewrite > H
  [reflexivity
  |intro;apply H1;apply in_list_filter_r;autobatch]]]
qed.

lemma subst_X_lemma : 
  ∀x1,x2,M,P,Q.x1 ≠ x2 → x1 # Q → 
    subst_X (subst_X M x1 P) x2 Q = subst_X (subst_X M x2 Q) x1 (subst_X P x2 Q).
intros;elim M
[simplify;apply (bool_elim ? (x1 ≟ c));simplify;intro
 [rewrite > p_eqb4
  [simplify;rewrite > H2;reflexivity
  |intro;autobatch]
 |apply (bool_elim ? (x2 ≟ c));simplify;intro
  [rewrite > subst_X_apart;autobatch
  |rewrite > H2;reflexivity]]
|reflexivity
|*:simplify;autobatch paramodulation]
qed.

lemma subst_cancel : ∀x,y,M.x # M → M = subst_X (subst_Y M y (Par x)) x (Var y).
intros 3;elim M
[simplify;simplify in H;rewrite > p_eqb4
 [reflexivity
 |intro;autobatch]
|simplify;apply (bool_elim ? (y ≟ c));simplify;intro
 [rewrite > p_eqb3 [|reflexivity]
  simplify;rewrite > (p_eqb1 ??? H1);reflexivity
 |reflexivity]
|simplify;simplify in H2;rewrite < H;
 [rewrite < H1
  [reflexivity
  |intro;apply H2;autobatch]
 |intro; apply H2;autobatch]
|simplify;simplify in H1;apply (bool_elim ? (y ≟ c));
 simplify;intro;
 [rewrite > subst_X_apart
  [reflexivity
  |apply H1]
 |rewrite < H
  [reflexivity
  |apply H1]]]
qed.

lemma subst_X_merge : ∀M,N,x1,x2.x2 # M →
  subst_X (subst_X M x1 (Par x2)) x2 N = subst_X M x1 N.
intros 4;elim M
[simplify;apply (bool_elim ? (x1 ≟ c));simplify;intro
 [rewrite > Neqb_n_n;reflexivity
 |rewrite > p_eqb4
  [reflexivity
  |intro;elim H;simplify;autobatch]]
|reflexivity
|simplify;simplify in H2;rewrite > H
 [rewrite > H1
  [reflexivity
  |intro;autobatch]
 |intro;autobatch]
|simplify;rewrite > H
 [reflexivity
 |apply H1]]
qed.

lemma subst_X_Y_commute : ∀x1,x2,y,M,N. x1 ≠ x2 → y ∉ LV N → 
  subst_Y (subst_X M x1 N) y (Par x2) = subst_X (subst_Y M y (Par x2)) x1 N.
intros;elim M
[simplify;apply (bool_elim ? (x1 ≟ c));simplify;intro
 [rewrite > subst_Y_not_dangling;autobatch
 |reflexivity]
|simplify;apply (bool_elim ? (y ≟ c));simplify;intro
 [rewrite > p_eqb4
  [reflexivity
  |assumption]
 |reflexivity]
|simplify;autobatch paramodulation
|simplify;apply (bool_elim ? (y ≟ c));simplify;intro
 [reflexivity
 |rewrite < H2;reflexivity]]
qed.

inductive LL (F : X → S_exp → Y) : S_exp → Prop ≝ 
| LLPar : ∀x.LL F (Par x)
| LLApp : ∀M,N.LL F M → LL F N → LL F (App M N)
| LLAbs : ∀x1,M.(∀x2.(x2 ∈ GV M → x2 = x1) → LL F (subst_X M x1 (Par x2))) → 
          LL F (Abs (F x1 M) (subst_X M x1 (Var (F x1 M)))).

include "nat/compare.ma".

definition max : nat → nat → nat ≝
  λx,y.match leb x y with
  [ true ⇒ y
  | false ⇒ x ].

let rec S_len M ≝ match M with
[ Par _ ⇒ O
| Var _ ⇒ O
| App N P ⇒ S (max (S_len N) (S_len P))
| Abs x N ⇒ S (S_len N) ].

lemma S_len_ind : 
  ∀P:S_exp → Prop.
    (∀M.(∀N.S_len N < S_len M → P N) → P M)
    → ∀M.P M.
intros;
cut (∀N.S_len N ≤ S_len M → P N)
[|elim M 0;simplify;intros
  [1,2:apply H;intros;elim (not_le_Sn_O (S_len N1));autobatch
  |apply H;intros;generalize in match (trans_le ??? H4 H3);unfold max;
   apply (bool_elim ? (leb (S_len s) (S_len s1)));simplify;intros;autobatch
  |apply H;intros;apply H1;apply le_S_S_to_le;autobatch]]
apply H;intros;autobatch;
qed.

record height : Type ≝
{
  H : X → S_exp → Y;
  HE : ∀M:S_exp. ∀x:X. ∀pi:Pi. (L H M) → H x M = H (pi x) (pi · M);
  HF : ∀M:S_exp. ∀x:X. (L H M) → H x M ∉ E x M;
  HP : ∀M,Q:S_exp. ∀x1,x2:X. (L H M) → (L H Q) → (x1 ≟ x2) = false → 
            apartb x1 Q = true → (H x1 M ≟ H x1 (subst_X M x2 Q)) = true
}.
coercion H 2.

record xheight : Type ≝
{
  XH  : X → S_exp → Y;
  XHE : ∀M:S_exp. ∀x:X. ∀pi:Pi. XH x M = XH (pi x) (pi · M);
  XHF : ∀M:S_exp. ∀x:X. XH x M ∉ E x M;
  XHP : ∀M,Q:S_exp. ∀x1,x2:X.(x1 ≟ x2) = false → 
            apartb x1 Q = true → (XH x1 M ≟ XH x1 (subst_X M x2 Q)) = true
}.
coercion XH 2.

include "logic/coimplication.ma".

definition coincl : ∀A.list A → list A → Prop ≝  λA,l1,l2.∀x.x ∈ l1 ↔ x ∈ l2.

notation > "hvbox(a break ≡ b)"
  non associative with precedence 45
for @{'equiv $a $b}.

notation < "hvbox(term 46 a break ≡ term 46 b)"
  non associative with precedence 45
for @{'equiv $a $b}.

interpretation "list coinclusion" 'equiv x y = (coincl ? x y).

lemma refl_coincl : ∀A.∀l:list A.l ≡ l.
intros;intro;split;intro;assumption;
qed.

lemma filter_append : ∀A,l1,l2,p.filter A (l1@l2) p = filter A l1 p @ filter A l2 p.
intros;elim l1
[reflexivity
|simplify;cases (p a);simplify;rewrite < H;reflexivity]
qed.

lemma GV_subst_X_Var : 
  ∀M,x,y. GV (subst_X M x (Var y)) ≡ filter ? (GV M) (λz.¬(x ≟ z)).
intros;elim M;simplify
[cases (x ≟ c);simplify;autobatch
|autobatch
|intro;split;intro
 [rewrite > filter_append;cases (in_list_append_to_or_in_list ???? H2)
  [cases (H x1);autobatch
  |cases (H1 x1);autobatch]
 |rewrite > filter_append in H2;cases (in_list_append_to_or_in_list ???? H2)
  [cases (H x1);autobatch
  |cases (H1 x1);autobatch]]
|intro;split;intro;cases (H x1);autobatch]
qed.

lemma swap_GV : ∀x,M. x ∈ GV M → ∀x1,x2.swap X x1 x2 x ∈ GV (pi_swap X x1 x2 · M).
intros;elim M in H
[simplify;simplify in H;rewrite > (in_list_singleton_to_eq ??? H);autobatch
|simplify in H;elim (not_in_list_nil ?? H)
|simplify in H2;simplify;cases (in_list_append_to_or_in_list ???? H2);autobatch
|simplify in H1;simplify;autobatch]
qed.

(* easy to prove, but not needed *)
lemma L_swap : ∀F:xheight.∀M.L F M →
               ∀x1,x2.L F (pi_swap ? x1 x2 · M).
intros;elim H
[simplify;autobatch
|simplify;autobatch
|simplify;rewrite > pi_lemma1;simplify;
 rewrite > (?: F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s))
 [apply LAbs;assumption
 |autobatch;]]
qed.

lemma LL_swap : ∀F:xheight.∀M.LL F M →
                ∀x1,x2.LL F (pi_swap ? x1 x2 · M).
intros;elim H
[simplify;autobatch
|simplify;autobatch
|simplify;rewrite > pi_lemma1;simplify;
 rewrite > (?: F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s))
 [apply LLAbs;intros;lapply (H2 (pi_swap ? x1 x2 x))
  [rewrite > (?: Par x = pi_swap ? x1 x2 · (Par (pi_swap ? x1 x2 x)))
   [autobatch
   |elim daemon (*involution*)]
  |intro;rewrite < (swap_inv ? x1 x2 c);
   rewrite < eq_swap_pi;apply eq_f;rewrite > eq_swap_pi;apply H3;
   rewrite < (swap_inv ? x1 x2 x);autobatch]
 |autobatch]]
qed.

(*lemma LL_subst_X : ∀F:xheight.∀M.LL F M → 
                   ∀x1,x2.LL F (subst_X M x1 (Par x2)).
intros 2;apply (S_len_ind ?? M);intro;cases M1;simplify;intros
[cases (x1 ≟ c);simplify;autobatch
|inversion H1;simplify;intros;destruct
|inversion H1;simplify;intros;destruct;
 clear H3 H5;apply LLApp;apply H;try assumption
 [(* len *)elim daemon
 |(* len *)elim daemon]
|inversion H1;simplify;intros;destruct;
   unfold lam in H4;clear H3;destruct;
   apply (bool_elim ? (x1 ≟ c1));intro
   [rewrite > subst_X_apart
    [assumption
    |intro;rewrite > (?: (x1 ≟ c1) = false) in H3
     [destruct
     |elim (GV_subst_X_Var s1 c1 (F c1 s1) x1);
      lapply (H5 H4);lapply (in_list_filter_to_p_true ???? Hletin);
      apply p_eqb4;intro;rewrite > H7 in Hletin1;
      rewrite > Neqb_n_n in Hletin1;simplify in Hletin1;destruct]]
   |letin c2 ≝ (N_fresh ? (x1::x2::c1::GV s1));
    cut (c2 ∉ (x1::x2::c1::GV s1)) as Hc2 [|apply p_fresh]
    clearbody c2;
    rewrite > (? : s1 = subst_X (subst_X s1 c1 (Par c2)) c2 (Par c1)) in ⊢ (? ? (? ? (? (? % ? ?) ? ?)))
    [|rewrite > subst_X_merge
     [autobatch
     |intro;apply Hc2;autobatch depth=4]]
    rewrite > (? : F c1 s1 = F c2 (subst_X s1 c1 (Par c2)))
    [|rewrite > subst_X_fp
     [rewrite < (swap_left ? c1 c2) in ⊢ (? ? ? (? ? % ?));
      rewrite > eq_swap_pi;autobatch
     |intro;elim Hc2;autobatch depth=4]]
    rewrite > subst_X_merge
    [|intro;apply Hc2;do 2 apply in_list_cons;generalize in match H4;
      elim s1 0;simplify;intros
      [apply (bool_elim ? (c1 ≟ c));intro;
       rewrite > H6 in H5;simplify in H5;
       lapply (in_list_singleton_to_eq ??? H5)
       [rewrite > Hletin;autobatch
       |rewrite > Hletin in H6;rewrite > Neqb_n_n in H6;destruct]
      |elim (not_in_list_nil ?? H5)
      |cases (in_list_append_to_or_in_list ???? H7)
       [cases (in_list_cons_case ???? (H5 H8));autobatch
       |cases (in_list_cons_case ???? (H6 H8));autobatch]
      |autobatch]]
    rewrite > (subst_X_lemma c2 x1 ? ??)
    [simplify;rewrite > (? : F c2 (subst_X s1 c1 (Par c2)) = F c2 (subst_X (subst_X s1 c1 (Par c2)) x1 (Par x2)))
     [|apply p_eqb1;apply XHP;
      [apply p_eqb4;intro;apply Hc2;autobatch
      |simplify;rewrite > (? : (c2 ≟ x2) = false)
       [reflexivity
       |apply p_eqb4;intro;apply Hc2;autobatch]]]
     apply LLAbs;
     intros (x3);
     apply H
     [(*len*)elim daemon
     |3:assumption
     |apply H
      [(*len*)elim daemon
      |apply H2;intro;elim Hc2;autobatch depth=4]]
    |intro;apply Hc2;autobatch
    |simplify;intro;elim Hc2;rewrite > (? : c2 = x2);autobatch]]]
qed.*)

lemma L_to_LL : ∀M.∀F:xheight.L F M → LL F M.
intros;elim H
[autobatch
|autobatch
|apply LLAbs;intros;rewrite > subst_X_fp;autobatch]
qed.

lemma LL_to_L : ∀M.∀F:xheight.LL F M → L F M.
intros;elim H
[1,2:autobatch
|apply LAbs;lapply (H2 c)
 [rewrite > subst_X_x_x in Hletin;assumption
 |intro;reflexivity]]
qed.

lemma subst_X_decompose : 
  ∀x,y,M,N.y ∉ LV M → y ∉ E x M → 
    subst_X M x N = subst_Y (subst_X M x (Var y)) y N.
intros 3;elim M
[simplify;cases (x ≟ c);simplify;
 [rewrite > p_eqb3;autobatch
 |reflexivity]
|simplify;simplify in H;
 rewrite > p_eqb4;
 [reflexivity
 |intro;apply H;autobatch]
|simplify;rewrite < H
 [rewrite < H1
  [reflexivity
  |intro;apply H2;simplify;autobatch
  |intro;apply H3;simplify;autobatch]
 |intro;apply H2;simplify;autobatch
 |intro;apply H3;simplify;autobatch]
|simplify;apply (bool_elim ? (y ≟ c));intros;
 [simplify;apply (bool_elim ? (apartb x s))
  [intro;simplify;
   lapply (apartb_true_to_apart ?? H4);
   rewrite > subst_X_apart
   [rewrite > subst_X_apart
    [reflexivity
    |assumption]
   |assumption]
  |intro;simplify in H2;rewrite > H4 in H2;
   simplify in H2;elim H2;
   rewrite > (p_eqb1 ??? H3);autobatch]
 |simplify;rewrite < H;
  [reflexivity
  |generalize in match H1;simplify;elim (LV s)
   [autobatch
   |intro;cases (in_list_cons_case ???? H6)
    [elim H5;simplify;rewrite < H7;rewrite > H3;simplify;autobatch
    |elim (H4 ? H7);intro;apply H5;simplify;cases (¬ (a ≟ c));simplify;autobatch]]
  |intro;apply H2;simplify;apply (bool_elim ? (apartb x s));intro
   [simplify;rewrite > E_fresh in H4
    [assumption
    |autobatch]
   |simplify;autobatch]]]]
qed.

lemma subst_Y_decompose : 
  ∀x,y,M,N.x # M → 
    subst_Y M y N = subst_X (subst_Y M y (Par x)) x N.
intros 3;elim M
[simplify;simplify in H;rewrite > p_eqb4
 [reflexivity
 |intro;apply H;autobatch]
|simplify;apply (bool_elim ? (y ≟ c));simplify;intro
 [rewrite > Neqb_n_n;reflexivity
 |reflexivity]
|simplify;rewrite < H
 [rewrite < H1
  [reflexivity
  |intro;apply H2;simplify;autobatch]
 |intro;apply H2;simplify;autobatch]
|simplify;simplify in H1;apply (bool_elim ? (y ≟ c));simplify;intro
 [simplify;rewrite > subst_X_apart
  [reflexivity
  |assumption]
 |rewrite < H
  [reflexivity
  |apply H1]]]
qed.

lemma pre_height : ∀x1,x2,y,M.y ∉ E x1 M → y ∉ LV M → 
  subst_X M x1 (Par x2) = subst_Y (subst_X M x1 (Var y)) y (Par x2).
intros;apply subst_X_decompose;assumption;
qed.

lemma HL_conv : ∀x,y,M.y ∈ E x M → M ≠ subst_Y (subst_X M x (Var y)) y (Par x).
intros 3;elim M
[simplify in H;elim (not_in_list_nil ?? H);
|simplify in H;elim (not_in_list_nil ?? H)
|simplify;intro;simplify in H2;destruct;
 cases (in_list_append_to_or_in_list ???? H2);autobatch
|simplify;simplify in H1;
 cut (apartb x s = false)
 [rewrite > Hcut in H1;simplify in H1;apply (bool_elim ? (y ≟ c));intro
  [simplify;intro;cut (¬ x # s)
   [apply Hcut1;generalize in match H3;elim s 0;simplify;
    [intro;apply (bool_elim ? (x ≟ c1));simplify;intros;
     [destruct
     |autobatch]
    |intros;autobatch
    |intros;destruct;intro;cases (in_list_append_to_or_in_list ???? H3)
     [apply H4
      [demodulate all
      |assumption]
     |apply H5
      [demodulate all
      |assumption]]
    |intros;destruct;apply H4;demodulate all]
   |intro;rewrite > (apart_to_apartb_true ?? H4) in Hcut;destruct]
  |simplify;intro;apply H
   [cases (in_list_cons_case ???? H1)
    [rewrite > p_eqb3 in H2
     [destruct
     |assumption]
    |assumption]
   |destruct;assumption]]
 |generalize in match H1;cases (apartb x s);simplify;intro
  [elim (not_in_list_nil ?? H2)
  |reflexivity]]]
qed.

let rec BV t ≝ match t with
  [ Par _ ⇒ []
  | Var _ ⇒ []
  | App t1 t2 ⇒ BV t1 @ BV t2
  | Abs y u ⇒ y::BV u ].

lemma E_BV : ∀x,M.E x M ⊆ BV M.
intros;elim M;simplify
[1,2:unfold;intros;assumption
|unfold;intros;cases (in_list_append_to_or_in_list ???? H2);autobatch
|cases (apartb x s);simplify
 [unfold;intros;elim (not_in_list_nil ?? H1)
 |autobatch]]
qed.
     
(*
let rec L_check (F:xheight) M on M ≝ match M with
  [ Par _ ⇒ true
  | Var _ ⇒ false
  | App N P ⇒ andb (L_check F N) (L_check F P)
  | Abs y N ⇒ let X ≝ (N_fresh ? (GV M)) in 
              andb (y ≟ F X (subst_Y N y (Par X)))
                   (L_check F (subst_Y N y (Par X))) ]. 
*)

let rec L_check_aux (F:xheight) M n on n ≝ match n with
[ O   ⇒ false (* vacuous *)
| S m ⇒ match M with
  [ Par _ ⇒ true
  | Var _ ⇒ false
  | App N P ⇒ andb (L_check_aux F N m) (L_check_aux F P m)
  | Abs y N ⇒ let X ≝ (N_fresh ? (GV M)) in 
              andb (y ≟ F X (subst_Y N y (Par X)))
                   (L_check_aux F (subst_Y N y (Par X)) m) ]].

lemma L_check_aux_sound : 
  ∀F,M,n.S_len M ≤ n → L_check_aux F M (S n) = true → L F M.
intros 2;apply (S_len_ind ?? M);intro;cases M1;intros
[autobatch
|simplify in H2;destruct
|simplify in H2;generalize in match H2;
 apply (andb_elim (L_check_aux F s n) (L_check_aux F s1 n));
 apply (bool_elim ? (L_check_aux F s n));simplify;intros
 [apply LApp
  [apply (H ?? (pred n))
   [simplify;(*len*)elim daemon
   |simplify in H1;generalize in match H1;cases n;intros
    [elim (not_le_Sn_O ? H5)
    |simplify;elim daemon (* H5 *)]
   |(* H3 *) elim daemon]
  |apply (H ?? (pred n))
   [simplify;(*len*) elim daemon
   |simplify in H1;generalize in match H1;cases n;intros
    [elim (not_le_Sn_O ? H5)
    |simplify;elim daemon (* H5 *)]
   |(* H4 *) elim daemon]]
 |destruct]
|simplify in H2;generalize in match H2;clear H2;
 apply (andb_elim (c ≟ F (N_fresh X (GV s)) (subst_Y s c (Par (N_fresh X (GV s))))) 
                  (L_check_aux F (subst_Y s c (Par (N_fresh X (GV s)))) n));
 apply (bool_elim ? (c≟F (N_fresh X (GV s)) (subst_Y s c (Par (N_fresh X (GV s))))));
 simplify;intros
 [rewrite > (p_eqb1 ??? H2);
  rewrite > (? : s = 
                 subst_X 
                   (subst_Y s c
                     (Par (N_fresh X (GV s))))
                   (N_fresh X (GV s))
                   (Var (F (N_fresh X (GV s)) (subst_Y s c (Par (N_fresh X (GV s)))))))
          in ⊢ (?? (?? %))
  [apply LAbs;apply (H ?? (pred n))
   [simplify;(*len*)elim daemon
   |simplify in H1;generalize in match H1;cases n;intros
    [elim (not_le_Sn_O ? H4)
    |simplify;elim daemon (* H4 *)]
   |rewrite > (? : S (pred n) = n)
    [assumption
    |(*arith*)elim daemon]]
  |rewrite < subst_Y_decompose
   [rewrite < (p_eqb1 ??? H2);autobatch
   |apply p_fresh]]
 |destruct]]
qed.

lemma LV_subst_X : ∀s,x,y. LV (subst_X s x (Var y)) ⊆ y::LV s.
intros 3;elim s
[simplify;cases (x ≟ c);simplify;
 [autobatch
 |unfold;intros;elim (not_in_list_nil ?? H)]
|simplify;unfold;intros;autobatch
|simplify;unfold;intros;
 cases (in_list_append_to_or_in_list ???? H2)
 [lapply (H ? H3);autobatch
 |lapply (H1 ? H3);cases (in_list_cons_case ???? Hletin)
  [applyS in_list_head
  |autobatch]]
|simplify;unfold;intros;
 lapply (in_list_filter ???? H1);
 lapply (H ? Hletin);
 cases (in_list_cons_case ???? Hletin1)
 [rewrite > H2;autobatch
 |apply in_list_cons;apply in_list_filter_r
  [assumption
  |apply (in_list_filter_to_p_true ???? H1)]]]
qed.

lemma eq_list_nil : ∀A.∀l:list A.(∀x.x ∉ l) → l = [].
intros 2;cases l;intro
[reflexivity
|elim (H a);autobatch]
qed.

(* to be revised *)
lemma L_to_closed : ∀F:xheight.∀M.L F M → LV M = [].
intros;elim H
[reflexivity
|simplify;autobatch paramodulation
|simplify;generalize in match H2;generalize in match (F c s);elim s
 [simplify;apply (bool_elim ? (c ≟ c1));simplify;intro
  [rewrite > p_eqb3;reflexivity
  |reflexivity]
 |simplify in H3;destruct
 |simplify in H5;simplify;
  rewrite > (? : 
    filter Y (LV (subst_X s1 c (Var c1))@LV (subst_X s2 c (Var c1))) (λz.¬(z≟c1)) =
    filter Y (LV (subst_X s1 c (Var c1))) (λz.¬(z≟c1))@ filter Y (LV (subst_X s2 c (Var c1))) (λz.¬(z≟c1)))
  [rewrite > H3
   [rewrite > H4
    [reflexivity
    |generalize in match H5;cases (LV s2);simplify;
     [intro;reflexivity
     |cases (LV s1);simplify;intro;destruct]]
   |generalize in match H5;cases (LV s1);simplify;intro
    [reflexivity
    |destruct]]
  |elim (LV (subst_X s1 c (Var c1)));simplify
   [reflexivity
   |cases (a ≟ c1);simplify;rewrite > H6;reflexivity]]
 |simplify;apply eq_list_nil;intro;intro;
  lapply (in_list_filter ???? H5) as H6;
  lapply (in_list_filter ???? H6) as H7;
  lapply (in_list_filter_to_p_true ???? H5) as H8;
  lapply (in_list_filter_to_p_true ???? H6) as H9;
  lapply (LV_subst_X ???? H7);
  cut (LV s1 ⊆ [c1])
  [cases (in_list_cons_case ???? Hletin)
   [rewrite > (p_eqb3 ??? H10) in H8;simplify in H8;destruct
   |lapply (Hcut ? H10);lapply (in_list_singleton_to_eq ??? Hletin1);
    rewrite > (p_eqb3 ??? Hletin2) in H9;simplify in H9;destruct]
  |simplify in H4;generalize in match H4;elim (LV s1) 0;simplify
   [intro;unfold;intros;elim (not_in_list_nil ?? H11)
   |intros 2;apply (bool_elim ? (a ≟ c1));simplify;intros
    [unfold;intros;cases (in_list_cons_case ???? H13)
     [rewrite > H14;rewrite > (p_eqb1 ??? H10);autobatch
     |apply H11;autobatch]
    |destruct]]]]]
qed.

lemma fresh_GV_subst_X_Var : ∀s,c,y.
  N_fresh X (GV (subst_X s c (Var y))) ∈ GV s → 
    N_fresh X (GV (subst_X s c (Var y))) = c.
intros;apply p_eqb1;
apply (bool_elim ? (N_fresh X (GV (subst_X s c (Var y)))≟c));intro
[reflexivity
|lapply (p_eqb2 ??? H1);lapply (p_fresh ? (GV (subst_X s c (Var y))));
 lapply (GV_subst_X_Var s c y);
 elim Hletin1;cases (Hletin2 (N_fresh X (GV (subst_X s c (Var y)))));
 apply H3;apply in_list_filter_r
 [assumption
 |change in ⊢ (???%) with (¬false);apply eq_f;
  apply p_eqb4;intro;elim (p_eqb2 ??? H1);autobatch]]
qed.

lemma L_check_aux_complete :
  ∀F:xheight.∀M.LL F M → ∀n.S_len M ≤ n → L_check_aux F M (S n) = true.
intros 3;elim H
[reflexivity
|simplify;simplify in H5;rewrite > (? : n = S (pred n))
 [rewrite > H2
  [rewrite > H4
   [reflexivity
   |(* H5 *) elim daemon]
  |(* H5 *) elim daemon]
 |(* H5 *) elim daemon]
|simplify;simplify in H3;
 rewrite > (? : (F c s ≟ F (N_fresh X (GV (subst_X s c (Var (F c s)))))
                          (subst_Y (subst_X s c (Var (F c s))) (F c s)
                            (Par (N_fresh X (GV (subst_X s c (Var (F c s))))))))
                = true)
 [simplify;
  rewrite > (? : subst_Y (subst_X s c (Var (F c s))) (F c s)
                  (Par (N_fresh X (GV (subst_X s c (Var (F c s)))))) =
                  subst_X s c (Par (N_fresh X (GV (subst_X s c (Var (F c s)))))))
  [rewrite > (? : n = S (pred n))
   [rewrite > H2
    [reflexivity
    |autobatch
    |(* H3 *) elim daemon]
   |(* H3 *) elim daemon]
  |rewrite < subst_X_decompose
   [reflexivity
   |rewrite > (L_to_closed F)
    [autobatch
    |lapply (H1 c)
     [autobatch
     |intro;reflexivity]]
   |autobatch]]
 |rewrite < subst_X_decompose
  [rewrite > subst_X_fp
   [rewrite < (swap_left X c) in ⊢ (? ? (? ? ? (? ? % ?)) ?);
    autobatch
   |autobatch]
  |rewrite > (L_to_closed F)
   [autobatch
   |lapply (H1 c)
    [autobatch
    |intro;reflexivity]]
  |autobatch]]]
qed.

inductive typ : Type ≝ 
| TPar : X → typ
| Fun  : typ → typ → typ.

notation "hvbox(a break ▸ b)" 
  left associative with precedence 50
for @{ 'blacktriangleright $a $b }.
interpretation "STT arrow type" 'blacktriangleright a b = (Fun a b).

include "datatypes/constructors.ma".

definition DOM : list (X × typ) → list X ≝ λC.map ?? (fst ??) C.

inductive context : list (X × typ) → Prop ≝ 
| ctx_nil  : context []
| ctx_cons : ∀x,t,C.x ∉ DOM C → context C → context (〈x,t〉::C).

(* ▸ = \rtrif *)
inductive typing (F:xheight): list (X × typ) → S_exp → typ → Prop ≝
| t_axiom : ∀C,x,t.context C → 〈x,t〉 ∈ C → typing F C (Par x) t
| t_App : ∀C,M,N,t,u.typing F C M (t ▸ u) → typing F C N t → 
          typing F C (App M N) u
| t_Lam : ∀C,x,M,t,u.x ∉ DOM C → typing F (〈x,t〉::C) M u → 
          typing F C (Abs (F x M) (subst_X M x (Var (F x M)))) (t ▸ u).

inductive typing2 (F:xheight): list (X × typ) → S_exp → typ → Prop ≝
| t2_axiom : ∀C,x,t.context C → 〈x,t〉 ∈ C → typing2 F C (Par x) t
| t2_App : ∀C,M,N,t,u.typing2 F C M (t ▸ u) → typing2 F C N t → 
          typing2 F C (App M N) u
| t2_Lam : ∀C,x1,M,t,u.
          (∀x2.x2 ∉ DOM C → (x2 ∈ GV M → x2 = x1) → 
            typing2 F (〈x2,t〉::C) (subst_X M x1 (Par x2)) u) → 
          typing2 F C (Abs (F x1 M) (subst_X M x1 (Var (F x1 M)))) (t ▸ u).

notation > "C ⊢[F] M : t" 
  non associative with precedence 30 for @{ 'typjudg F $C $M $t }.  
notation > "C ⊢ M : t" 
  non associative with precedence 30 for @{ 'typjudg ? $C $M $t }.  
notation < "mstyle color #007f00 (hvbox(C maction (⊢) (⊢ \sub F) break M : break t))" 
  non associative with precedence 30 for @{ 'typjudg $F $C $M $t }.  
interpretation "Fsub subtype judgement" 'typjudg F C M t = (typing F C M t).

notation > "C ⊨[F] M : t" 
  non associative with precedence 30 for @{ 'typjudg2 F $C $M $t }.  
notation > "C ⊨ M : t" 
  non associative with precedence 30 for @{ 'typjudg2 ? $C $M $t }.  
notation < "mstyle color #007f00 (hvbox(C maction (⊨) (⊨ \sub F) break M : break t))" 
  non associative with precedence 30 for @{ 'typjudg2 $F $C $M $t }.  
interpretation "Fsub strong subtype judgement" 'typjudg2 F C M t = (typing2 F C M t).

lemma in_ctx_to_in_DOM : ∀x,t.∀C:list (X × typ).〈x,t〉 ∈ C → x ∈ DOM C.
intros 3;elim C
[elim (not_in_list_nil ?? H)
|elim (in_list_cons_case ???? H1)
 [rewrite < H2;simplify;autobatch
 |cases a;simplify;autobatch]]
qed.

lemma in_DOM_to_in_ctx : ∀x,C.x ∈ DOM C → ∃t.〈x,t〉 ∈ C.
intros 2;elim C
[elim (not_in_list_nil X ? H)
|elim a in H1;simplify in H1;elim (in_list_cons_case ???? H1)
 [rewrite > H2;autobatch
 |cases (H H2);autobatch]]
qed.

lemma incl_DOM : ∀l1,l2. l1 ⊆ l2 → DOM l1 ⊆ DOM l2.
intros;unfold in H;unfold;intros;cases (in_DOM_to_in_ctx ?? H1);autobatch;
qed.

lemma typing2_weakening : ∀F,C,M,t.
                         C ⊨[F] M : t → ∀D.context D → C ⊆ D → D ⊨[F] M : t.
intros 5;elim H;try autobatch size=7;
apply t2_Lam;intros;apply H2;
[intro;autobatch
|*:autobatch]
qed.

definition swap_list : ∀N:Nset.N → N → list N → list N ≝
  λN,a,b,l.map ?? (pi_swap ? a b) l.

lemma in_list_swap : ∀N:Nset.∀x,l.x ∈ l → ∀a,b.swap N a b x ∈ swap_list N a b l.
intros;elim H;simplify;autobatch;
qed.

definition ctx_swap_X : X → X → list (X × typ) → list (X × typ) ≝ 
  λx1,x2,C.map ?? (λp.
    match p with 
    [pair x t ⇒ 〈pi_swap ? x1 x2 x,t〉]) C.

lemma in_ctx_swap : ∀x,t,C.〈x,t〉 ∈ C → ∀a,b.〈swap ? a b x,t〉 ∈ ctx_swap_X a b C.
intros;generalize in match H;elim C;
[elim (not_in_list_nil ?? H1)
|simplify;inversion H2;simplify;intros;destruct;simplify;autobatch]
qed.

lemma ctx_swap_X_swap_list : 
  ∀C,x1,x2.DOM (ctx_swap_X x1 x2 C) = swap_list ? x1 x2 (DOM C).
intros;elim C
[reflexivity
|cases a;simplify;autobatch]
qed.

lemma swap_list_inv : ∀N,x1,x2,l.swap_list N x1 x2 (swap_list N x1 x2 l) = l.
intros;elim l;simplify;autobatch;
qed.

lemma context_eqv : ∀C.context C → ∀a,b.context (ctx_swap_X a b C).
intros;elim H
[simplify;autobatch
|simplify;apply ctx_cons
 [intro;apply H1;rewrite > ctx_swap_X_swap_list in H4;
  rewrite < (swap_inv ? a b);
  rewrite < (swap_list_inv ? a b);autobatch
 |assumption]]
qed.

lemma typing_swap : ∀F:xheight.∀C,M,t,x1,x2.
  C ⊨[F] M : t → ctx_swap_X x1 x2 C ⊨[F] (pi_swap ? x1 x2)·M : t.
intros;elim H
[simplify;apply t2_axiom
 [autobatch
 |rewrite < eq_swap_pi;autobatch]
|simplify;autobatch
|simplify;rewrite > pi_lemma1;simplify;applyS t2_Lam;
 intros;rewrite < (swap_inv ? x1 x2 x);
 change in ⊢ (? ? ? (? ? ? %) ?) with (pi_swap X x1 x2 · Par (swap X x1 x2 x));
 rewrite < pi_lemma1;apply H2
 [intro;apply H3;rewrite < (swap_inv ? x1 x2 x);
  rewrite > ctx_swap_X_swap_list;autobatch
 |intro;rewrite > H4;autobatch]]
qed.

lemma typing_to_typing2 : ∀F:xheight.∀C,M,t.C ⊢[F] M : t → C ⊨[F] M : t.
intros;elim H;try autobatch;
apply t2_Lam;intros;
rewrite > subst_X_fp
[rewrite > (? : 〈x2,t1〉::l = ctx_swap_X c x2 (〈c,t1〉::l))
 [autobatch
 |simplify;rewrite < eq_swap_pi;rewrite > swap_left;
  rewrite < (? : l = ctx_swap_X c x2 l)
  [reflexivity
  |generalize in match H1;generalize in match H4;elim l 0
   [intros;reflexivity
   |intro;cases a;simplify;intros;
    rewrite < eq_swap_pi;rewrite > swap_other
    [rewrite < H6
     [reflexivity
     |*:intro;autobatch]
    |*:intro;autobatch]]]]
|assumption]
qed.

lemma typing2_to_typing : ∀F:xheight.∀C,M,t.C ⊨[F] M : t → C ⊢[F] M : t.
intros;elim H;try autobatch;
generalize in match (p_fresh ? (c::DOM l@GV s));
generalize in match (N_fresh ? (c::DOM l@GV s));
intros (xn f_xn);
lapply (H2 xn)
[rewrite > subst_X_fp in Hletin
 [lapply (t_Lam ??????? Hletin)
  [intro;apply f_xn;autobatch
  |rewrite < subst_X_fp in Hletin1
   [rewrite > subst_X_merge in Hletin1
    [rewrite < (? : F c s = F xn (subst_X s c (Par xn))) in Hletin1
     [assumption
     |rewrite > subst_X_fp
      [rewrite < (swap_left ? c xn) in ⊢ (? ? ? (? ? % ?));
       rewrite > eq_swap_pi;autobatch]]]]]]]
intro;elim f_xn;autobatch;
qed.