From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Tue, 6 Mar 2012 18:01:33 +0000 (+0000)
Subject: commit by user ricciott
X-Git-Tag: make_still_working~1893
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4d18494d87350c31e679a540bb2638cd821343f4;p=helm.git

commit by user ricciott
---

diff --git a/weblib/cr/lambda.ma b/weblib/cr/lambda.ma
new file mode 100644
index 000000000..493f63304
--- /dev/null
+++ b/weblib/cr/lambda.ma
@@ -0,0 +1,1696 @@
+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:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a T1.∀l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a T2.∀P:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a T1 → a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a T2 → Prop.
+  a href="cic:/matita/basics/list/length.fix(0,1,1)"length/a ? l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/list/length.fix(0,1,1)"length/a ? l2 →
+  (P (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a ?) (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a ?)) → 
+  (∀hd1,hd2,tl1,tl2. P tl1 tl2 → P (hd1a title="cons" href="cic:/fakeuri.def(1)":/a:tl1) (hd2a title="cons" href="cic:/fakeuri.def(1)":/a: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 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g x) → a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B f l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B g l.
+#A #B #f #g #l #Efg
+elim l normalize //
+qed.
+
+lemma le_length_filter : ∀A,l,p.a href="cic:/matita/basics/list/length.fix(0,1,1)"length/a A (a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l) a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/basics/list/length.fix(0,1,1)"length/a A l.
+#A #l #p elim l normalize
+[//
+|#a #tl #IH cases (p a) normalize
+ [@a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a //
+ |%2 //
+ ]
+]
+qed.
+
+lemma length_append : ∀A,l,m.a href="cic:/matita/basics/list/length.fix(0,1,1)"length/a A (la title="append" href="cic:/fakeuri.def(1)"@/am) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/list/length.fix(0,1,1)"length/a A l a title="natural plus" href="cic:/fakeuri.def(1)"+/a a href="cic:/matita/basics/list/length.fix(0,1,1)"length/a A m.
+#A #l #m elim l
+[//
+|#H #tl #IH normalize <IH //]
+qed.
+
+inductive in_list (A:Type[0]): A → (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) → Prop ≝
+| in_list_head : ∀ x,l.(in_list A x (xa title="cons" href="cic:/fakeuri.def(1)":/a:l))
+| in_list_cons : ∀ x,y,l.(in_list A x l) → (in_list A x (ya title="cons" href="cic:/fakeuri.def(1)":/a:l)).
+
+definition incl : ∀A.(a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) → (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) → Prop ≝
+  λA,l,m.∀x.a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x l → a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a 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.a title="logical not" href="cic:/fakeuri.def(1)"¬/a a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x a title="nil" href="cic:/fakeuri.def(1)"[/a].
+(*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.a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) →
+                          x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a a title="logical or" href="cic:/fakeuri.def(1)"∨/a a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x l.
+(*intros;inversion H;intros
+  [destruct H2;left;reflexivity
+  |destruct H4;right;assumption]
+qed.*)
+
+axiom in_list_tail : ∀l,x,y.
+      a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a x (ya title="cons" href="cic:/fakeuri.def(1)":/a:l) → x a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a y → a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a x l.
+(*intros 4;elim (in_list_cons_case ? ? ? ? H)
+  [elim (H2 H1)
+  |assumption]
+qed.*)
+
+axiom in_list_singleton_to_eq : ∀A,x,y.a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x (ya title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]) → x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 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.a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a ? x l1 → a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a ? x (l1a title="append" href="cic:/fakeuri.def(1)"@/al2).
+(*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. a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a ? x l2 → a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a ? x (l1a title="append" href="cic:/fakeuri.def(1)"@/al2).
+(*intros 3.
+elim l1;simplify
+  [assumption
+  |apply in_list_cons;apply H;assumption
+  ]
+qed.*)
+
+lemma in_list_append_elim: 
+  ∀A,x,l1,l2.a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x (l1a title="append" href="cic:/fakeuri.def(1)"@/al2) → 
+  ∀P:Prop.(a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x l1 → P) → (a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a 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; @(a href="cic:/matita/cr/lambda/in_list_inv_ind.def(2)"in_list_inv_ind/a ? x … H)
+  [#a1 #al1 #e0 #e1 destruct /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/cr/lambda/in_list.con(0,1,1)"in_list_head/a/span/span/
+  |#a1 #a2 #al1 #H3 #H4 #e1 #e2 destruct @(IH l2) /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/cr/lambda/in_list.con(0,2,1)"in_list_cons/a/span/span/
+  ]
+]
+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 → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a;
+  p_eqb1  : ∀x,y.N_eqb x y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y;
+  p_eqb2  : ∀x,y.N_eqb x y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → x a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a y; 
+  N_fresh : a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a carrier → carrier;
+  p_fresh : ∀l.N_fresh l a title="list not member" href="cic:/fakeuri.def(1)"∉/a l
+}.
+
+lemma bool_elim : 
+∀P:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → Prop.∀b.(b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → P a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) → (b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → P a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a) → P b.
+#P * /span class="autotactic"2span class="autotrace" trace /span/span/
+qed.
+
+lemma p_eqb3 : ∀X,x,y.x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y → a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"N_eqb/a X x y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
+#X #x #y @(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"N_eqb/a X x y)) //
+#H1 cases (a href="cic:/matita/cr/lambda/p_eqb2.fix(0,0,3)"p_eqb2/a ??? H1) #H2 #H3 cases (H2 H3)
+qed.
+
+lemma p_eqb4 : ∀X,x,y.x a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a y → a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"N_eqb/a X x y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a.
+#X #x #y #H1 @(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"N_eqb/a X x y)) //
+#H2 cases H1 #H3 cases (H3 (a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a ??? H2))
+qed.
+
+axiom X : a href="cic:/matita/cr/lambda/Nset.ind(1,0,0)"Nset/a.
+
+inductive pre_tm : Type[0] ≝
+| Par : a href="cic:/matita/cr/lambda/X.dec"X/a → pre_tm
+| Var : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → pre_tm
+| App : pre_tm → pre_tm → pre_tm
+| Abs : pre_tm → pre_tm.
+
+inductive tm_level : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → Prop ≝ 
+| tml_Par : ∀n,x.tm_level n (a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a x)
+| tml_Var : ∀n,m.n a title="natural 'greater than'" href="cic:/fakeuri.def(1)">/a m → tm_level n (a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"Var/a m)
+| tml_App : ∀n,M1,M2.tm_level n M1 → tm_level n M2 → tm_level n (a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a M1 M2)
+| tml_Abs : ∀n,M0.tm_level (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n) M0 → tm_level n (a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a M0).
+
+record ext_tm (l:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) : Type[0] ≝ {
+  tm_of_etm :> a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a;
+  etm_level : a href="cic:/matita/cr/lambda/tm_level.ind(1,0,0)"tm_level/a 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 : a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a ≝ 
+  match t with 
+  [ Par x2 ⇒ match x a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a x2 with
+    [ true ⇒ u
+    | false ⇒ t ]
+  | Var _ ⇒ t
+  | App t1 t2 ⇒ a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a (subst t1 x u) (subst t2 x u)
+  | Abs t1 ⇒ a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a (subst t1 x u) ].
+
+let rec nth A (xl:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) n on xl ≝ 
+  match xl with
+  [ nil ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a A
+  | cons x0 xl0 ⇒ match n with
+    [ O ⇒ a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a A x0
+    | S m ⇒ nth A xl0 m ] ].
+    
+(* it's necessary to specify Nset... unification hint? *)    
+let rec posn (A:a href="cic:/matita/cr/lambda/Nset.ind(1,0,0)"Nset/a) (xl:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) x on xl ≝ 
+  match xl with
+  [ nil ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a
+  | cons x0 xl0 ⇒ match x a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a x0 with
+    [ true ⇒ a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a
+    | false ⇒ match posn A xl0 x with
+      [ None ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a
+      | Some n ⇒ a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n) ] ] ].
+
+let rec vopen t xl k on t ≝ 
+  match t with
+  [ Par _ ⇒ t
+  | Var n ⇒ match a href="cic:/matita/cr/lambda/nth.fix(0,1,1)"nth/a ? xl (na title="natural plus" href="cic:/fakeuri.def(1)"+/ak) with
+    [ None ⇒ t
+    | Some x ⇒ a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a x ]
+  | App t1 t2 ⇒ a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a (vopen t1 xl k) (vopen t2 xl k)
+  | Abs t1 ⇒ a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a (vopen t1 xl (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a k)) ].
+
+let rec vclose t xl k on t ≝ 
+  match t with
+  [ Par x0 ⇒ match a href="cic:/matita/cr/lambda/posn.fix(0,1,3)"posn/a ? xl x0 with
+    [ None ⇒ t
+    | Some n ⇒ a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"Var/a (na title="natural plus" href="cic:/fakeuri.def(1)"+/ak) ]
+  | Var n ⇒ t
+  | App t1 t2 ⇒ a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a (vclose t1 xl k) (vclose t2 xl k)
+  | Abs t1 ⇒ a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a (vclose t1 xl (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a k)) ].
+
+let rec GV t ≝
+  match t with
+  [ Par x ⇒ xa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a] 
+  | Var _ ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a]
+  | App u v ⇒ GV u a title="append" href="cic:/fakeuri.def(1)"@/a 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:a href="cic:/matita/cr/lambda/Nset.ind(1,0,0)"Nset/a) : Type[0] ≝
+{ 
+  fp_perm       :1> X → X;
+  fp_injective  :  a href="cic:/matita/basics/relations/injective.def(1)"injective/a ?? fp_perm;
+  fp_surjective :  a href="cic:/matita/basics/relations/surjective.def(1)"surjective/a ?? fp_perm;
+  fp_finite     :  a title="exists" href="cic:/fakeuri.def(1)"∃/al.∀x.x a title="list not member" href="cic:/fakeuri.def(1)"∉/a l → fp_perm x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x
+}.
+
+definition Pi ≝ a href="cic:/matita/cr/lambda/fp.ind(1,0,1)"fp/a a href="cic:/matita/cr/lambda/X.dec"X/a.
+
+record fp_pre_tm : Type[0] ≝
+{
+  fppt_perm       :1> a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a;
+  fppt_injective  :  a href="cic:/matita/basics/relations/injective.def(1)"injective/a ?? fppt_perm;
+  fppt_surjective :  a href="cic:/matita/basics/relations/surjective.def(1)"surjective/a ?? 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:a href="cic:/matita/cr/lambda/fp.ind(1,0,1)"fp/a a href="cic:/matita/cr/lambda/X.dec"X/a) t on t : a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a ≝
+  match t with
+  [ Par x ⇒ a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a (p x)
+  | Var _ ⇒ t
+  | App u v ⇒ a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a (mapX p u) (mapX p v)
+  | Abs u ⇒ a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a (mapX p u) ].
+  
+definition swap : ∀N:a href="cic:/matita/cr/lambda/Nset.ind(1,0,0)"Nset/a.N → N → N → N ≝
+  λN,u,v,x.match (x a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a u) with
+    [true ⇒ v
+    |false ⇒ match (x a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a v) with
+       [true ⇒ u
+       |false ⇒ x]].
+
+lemma Neqb_n_n : ∀N:a href="cic:/matita/cr/lambda/Nset.ind(1,0,0)"Nset/a.∀n:N.(n a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a n) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
+#N #n /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/cr/lambda/p_eqb3.def(4)"p_eqb3/a/span/span/
+qed.
+       
+lemma swap_left : ∀N,x,y.(a href="cic:/matita/cr/lambda/swap.def(3)"swap/a N x y x) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y.
+#N #x #y whd in ⊢ (??%?); >(a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"Neqb_n_n/a) //
+qed.
+
+lemma swap_right : ∀N,x,y.(a href="cic:/matita/cr/lambda/swap.def(3)"swap/a N x y y) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x.
+#N #x #y whd in ⊢ (??%?); >(a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"Neqb_n_n/a) @(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (y a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a x)) 
+normalize #H /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a/span/span/
+qed.
+
+lemma swap_other : ∀N,x,y,z.(z a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a x) → (z a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a y) → (a href="cic:/matita/cr/lambda/swap.def(3)"swap/a N x y z) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a z.
+#N #x #y #z #H1 #H2 normalize >(a href="cic:/matita/cr/lambda/p_eqb4.def(4)"p_eqb4/a … H1) 
+normalize >(a href="cic:/matita/cr/lambda/p_eqb4.def(4)"p_eqb4/a … H2) %
+qed.
+
+lemma swap_inv : ∀N,u,v,x.(a href="cic:/matita/cr/lambda/swap.def(3)"swap/a N u v (a href="cic:/matita/cr/lambda/swap.def(3)"swap/a N u v x)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x.
+#N #u #v #x normalize
+@(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (x a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a u)) #H1 >H1 normalize
+[normalize >a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"Neqb_n_n/a normalize
+ @(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (v a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a u)) #H2 normalize
+ [>(a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a … H2) >(a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a … H1) %
+ |>(a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a … H1) %
+ ]
+|@(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (x a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a v)) #H2 normalize
+ [>a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"Neqb_n_n/a normalize >(a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a … H2) %
+ |>H1 >H2 %
+ ]
+]
+qed.
+
+lemma swap_inj : ∀N,u,v.a href="cic:/matita/basics/relations/injective.def(1)"injective/a ?? (a href="cic:/matita/cr/lambda/swap.def(3)"swap/a N u v).
+#N #u #v #x #y normalize @(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (x a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a u)) normalize #H1
+[@(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (y a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a u)) normalize #H2
+ [#H3 >(a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a … H2) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a/span/span/
+ |@(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (y a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a v)) normalize #H3
+  [>(a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a ??? H3) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a/span/span/
+  |#H4 cases (a href="cic:/matita/cr/lambda/p_eqb2.fix(0,0,3)"p_eqb2/a ??? H3) #H5 cases (H5 ?) //
+  ]
+ ]
+|@(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (y a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a u)) normalize #H2
+ [@(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (x a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a v)) normalize #H3 #H4
+  [>H4 in H1; #H1 >H1 in H3;#H3 destruct (H3)
+  |>H4 in H3; >a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"Neqb_n_n/a #H5 destruct (H5)
+  ]
+ |@(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (x a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a v)) normalize #H3
+  [@(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (y a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a v)) normalize #H4 #H5
+   [>(a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a … H4) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a/span/span/
+   |>H5 in H2; >a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"Neqb_n_n/a #H2 destruct (H2)
+   ]
+  |cases (y a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a v) normalize #H4
+   [>H4 in H1; >a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"Neqb_n_n/a #H1 destruct (H1)
+   |//
+   ]
+  ]
+ ]
+]
+qed.
+
+lemma swap_surj : ∀N,u,v.a href="cic:/matita/basics/relations/surjective.def(1)"surjective/a ?? (a href="cic:/matita/cr/lambda/swap.def(3)"swap/a N u v).
+#N #u #v #z normalize @(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (z a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a v)); #H1
+  [%[@u] >a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"Neqb_n_n/a normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a/span/span/
+  |@(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (z a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a u)) #H2
+    [%[@v]
+     >(a href="cic:/matita/cr/lambda/p_eqb4.def(4)"p_eqb4/a ? v u)
+       [>a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"Neqb_n_n/a normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a/span/span/
+       |% #H3 cases (a href="cic:/matita/cr/lambda/p_eqb2.fix(0,0,3)"p_eqb2/a ??? H1) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/
+       ]
+    |%[@z]
+     >H1 >H2 %
+    ]
+  ]
+qed.
+
+lemma swap_finite : ∀N,u,v.a title="exists" href="cic:/fakeuri.def(1)"∃/al.∀x.x a title="list not member" href="cic:/fakeuri.def(1)"∉/a l → (a href="cic:/matita/cr/lambda/swap.def(3)"swap/a N u v) x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x.
+#N #u #v %[@ (ua title="cons" href="cic:/fakeuri.def(1)":/a:va title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a])]
+#x #H1 @a href="cic:/matita/cr/lambda/swap_other.def(5)"swap_other/a % #H2 cases H1 #H3 @H3 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/cr/lambda/in_list.con(0,1,1)"in_list_head/a, a href="cic:/matita/cr/lambda/in_list.con(0,2,1)"in_list_cons/a/span/span/
+qed.
+
+definition pi_swap : ∀N,u,v.a href="cic:/matita/cr/lambda/fp.ind(1,0,1)"fp/a N ≝ 
+λN,u,v.a href="cic:/matita/cr/lambda/fp.con(0,1,1)"mk_fp/a ? (a href="cic:/matita/cr/lambda/swap.def(3)"swap/a N u v) (a href="cic:/matita/cr/lambda/swap_inj.def(6)"swap_inj/a N u v) (a href="cic:/matita/cr/lambda/swap_surj.def(6)"swap_surj/a N u v) (a href="cic:/matita/cr/lambda/swap_finite.def(6)"swap_finite/a N u v).
+
+lemma eq_swap_pi : ∀N,u,v,x.a href="cic:/matita/cr/lambda/swap.def(3)"swap/a N u v x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/cr/lambda/pi_swap.def(7)"pi_swap/a 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.a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a M x (a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a x) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a M.
+#M #x elim M normalize
+[#x0 @(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (x a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a x0)) normalize #H1 /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a, a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a/span/span/
+|*:/span class="autotactic"2span class="autotrace" trace /span/span/]
+qed.
+
+lemma pre_tm_inv_Par : 
+ ∀P:a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → Prop.
+ ∀x.(∀x0.P (a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a x) (a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a x0)) → ∀M.a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a M → P (a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a 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:a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → Prop.
+ ∀n.(∀n0.P (a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"Var/a n) (a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"Var/a n0)) → ∀M.a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"Var/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a M → P (a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"Var/a 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:a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → Prop.
+ ∀M.(∀N0.P (a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a M) (a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a N0)) → ∀N.a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a M a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a N → P (a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a 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:a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → Prop.
+ ∀M1,M2.(∀N1,N2.P (a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a M1 M2) (a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a N1 N2)) → 
+ ∀N.a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a M1 M2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a N → P (a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a 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 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a z → P) → a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a pa title="permutation of pre_tm" href="cic:/fakeuri.def(1)"·/ay → P.
+#P #p #x #y cases y
+[#x0 #H1 #H2 /span class="autotactic"2span class="autotrace" trace /span/span/
+|#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 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"Var/a n0 → P) → a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"Var/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a pa title="permutation of pre_tm" href="cic:/fakeuri.def(1)"·/ay → P.
+#P #p #n #y cases y
+[#x0 #H1 #H2 normalize in H2; destruct (H2)
+|#n0 #H1 #H2 /span class="autotactic"2span class="autotrace" trace /span/span/
+|#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 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a N1 N2 → P) → a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a M1 M2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a pa title="permutation of pre_tm" href="cic:/fakeuri.def(1)"·/ay → 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 /span class="autotactic"2span class="autotrace" trace /span/span/
+|#M0 #H1 #H2 normalize in H2; destruct (H2)
+]
+qed.
+
+lemma Pi_Abs_elim : ∀P:Prop.∀p,M0,y.(∀N0.y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a N0 → P) → a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a M0 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a pa title="permutation of pre_tm" href="cic:/fakeuri.def(1)"·/ay → 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 /span class="autotactic"2span class="autotrace" trace /span/span/
+]
+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 : a href="cic:/matita/cr/lambda/fp.ind(1,0,1)"fp/a a href="cic:/matita/cr/lambda/X.dec"X/a → a href="cic:/matita/cr/lambda/fp_pre_tm.ind(1,0,0)"fp_pre_tm/a.
+#p @a href="cic:/matita/cr/lambda/fp_pre_tm.con(0,1,0)"mk_fp_pre_tm/a
+[@(a href="cic:/matita/cr/lambda/mapX.fix(0,1,3)"mapX/a p)
+|#x elim x
+ [#x0 #y #H1 @(a href="cic:/matita/cr/lambda/Pi_Par_elim.def(4)"Pi_Par_elim/a … H1)
+  #z #H2 >H2 in H1; #H1 normalize in H1; destruct (H1) /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a, a href="cic:/matita/cr/lambda/fp_injective.fix(0,1,3)"fp_injective/a/span/span/
+ |#n #y #H1 @(a href="cic:/matita/cr/lambda/Pi_Var_elim.def(4)"Pi_Var_elim/a … H1)
+  #z #H2 >H2 in H1; #H1 @H1
+ |#M1 #M2 #IH1 #IH2 #y #H1 @(a href="cic:/matita/cr/lambda/Pi_App_elim.def(4)"Pi_App_elim/a … H1)
+  #N1 #N2 #H2 >H2 in H1; #H1 normalize in H1; destruct (H1)
+  generalize in match e1; -e1 >e0 normalize in ⊢ (??%% → ?); #e1 /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/eq_f2.def(3)"eq_f2/a/span/span/
+ |#M0 #IH0 #y #H1 @(a href="cic:/matita/cr/lambda/Pi_Abs_elim.def(4)"Pi_Abs_elim/a … H1)
+  #N0 #H2 >H2 in H1; #H1 normalize in H1; destruct (H1) /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a/span/span/
+ ]
+|#z elim z
+ [#x0 cases (a href="cic:/matita/cr/lambda/fp_surjective.fix(0,1,3)"fp_surjective/a ? p x0) #x1 #H1 %[@(a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a x1)] >H1 %
+ |#n0 %[@(a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"Var/a n0)] %
+ |#M1 #M2 * #N1 #IH1 * #N2 #IH2
+  %[@(a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a N1 N2)] /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/eq_f2.def(3)"eq_f2/a/span/span/
+ |#M0 * #N0 #IH0 %[@(a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a N0)] /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a/span/span/
+]
+qed.
+
+lemma pi_lemma1 : 
+  ∀M,P,x,pi.pi a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"·/a (a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a M x P) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a (pi a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"·/a M) (pi x) (pi a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"·/a P).
+#M #P #x #pi elim M
+[#c normalize @(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (x a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a c)) normalize #H1
+ [cut (pi x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a pi c);
+  [/span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a, a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a/span/span/
+  |#H2 >a href="cic:/matita/cr/lambda/p_eqb3.def(4)"p_eqb3/a // ]
+ |cut (pi x a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a pi c)
+  [% #H2 >(a href="cic:/matita/cr/lambda/fp_injective.fix(0,1,3)"fp_injective/a … H2) in H1; >a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"Neqb_n_n/a #H1 destruct (H1)
+  |#H2 >a href="cic:/matita/cr/lambda/p_eqb4.def(4)"p_eqb4/a // ]
+ ]
+|*: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:a href="cic:/matita/cr/lambda/X.dec"X/a.λM:a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a.a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a (a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"vclose/a M (xa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]) a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a).
+
+definition Judg ≝ λG,M.a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"vclose/a M G a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a.
+
+definition body ≝ λx,M.match M with
+ [ Abs M0 ⇒ a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"vopen/a M (xa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]) a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a
+ | _  ⇒ 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