--- /dev/null
+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 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.
\ No newline at end of file
projects / helm.git / commitdiff