weblib/cr/lambda.ma

   1 include "basics/list.ma".
   2 include "basics/types.ma".
   3
   4 (* LIST THEORY *)
   5 (*theorem nil_cons:
   6   ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
   7 #A;#l;#a; @; #H; ndestruct;
   8 nqed.
   9
  10 ntheorem append_nil: ∀A:Type.∀l:list A.l @ □ = l.
  11 #A;#l;nelim l;//;
  12 #a;#l1;#IH;nnormalize;//;
  13 nqed.
  14
  15 ntheorem associative_append: ∀A:Type[0].associative (list A) (append A).
  16 #A;#x;#y;#z;nelim x
  17 ##[//
  18 ##|#a;#x1;#H;nnormalize;//]
  19 nqed.
  20
  21 ntheorem cons_append_commute:
  22   ∀A:Type[0].∀l1,l2:list A.∀a:A.
  23     a :: (l1 @ l2) = (a :: l1) @ l2.
  24 //;
  25 nqed.
  26
  27 nlemma append_cons: ∀A.∀a:A.∀l,l1. l@(a::l1)=(l@[a])@l1.
  28 #A;#a;#l;#l1;nrewrite > (associative_append ????);//;
  29 nqed.
  30
  31
  32 nlet rec nth A l d n on n ≝
  33   match n with
  34   [ O ⇒ match l with
  35         [ nil ⇒ d
  36         | cons (x : A) _ ⇒ x ]
  37   | S n' ⇒ nth A (tail ? l) d n'].
  38
  39 nlet rec map A B f l on l ≝
  40   match l with [ nil ⇒ nil B | cons (x:A) tl ⇒ f x :: map A B f tl ].
  41
  42 nlet rec foldr (A,B:Type[0]) (f : A → B → B) (b:B) l on l ≝
  43   match l with [ nil ⇒ b | cons (a:A) tl ⇒ f a (foldr A B f b tl) ].
  44
  45 ndefinition length ≝ λT:Type[0].λl:list T.foldr T nat (λx,c.S c) O l.
  46
  47 ndefinition filter ≝
  48   λT:Type[0].λl:list T.λp:T → bool.
  49   foldr T (list T)
  50     (λx,l0.match (p x) with [ true => x::l0 | false => l0]) [] l.
  51
  52 ndefinition iota : nat → nat → list nat ≝
  53   λn,m. nat_rect_Type0 (λ_.list ?) (nil ?) (λx,acc.cons ? (n+x) acc) m.
  54 *)
  55 (* ### induction principle for functions visiting 2 lists in parallel *)
  56 lemma list_ind2 :
  57   ∀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.
  58   \ 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 →
  59   (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 ?)) →
  60   (∀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)) →
  61   P l1 l2.
  62 #T1 #T2 #l1 #l2 #P #Hl #Pnil #Pcons
  63 generalize in match Hl; generalize in match l2;
  64 elim l1
  65 [#l2 cases l2 //
  66  normalize #t2 #tl2 #H destruct
  67 |#t1 #tl1 #IH #l2 cases l2
  68  [normalize #H destruct
  69  |#t2 #tl2 #H @Pcons @IH normalize in H;destruct //]
  70 ]
  71 qed.
  72
  73 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.
  74 #A #B #f #g #l #Efg
  75 elim l normalize //
  76 qed.
  77
  78 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.
  79 #A #l #p elim l normalize
  80 [//
  81 |#a #tl #IH cases (p a) normalize
  82  [@\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"\ 6le_S_S\ 5/a\ 6 //
  83  |%2 //
  84  ]
  85 ]
  86 qed.
  87
  88 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.
  89 #A #l #m elim l
  90 [//
  91 |#H #tl #IH normalize <IH //]
  92 qed.
  93
  94 inductive in_list (A:Type[0]): A → (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) → Prop ≝
  95 | in_list_head : ∀ x,l.(in_list A x (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l))
  96 | 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)).
  97
  98 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 ≝
  99   λ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.
 100
 101 notation "hvbox(a break ∉ b)" non associative with precedence 45
 102 for @{ 'notmem $a $b }.
 103
 104 interpretation "list member" 'mem x l = (in_list ? x l).
 105 interpretation "list not member" 'notmem x l = (Not (in_list ? x l)).
 106 interpretation "list inclusion" 'subseteq l1 l2 = (incl ? l1 l2).
 107
 108 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].
 109 (*intros.unfold.intro.inversion H
 110   [intros;lapply (sym_eq ? ? ? H2);destruct Hletin
 111   |intros;destruct H4]
 112 qed.*)
 113
 114 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) →
 115                           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.
 116 (*intros;inversion H;intros
 117   [destruct H2;left;reflexivity
 118   |destruct H4;right;assumption]
 119 qed.*)
 120
 121 axiom in_list_tail : ∀l,x,y.
 122       \ 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.
 123 (*intros 4;elim (in_list_cons_case ? ? ? ? H)
 124   [elim (H2 H1)
 125   |assumption]
 126 qed.*)
 127
 128 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.
 129 (*intros;elim (in_list_cons_case ? ? ? ? H)
 130   [assumption
 131   |elim (not_in_list_nil ? ? H1)]
 132 qed.*)
 133
 134 axiom in_list_to_in_list_append_l:
 135   ∀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).
 136 (*intros.
 137 elim H;simplify
 138   [apply in_list_head
 139   |apply in_list_cons;assumption
 140   ]
 141 qed.*)
 142
 143 axiom in_list_to_in_list_append_r:
 144   ∀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).
 145 (*intros 3.
 146 elim l1;simplify
 147   [assumption
 148   |apply in_list_cons;apply H;assumption
 149   ]
 150 qed.*)
 151
 152 lemma in_list_append_elim:
 153   ∀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) →
 154   ∀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.
 155 #A #x #l1 elim l1
 156 [ #l2 #H #P #H1 #H2 @H2 @H
 157 | #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)
 158   [#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/
 159   |#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/
 160   ]
 161 ]
 162 qed.
 163
 164
 165 (*
 166 let rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝
 167  match l with
 168   [ nil ⇒ false
 169   | (cons a l') ⇒
 170     match eq x a with
 171      [ true ⇒ true
 172      | false ⇒ mem A eq x l'
 173      ]
 174   ].
 175
 176 naxiom mem_true_to_in_list :
 177   \forall A,equ.
 178   (\forall x,y.equ x y = true \to x = y) \to
 179   \forall x,l.mem A equ x l = true \to in_list A x l.
 180 (* intros 5.elim l
 181   [simplify in H1;destruct H1
 182   |simplify in H2;apply (bool_elim ? (equ x a))
 183      [intro;rewrite > (H ? ? H3);apply in_list_head
 184      |intro;rewrite > H3 in H2;simplify in H2;
 185       apply in_list_cons;apply H1;assumption]]
 186 qed.*)
 187
 188 naxiom in_list_to_mem_true :
 189   \forall A,equ.
 190   (\forall x.equ x x = true) \to
 191   \forall x,l.in_list A x l \to mem A equ x l = true.
 192 (*intros 5.elim l
 193   [elim (not_in_list_nil ? ? H1)
 194   |elim H2
 195     [simplify;rewrite > H;reflexivity
 196     |simplify;rewrite > H4;apply (bool_elim ? (equ a1 a2));intro;reflexivity]].
 197 qed.*)
 198
 199 naxiom in_list_filter_to_p_true : \forall A,l,x,p.
 200 in_list A x (filter A l p) \to p x = true.
 201 (* intros 4;elim l
 202   [simplify in H;elim (not_in_list_nil ? ? H)
 203   |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
 204    simplify in H1
 205      [elim (in_list_cons_case ? ? ? ? H1)
 206         [rewrite > H3;assumption
 207         |apply (H H3)]
 208      |apply (H H1)]]
 209 qed.*)
 210
 211 naxiom in_list_filter : \forall A,l,p,x.in_list A x (filter A l p) \to in_list A x l.
 212 (*intros 4;elim l
 213   [simplify in H;elim (not_in_list_nil ? ? H)
 214   |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
 215    simplify in H1
 216      [elim (in_list_cons_case ? ? ? ? H1)
 217         [rewrite > H3;apply in_list_head
 218         |apply in_list_cons;apply H;assumption]
 219      |apply in_list_cons;apply H;assumption]]
 220 qed.*)
 221
 222 naxiom in_list_filter_r : \forall A,l,p,x.
 223               in_list A x l \to p x = true \to in_list A x (filter A l p).
 224 (* intros 4;elim l
 225   [elim (not_in_list_nil ? ? H)
 226   |elim (in_list_cons_case ? ? ? ? H1)
 227      [rewrite < H3;simplify;rewrite > H2;simplify;apply in_list_head
 228      |simplify;apply (bool_elim ? (p a));intro;simplify;
 229         [apply in_list_cons;apply H;assumption
 230         |apply H;assumption]]]
 231 qed.*)
 232
 233 naxiom incl_A_A: ∀T,A.incl T A A.
 234 (*intros.unfold incl.intros.assumption.
 235 qed.*)
 236
 237 naxiom incl_append_l : ∀T,A,B.incl T A (A @ B).
 238 (*unfold incl; intros;autobatch.
 239 qed.*)
 240
 241 naxiom incl_append_r : ∀T,A,B.incl T B (A @ B).
 242 (*unfold incl; intros;autobatch.
 243 qed.*)
 244
 245 naxiom incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B).
 246 (*unfold incl; intros;elim (in_list_cons_case ? ? ? ? H1);autobatch.
 247 qed.*)
 248
 249 *)
 250
 251
 252 record Nset : Type[1] ≝
 253 {
 254   (* carrier is specified as a coercion: when an object X of type Nset is
 255      given, but something of type Type is expected, Matita will insert a
 256      hidden coercion: the user sees "X", but really means "carrier X"     *)
 257   carrier :> Type[0];
 258   N_eqb   : carrier → carrier → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6;
 259   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;
 260   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;
 261   N_fresh : \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 carrier → carrier;
 262   p_fresh : ∀l.N_fresh l \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 l
 263 }.
 264
 265 lemma bool_elim :
 266 ∀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.
 267 #P * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
 268 qed.
 269
 270 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.
 271 #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)) //
 272 #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)
 273 qed.
 274
 275 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.
 276 #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)) //
 277 #H2 cases H1 #H3 cases (H3 (\ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"\ 6p_eqb1\ 5/a\ 6 ??? H2))
 278 qed.
 279
 280 axiom X : \ 5a href="cic:/matita/cr/lambda/Nset.ind(1,0,0)"\ 6Nset\ 5/a\ 6.
 281
 282 inductive pre_tm : Type[0] ≝
 283 | Par : \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6 → pre_tm
 284 | Var : \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → pre_tm
 285 | App : pre_tm → pre_tm → pre_tm
 286 | Abs : pre_tm → pre_tm.
 287
 288 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 ≝
 289 | tml_Par : ∀n,x.tm_level n (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 x)
 290 | 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)
 291 | 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)
 292 | 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).
 293
 294 record ext_tm (l:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) : Type[0] ≝ {
 295   tm_of_etm :> \ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6;
 296   etm_level : \ 5a href="cic:/matita/cr/lambda/tm_level.ind(1,0,0)"\ 6tm_level\ 5/a\ 6 l tm_of_etm
 297 }.
 298
 299 (*
 300  * we don't want to specify "N_eqb X" or "N_eqb Y" for the equality on X or Y,
 301  * so we use a notation "a ? b" to hide the naming structure
 302  * to type ?, write \equest.
 303  *)
 304 notation > "hvbox(a break ≟ b)"
 305   non associative with precedence 40
 306 for @{ 'equiv ? $a $b }.
 307 notation < "hvbox(a break maction (≟) (≟\sub t) b)"
 308   non associative with precedence 40
 309 for @{ 'equiv $t $a $b }.
 310 interpretation "name decidable equality" 'equiv t a b = (N_eqb t a b).
 311
 312 (* valida solo se u è chiuso *)
 313 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 ≝
 314   match t with
 315   [ Par x2 ⇒ match x \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 x2 with
 316     [ true ⇒ u
 317     | false ⇒ t ]
 318   | Var _ ⇒ t
 319   | 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)
 320   | Abs t1 ⇒ \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 (subst t1 x u) ].
 321
 322 let rec nth A (xl:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) n on xl ≝
 323   match xl with
 324   [ nil ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 A
 325   | cons x0 xl0 ⇒ match n with
 326     [ O ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 A x0
 327     | S m ⇒ nth A xl0 m ] ].
 328
 329 (* it's necessary to specify Nset... unification hint? *)
 330 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 ≝
 331   match xl with
 332   [ 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
 333   | cons x0 xl0 ⇒ match x \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 x0 with
 334     [ 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
 335     | false ⇒ match posn A xl0 x with
 336       [ 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
 337       | 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) ] ] ].
 338
 339 let rec vopen t xl k on t ≝
 340   match t with
 341   [ Par _ ⇒ t
 342   | 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
 343     [ None ⇒ t
 344     | Some x ⇒ \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 x ]
 345   | 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)
 346   | 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)) ].
 347
 348 let rec vclose t xl k on t ≝
 349   match t with
 350   [ Par x0 ⇒ match \ 5a href="cic:/matita/cr/lambda/posn.fix(0,1,3)"\ 6posn\ 5/a\ 6 ? xl x0 with
 351     [ None ⇒ t
 352     | 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) ]
 353   | Var n ⇒ t
 354   | 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)
 355   | 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)) ].
 356
 357 let rec GV t ≝
 358   match t with
 359   [ 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]
 360   | Var _ ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]
 361   | App u v ⇒ GV u \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 GV v
 362   | Abs u ⇒ GV u ].
 363
 364 (* as above, fp_perm is a coercion
 365  * but being a coercion to FunClass, a different syntax is required
 366  * I'll fix this later *)
 367 record fp (X:\ 5a href="cic:/matita/cr/lambda/Nset.ind(1,0,0)"\ 6Nset\ 5/a\ 6) : Type[0] ≝
 368 {
 369   fp_perm       :1> X → X;
 370   fp_injective  :  \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 ?? fp_perm;
 371   fp_surjective :  \ 5a href="cic:/matita/basics/relations/surjective.def(1)"\ 6surjective\ 5/a\ 6 ?? fp_perm;
 372   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
 373 }.
 374
 375 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.
 376
 377 record fp_pre_tm : Type[0] ≝
 378 {
 379   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;
 380   fppt_injective  :  \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 ?? fppt_perm;
 381   fppt_surjective :  \ 5a href="cic:/matita/basics/relations/surjective.def(1)"\ 6surjective\ 5/a\ 6 ?? fppt_perm
 382 }.
 383
 384 (*coercion fp_perm : ∀N:Nset.∀F:fp N.N → N ≝ fp_perm on _F:(fp N) to ? → ?.
 385 coercion fppt_perm : ∀F:fp_pre_tm.pre_tm → pre_tm ≝ fppt_perm on _F:fp_pre_tm to ? → ?.*)
 386
 387 (* notation "p·x" right associative with precedence 60 for @{'middot $p $x}.
 388 interpretation "apply fp" 'middot p x = (fp_perm ? p x).
 389 interpretation "apply fppt" 'middot p x = (fppt_perm p x).*)
 390
 391 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 ≝
 392   match t with
 393   [ Par x ⇒ \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 (p x)
 394   | Var _ ⇒ t
 395   | 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)
 396   | Abs u ⇒ \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 (mapX p u) ].
 397
 398 definition swap : ∀N:\ 5a href="cic:/matita/cr/lambda/Nset.ind(1,0,0)"\ 6Nset\ 5/a\ 6.N → N → N → N ≝
 399   λN,u,v,x.match (x \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 u) with
 400     [true ⇒ v
 401     |false ⇒ match (x \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 v) with
 402        [true ⇒ u
 403        |false ⇒ x]].
 404
 405 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.
 406 #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/
 407 qed.
 408
 409 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.
 410 #N #x #y whd in ⊢ (??%?); >(\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"\ 6Neqb_n_n\ 5/a\ 6) //
 411 qed.
 412
 413 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.
 414 #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))
 415 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/
 416 qed.
 417
 418 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.
 419 #N #x #y #z #H1 #H2 normalize >(\ 5a href="cic:/matita/cr/lambda/p_eqb4.def(4)"\ 6p_eqb4\ 5/a\ 6 … H1)
 420 normalize >(\ 5a href="cic:/matita/cr/lambda/p_eqb4.def(4)"\ 6p_eqb4\ 5/a\ 6 … H2) %
 421 qed.
 422
 423 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.
 424 #N #u #v #x normalize
 425 @(\ 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
 426 [normalize >\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"\ 6Neqb_n_n\ 5/a\ 6 normalize
 427  @(\ 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
 428  [>(\ 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) %
 429  |>(\ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"\ 6p_eqb1\ 5/a\ 6 … H1) %
 430  ]
 431 |@(\ 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
 432  [>\ 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) %
 433  |>H1 >H2 %
 434  ]
 435 ]
 436 qed.
 437
 438 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).
 439 #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
 440 [@(\ 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
 441  [#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/
 442  |@(\ 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
 443   [>(\ 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/
 444   |#H4 cases (\ 5a href="cic:/matita/cr/lambda/p_eqb2.fix(0,0,3)"\ 6p_eqb2\ 5/a\ 6 ??? H3) #H5 cases (H5 ?) //
 445   ]
 446  ]
 447 |@(\ 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
 448  [@(\ 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
 449   [>H4 in H1; #H1 >H1 in H3;#H3 destruct (H3)
 450   |>H4 in H3; >\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"\ 6Neqb_n_n\ 5/a\ 6 #H5 destruct (H5)
 451   ]
 452  |@(\ 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
 453   [@(\ 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
 454    [>(\ 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/
 455    |>H5 in H2; >\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"\ 6Neqb_n_n\ 5/a\ 6 #H2 destruct (H2)
 456    ]
 457   |cases (y \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 v) normalize #H4
 458    [>H4 in H1; >\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"\ 6Neqb_n_n\ 5/a\ 6 #H1 destruct (H1)
 459    |//
 460    ]
 461   ]
 462  ]
 463 ]
 464 qed.
 465
 466 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).
 467 #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
 468   [%[@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/
 469   |@(\ 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
 470     [%[@v]
 471      >(\ 5a href="cic:/matita/cr/lambda/p_eqb4.def(4)"\ 6p_eqb4\ 5/a\ 6 ? v u)
 472        [>\ 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/
 473        |% #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/
 474        ]
 475     |%[@z]
 476      >H1 >H2 %
 477     ]
 478   ]
 479 qed.
 480
 481 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.
 482 #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])]
 483 #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/
 484 qed.
 485
 486 definition pi_swap : ∀N,u,v.\ 5a href="cic:/matita/cr/lambda/fp.ind(1,0,1)"\ 6fp\ 5/a\ 6 N ≝
 487 λ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).
 488
 489 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.
 490 #N #u #v #x %
 491 qed.
 492
 493 (* lemma subst_fp :
 494   ∀s,c,x.(x ∈ GV s → x = c) → subst_X s c (Par x) = (pi_swap ? c x)·s.
 495 intros 3;elim s 0;simplify;intros
 496 [rewrite < eq_swap_pi;apply (bool_elim ? (c ≟ c1));simplify;intro
 497  [rewrite > (p_eqb1 ??? H1);autobatch
 498  |apply (bool_elim ? (x ≟ c1));intro
 499   [elim (p_eqb2 ??? H1);rewrite < H
 500    [autobatch
 501    |rewrite > (p_eqb1 ??? H2);autobatch]
 502   |rewrite > swap_other;autobatch]]
 503 |reflexivity
 504 |rewrite > H
 505  [rewrite > H1
 506   [reflexivity
 507   |intro;apply H2;autobatch]
 508  |intro;apply H2;autobatch]
 509 |rewrite > H
 510  [reflexivity
 511  |assumption]]
 512 qed. *)
 513
 514 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.
 515 #M #x elim M normalize
 516 [#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/
 517 |*:/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/]
 518 qed.
 519
 520 lemma pre_tm_inv_Par :
 521  ∀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.
 522  ∀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.
 523 #P #x #H #M cases M
 524 [//
 525 |#n #H1 destruct (H1)
 526 |#M1 #M2 #H1 destruct (H1)
 527 |#M0 #H1 destruct (H1)
 528 ]
 529 qed.
 530
 531 lemma pre_tm_inv_Var :
 532  ∀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.
 533  ∀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.
 534 #P #n #H #M cases M
 535 [2://
 536 |#x #H1 destruct (H1)
 537 |#M1 #M2 #H1 destruct (H1)
 538 |#M0 #H1 destruct (H1)
 539 ]
 540 qed.
 541
 542 lemma pre_tm_inv_Lam :
 543  ∀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.
 544  ∀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.
 545 #P #M #H #N cases N
 546 [4://
 547 |#x #H1 destruct (H1)
 548 |#n #H1 destruct (H1)
 549 |#M1 #M2 #H1 destruct (H1)
 550 ]
 551 qed.
 552
 553 lemma pre_tm_inv_App :
 554  ∀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.
 555  ∀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)) →
 556  ∀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.
 557 #P #M1 #M2 #H #N cases N
 558 [3://
 559 |#x #H1 destruct (H1)
 560 |#n #H1 destruct (H1)
 561 |#M0 #H1 destruct (H1)
 562 ]
 563 qed.
 564
 565 interpretation "permutation of pre_tm" 'middot p M = (mapX p M).
 566
 567 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.
 568 #P #p #x #y cases y
 569 [#x0 #H1 #H2 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
 570 |#n #H1 #H2 normalize in H2; destruct (H2)
 571 |#M1 #M2 #H1 #H2 normalize in H2; destruct (H2)
 572 |#M0 #H1 #H2 normalize in H2; destruct (H2)
 573 ]
 574 qed.
 575
 576 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.
 577 #P #p #n #y cases y
 578 [#x0 #H1 #H2 normalize in H2; destruct (H2)
 579 |#n0 #H1 #H2 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
 580 |#M1 #M2 #H1 #H2 normalize in H2; destruct (H2)
 581 |#M0 #H1 #H2 normalize in H2; destruct (H2)
 582 ]
 583 qed.
 584
 585 lemma Pi_App_elim :
 586   ∀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.
 587 #P #p #M1 #M2 #y cases y
 588 [#x0 #H1 #H2 normalize in H2; destruct (H2)
 589 |#n #H1 #H2 normalize in H2; destruct (H2)
 590 |#M1 #M2 #H1 #H2 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
 591 |#M0 #H1 #H2 normalize in H2; destruct (H2)
 592 ]
 593 qed.
 594
 595 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.
 596 #P #p #M0 #y cases y
 597 [#x0 #H1 #H2 normalize in H2; destruct (H2)
 598 |#n #H1 #H2 normalize in H2; destruct (H2)
 599 |#M1 #M2 #H1 #H2 normalize in H2; destruct (H2)
 600 |#M0 #H1 #H2 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
 601 ]
 602 qed.
 603
 604 (*lemma mapX_elim :
 605   ∀P:pre_tm → Prop.∀p,x,y.(∀z.P (p·z)) → p·x = y → P y.
 606 #P #p #x #y #H1 *)
 607
 608 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.
 609 #p @\ 5a href="cic:/matita/cr/lambda/fp_pre_tm.con(0,1,0)"\ 6mk_fp_pre_tm\ 5/a\ 6
 610 [@(\ 5a href="cic:/matita/cr/lambda/mapX.fix(0,1,3)"\ 6mapX\ 5/a\ 6 p)
 611 |#x elim x
 612  [#x0 #y #H1 @(\ 5a href="cic:/matita/cr/lambda/Pi_Par_elim.def(4)"\ 6Pi_Par_elim\ 5/a\ 6 … H1)
 613   #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/
 614  |#n #y #H1 @(\ 5a href="cic:/matita/cr/lambda/Pi_Var_elim.def(4)"\ 6Pi_Var_elim\ 5/a\ 6 … H1)
 615   #z #H2 >H2 in H1; #H1 @H1
 616  |#M1 #M2 #IH1 #IH2 #y #H1 @(\ 5a href="cic:/matita/cr/lambda/Pi_App_elim.def(4)"\ 6Pi_App_elim\ 5/a\ 6 … H1)
 617   #N1 #N2 #H2 >H2 in H1; #H1 normalize in H1; destruct (H1)
 618   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/
 619  |#M0 #IH0 #y #H1 @(\ 5a href="cic:/matita/cr/lambda/Pi_Abs_elim.def(4)"\ 6Pi_Abs_elim\ 5/a\ 6 … H1)
 620   #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/
 621  ]
 622 |#z elim z
 623  [#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 %
 624  |#n0 %[@(\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"\ 6Var\ 5/a\ 6 n0)] %
 625  |#M1 #M2 * #N1 #IH1 * #N2 #IH2
 626   %[@(\ 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/
 627  |#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/
 628 ]
 629 qed.
 630
 631 lemma pi_lemma1 :
 632   ∀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).
 633 #M #P #x #pi elim M
 634 [#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
 635  [cut (pi x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 pi c);
 636   [/\ 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/
 637   |#H2 >\ 5a href="cic:/matita/cr/lambda/p_eqb3.def(4)"\ 6p_eqb3\ 5/a\ 6 // ]
 638  |cut (pi x \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 pi c)
 639   [% #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)
 640   |#H2 >\ 5a href="cic:/matita/cr/lambda/p_eqb4.def(4)"\ 6p_eqb4\ 5/a\ 6 // ]
 641  ]
 642 |*:normalize //]
 643 qed.
 644
 645 (*
 646 lemma pi_lemma2 :
 647   ∀M,P,y,pi. pi · (subst_Y M y P) = subst_Y (pi · M) y (pi · P).
 648 intros;elim M
 649 [reflexivity
 650 |simplify;apply (bool_elim ? (y ≟ c));simplify;intro;reflexivity
 651 |simplify;autobatch paramodulation
 652 |simplify;apply (bool_elim ? (y ≟ c));simplify;intro;autobatch paramodulation]
 653 qed.
 654 *)
 655
 656 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).
 657
 658 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.
 659
 660 definition body ≝ λx,M.match M with
 661  [ 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
 662  | _  ⇒ M ].
 663
 664 inductive L (F:X → S_exp → Y) : S_exp → Prop \def
 665 | LPar : ∀x:X.L F (Par x)
 666 | LApp : ∀M,N:S_exp. (L F M) → (L F N) → L F (App M N)
 667 | LAbs : ∀M:S_exp. ∀x:X. (L F M) →
 668    L F (Abs (F x M) (subst_X M x (Var (F x M)))).
 669
 670 definition apartb : X → S_exp → bool ≝
 671   λx,M.notb (mem X (N_eqb X) x (GV M)).
 672
 673 let rec E (x:X) (M:S_exp) on M : list Y ≝
 674   match M with
 675     [ Par x ⇒ []
 676     | Var _ ⇒ []
 677     | App u v ⇒ E x u @ E x v
 678     | Abs y u ⇒ match apartb x u with
 679         [ true ⇒ []
 680         | false ⇒ y :: E x u ]].
 681
 682 definition apart : X → S_exp → Prop ≝
 683   λx,M.¬ x ∈ GV M.
 684
 685 interpretation "name apartness wrt GV" 'apart x s = (apart x s).
 686
 687 lemma apartb_true_to_apart : ∀x,s.apartb x s = true → x # s.
 688 intros;intro;
 689 lapply (in_list_to_mem_true ? (N_eqb X) ??? H1)
 690 [simplify;intro;generalize in match (p_eqb2 ? x1 x1);
 691  cases (x1 ≟ x1);intro;try autobatch;
 692  elim H2;reflexivity;
 693 |unfold apartb in H;rewrite > Hletin in H;simplify in H;destruct]
 694 qed.
 695
 696 lemma apart_to_apartb_true : ∀x,s.x # s → apartb x s = true.
 697 intros;cut (¬ (mem X (N_eqb X) x (GV s)) = true)
 698 [unfold apartb;generalize in match Hcut;
 699  cases (mem X (N_eqb X) x (GV s));intro;
 700  [elim H1;reflexivity
 701  |reflexivity]
 702 |intro;apply H;autobatch]
 703 qed.
 704
 705 lemma E_fresh : ∀x,M.x # M → E x M = [].
 706 intros 2;elim M;simplify
 707 [1,2:reflexivity
 708 |rewrite > H
 709  [rewrite > H1
 710   [reflexivity
 711   |elim s1 in H2;simplify;
 712    [simplify in H2;intro;apply H2;autobatch
 713    |autobatch
 714    |simplify in H4;intro;apply H4;autobatch
 715    |simplify in H3;intro;apply H3;autobatch]]
 716  |elim s in H2;simplify;
 717    [simplify in H2;intro;apply H2;lapply (in_list_singleton_to_eq ??? H3);
 718     autobatch
 719    |autobatch
 720    |simplify in H4;intro;apply H4;autobatch
 721    |simplify in H3;intro;apply H3;autobatch]]
 722 |rewrite > H
 723  [rewrite > (apart_to_apartb_true ?? H1);simplify;reflexivity
 724  |apply H1]]
 725 qed.
 726
 727 lemma mem_false_to_not_in_list :
 728   ∀A,equ.(∀x,y.x = y → equ x y = true) →
 729   ∀x,l.mem A equ x l = false → x ∉ l.
 730 intros 5;elim l
 731 [autobatch
 732 |intro;apply (bool_elim ? (equ x a));intros
 733  [simplify in H2;rewrite > H4 in H2;simplify in H2;destruct
 734  |cases (in_list_cons_case ???? H3)
 735   [rewrite > H in H4
 736    [destruct
 737    |assumption]
 738   |apply H1;
 739    [generalize in match H2;simplify;rewrite > H4;simplify;
 740     intro;assumption
 741    |assumption]]]]
 742 qed.
 743
 744 lemma mem_append : ∀A,equ.
 745  (∀x,y. x = y → equ x y = true) →
 746  (∀x,y. equ x y = true → x = y) →
 747   ∀x,l1,l2.mem A equ x (l1@l2) = orb (mem A equ x l1) (mem A equ x l2).
 748 intros;apply (bool_elim ? (mem A equ x (l1@l2)));intro
 749 [cut (x ∈ l1@l2)
 750  [cases (in_list_append_to_or_in_list ???? Hcut)
 751   [rewrite > in_list_to_mem_true
 752    [reflexivity
 753    |intro;apply H;reflexivity
 754    |assumption]
 755   |cases (mem A equ x l1);simplify;try reflexivity;
 756    rewrite > in_list_to_mem_true
 757    [reflexivity
 758    |intro;apply H;reflexivity
 759    |assumption]]
 760  |autobatch]
 761 |lapply (mem_false_to_not_in_list ????? H2)
 762  [assumption
 763  |apply orb_elim;apply (bool_elim ? (mem A equ x l1));intro;simplify
 764   [lapply (mem_true_to_in_list ????? H3);try assumption;
 765    elim Hletin;autobatch
 766   |apply (bool_elim ? (mem A equ x l2));intro;simplify
 767    [lapply (mem_true_to_in_list ????? H4);try assumption;
 768     elim Hletin;autobatch
 769    |reflexivity]]]]
 770 qed.
 771
 772 (* lemma apartb_App_apart1 : ∀x,M,N.apartb x (App M N) = true → apartb x M = true.
 773 simplify;intros;unfold apartb;
 774 apply (bool_elim ? (mem X (N_eqb X) x (GV M)));
 775 simplify;intro
 776 [
 777
 778 cut (x ∉ GV M @ GV N)
 779 [cut (apartb x M = false → False)
 780  [generalize in match Hcut1;cases (apartb x M);simplify;intro;
 781   [reflexivity|elim H1;reflexivity]
 782  |intro;apply Hcut;
 783
 784
 785 lemma apartb_App_apart1 : ∀x,M,N.apartb x (App M N) = true → apartb x M = true.
 786
 787 lemma apartb_App_apart1 : ∀x,M,N.apartb x (App M N) = true → apartb x M = true.*)
 788
 789 axiom daemon : False.
 790
 791 lemma Ep : ∀x1,x2,M,Q.x1 ≠ x2 → x1 # Q → E x1 M = E x1 (subst_X M x2 Q).
 792 intros;elim M
 793 [simplify;cases (x2 ≟ c);simplify;autobatch
 794 |reflexivity
 795 |simplify;autobatch
 796 |whd in ⊢ (??%?);rewrite > H2;
 797  simplify in ⊢ (???%);
 798  rewrite > (? : apartb x1 s = apartb x1 (subst_X s x2 Q))
 799  [reflexivity
 800  |elim s
 801   [simplify;simplify in H2;apply (bool_elim ? (x1 ≟ c1));simplify;intro
 802    [apply (bool_elim ? (x2 ≟ c1));simplify;intro
 803     [lapply (p_eqb1 ??? H3);elim H;autobatch;
 804     |rewrite > H3;reflexivity]
 805    |apply (bool_elim ? (x2 ≟ c1));simplify;intro
 806     [autobatch
 807     |rewrite > H3;reflexivity]]
 808   |reflexivity
 809   |simplify;rewrite > mem_append
 810    [rewrite > mem_append
 811     [unfold apartb in H3;unfold apartb in H4;autobatch paramodulation
 812     |*:autobatch]
 813    |*:autobatch]
 814   |apply H3]]]
 815 qed.
 816
 817 lemma pi_Abs : ∀pi,x,M.pi · Abs x M = Abs x (pi · M).
 818 intros;reflexivity;
 819 qed.
 820
 821 lemma E_Abs : ∀x,y,v,M.y ∈ E x (Abs v M) → y ∈ v::E x M.
 822 intros 4;simplify;cases (apartb x M);simplify;intro
 823 [elim (not_in_list_nil ?? H)
 824 |assumption]
 825 qed.
 826
 827 lemma E_all_fresh : ∀x1,x2,x3,M.
 828   x3 ≠ x1 → x3 ≠ x2 → E x3 M = E x3 (subst_X M x1 (Par x2)).
 829 intros;elim M;simplify
 830 [cases (x1 ≟ c);reflexivity
 831 |reflexivity
 832 |autobatch paramodulation
 833 |rewrite > (? : apartb x3 s = apartb x3 (subst_X s x1 (Par x2)))
 834  [rewrite > H2;reflexivity
 835  |elim s
 836   [simplify;simplify in H2;apply (bool_elim ? (x1 ≟ c1));simplify;intro
 837    [lapply (p_eqb1 ??? H3);rewrite < Hletin;
 838     rewrite > p_eqb4 [|assumption]
 839     rewrite > p_eqb4 [|assumption]
 840      reflexivity
 841    |reflexivity]
 842   |reflexivity
 843   |simplify;rewrite > mem_append
 844    [rewrite > mem_append
 845     [unfold apartb in H3;unfold apartb in H4;
 846      autobatch paramodulation
 847     |*:autobatch]
 848    |*:autobatch]
 849   |apply H3]]]
 850 qed.
 851
 852 lemma E_fresh_subst_Y :
 853   ∀x1,x2,y,S.x1 ≠ x2 → E x1 S = E x1 (subst_Y S y (Par x2)).
 854 intros;elim S
 855 [reflexivity
 856 |simplify;cases (y ≟ c);simplify;reflexivity
 857 |simplify;autobatch paramodulation
 858 |simplify;apply (bool_elim ? (y ≟ c));intro;simplify
 859  [reflexivity
 860  |rewrite < H1;rewrite < (? : apartb x1 s = apartb x1 (subst_Y s y (Par x2)))
 861   [reflexivity
 862   |elim s;simplify
 863    [reflexivity
 864    |cases (y ≟ c1);simplify
 865     [rewrite > p_eqb4;autobatch
 866     |reflexivity]
 867    |rewrite > mem_append [|*:autobatch]
 868     rewrite > mem_append [|*:autobatch]
 869     unfold apartb in H3;unfold apartb in H4;
 870     autobatch paramodulation
 871    |cases (y ≟ c1); simplify
 872     [reflexivity
 873     |apply H3]]]]]
 874 qed.
 875
 876 lemma subst_X_apart : ∀x,M,N. x # M → subst_X M x N = M.
 877 intros 2;
 878 elim M
 879 [simplify;simplify in H;
 880  rewrite > p_eqb4
 881  [reflexivity
 882  |intro;apply H;autobatch]
 883 |reflexivity
 884 |simplify;rewrite > H
 885  [rewrite > H1
 886   [reflexivity
 887   |intro;apply H2;simplify;autobatch]
 888  |intro;apply H2;simplify;autobatch]
 889 |simplify;rewrite >H
 890  [reflexivity
 891  |apply H1]]
 892 qed.
 893
 894 lemma subst_Y_not_dangling : ∀y,M,N. y ∉ LV M → subst_Y M y N = M.
 895 intros 2;
 896 elim M
 897 [reflexivity
 898 |simplify;simplify in H;
 899  rewrite > p_eqb4
 900  [reflexivity
 901  |intro;apply H;autobatch]
 902 |simplify;rewrite > H
 903  [rewrite > H1
 904   [reflexivity
 905   |intro;apply H2;simplify;autobatch]
 906  |intro;apply H2;simplify;autobatch]
 907 |simplify;simplify in H1;apply (bool_elim ? (y ≟ c));simplify;intro
 908  [reflexivity
 909  |rewrite > H
 910   [reflexivity
 911   |intro;apply H1;apply in_list_filter_r;autobatch]]]
 912 qed.
 913
 914 lemma subst_X_lemma :
 915   ∀x1,x2,M,P,Q.x1 ≠ x2 → x1 # Q →
 916     subst_X (subst_X M x1 P) x2 Q = subst_X (subst_X M x2 Q) x1 (subst_X P x2 Q).
 917 intros;elim M
 918 [simplify;apply (bool_elim ? (x1 ≟ c));simplify;intro
 919  [rewrite > p_eqb4
 920   [simplify;rewrite > H2;reflexivity
 921   |intro;autobatch]
 922  |apply (bool_elim ? (x2 ≟ c));simplify;intro
 923   [rewrite > subst_X_apart;autobatch
 924   |rewrite > H2;reflexivity]]
 925 |reflexivity
 926 |*:simplify;autobatch paramodulation]
 927 qed.
 928
 929 lemma subst_cancel : ∀x,y,M.x # M → M = subst_X (subst_Y M y (Par x)) x (Var y).
 930 intros 3;elim M
 931 [simplify;simplify in H;rewrite > p_eqb4
 932  [reflexivity
 933  |intro;autobatch]
 934 |simplify;apply (bool_elim ? (y ≟ c));simplify;intro
 935  [rewrite > p_eqb3 [|reflexivity]
 936   simplify;rewrite > (p_eqb1 ??? H1);reflexivity
 937  |reflexivity]
 938 |simplify;simplify in H2;rewrite < H;
 939  [rewrite < H1
 940   [reflexivity
 941   |intro;apply H2;autobatch]
 942  |intro; apply H2;autobatch]
 943 |simplify;simplify in H1;apply (bool_elim ? (y ≟ c));
 944  simplify;intro;
 945  [rewrite > subst_X_apart
 946   [reflexivity
 947   |apply H1]
 948  |rewrite < H
 949   [reflexivity
 950   |apply H1]]]
 951 qed.
 952
 953 lemma subst_X_merge : ∀M,N,x1,x2.x2 # M →
 954   subst_X (subst_X M x1 (Par x2)) x2 N = subst_X M x1 N.
 955 intros 4;elim M
 956 [simplify;apply (bool_elim ? (x1 ≟ c));simplify;intro
 957  [rewrite > Neqb_n_n;reflexivity
 958  |rewrite > p_eqb4
 959   [reflexivity
 960   |intro;elim H;simplify;autobatch]]
 961 |reflexivity
 962 |simplify;simplify in H2;rewrite > H
 963  [rewrite > H1
 964   [reflexivity
 965   |intro;autobatch]
 966  |intro;autobatch]
 967 |simplify;rewrite > H
 968  [reflexivity
 969  |apply H1]]
 970 qed.
 971
 972 lemma subst_X_Y_commute : ∀x1,x2,y,M,N. x1 ≠ x2 → y ∉ LV N →
 973   subst_Y (subst_X M x1 N) y (Par x2) = subst_X (subst_Y M y (Par x2)) x1 N.
 974 intros;elim M
 975 [simplify;apply (bool_elim ? (x1 ≟ c));simplify;intro
 976  [rewrite > subst_Y_not_dangling;autobatch
 977  |reflexivity]
 978 |simplify;apply (bool_elim ? (y ≟ c));simplify;intro
 979  [rewrite > p_eqb4
 980   [reflexivity
 981   |assumption]
 982  |reflexivity]
 983 |simplify;autobatch paramodulation
 984 |simplify;apply (bool_elim ? (y ≟ c));simplify;intro
 985  [reflexivity
 986  |rewrite < H2;reflexivity]]
 987 qed.
 988
 989 inductive LL (F : X → S_exp → Y) : S_exp → Prop ≝
 990 | LLPar : ∀x.LL F (Par x)
 991 | LLApp : ∀M,N.LL F M → LL F N → LL F (App M N)
 992 | LLAbs : ∀x1,M.(∀x2.(x2 ∈ GV M → x2 = x1) → LL F (subst_X M x1 (Par x2))) →
 993           LL F (Abs (F x1 M) (subst_X M x1 (Var (F x1 M)))).
 994
 995 include "nat/compare.ma".
 996
 997 definition max : nat → nat → nat ≝
 998   λx,y.match leb x y with
 999   [ true ⇒ y
1000   | false ⇒ x ].
1001
1002 let rec S_len M ≝ match M with
1003 [ Par _ ⇒ O
1004 | Var _ ⇒ O
1005 | App N P ⇒ S (max (S_len N) (S_len P))
1006 | Abs x N ⇒ S (S_len N) ].
1007
1008 lemma S_len_ind :
1009   ∀P:S_exp → Prop.
1010     (∀M.(∀N.S_len N < S_len M → P N) → P M)
1011     → ∀M.P M.
1012 intros;
1013 cut (∀N.S_len N ≤ S_len M → P N)
1014 [|elim M 0;simplify;intros
1015   [1,2:apply H;intros;elim (not_le_Sn_O (S_len N1));autobatch
1016   |apply H;intros;generalize in match (trans_le ??? H4 H3);unfold max;
1017    apply (bool_elim ? (leb (S_len s) (S_len s1)));simplify;intros;autobatch
1018   |apply H;intros;apply H1;apply le_S_S_to_le;autobatch]]
1019 apply H;intros;autobatch;
1020 qed.
1021
1022 record height : Type ≝
1023 {
1024   H : X → S_exp → Y;
1025   HE : ∀M:S_exp. ∀x:X. ∀pi:Pi. (L H M) → H x M = H (pi x) (pi · M);
1026   HF : ∀M:S_exp. ∀x:X. (L H M) → H x M ∉ E x M;
1027   HP : ∀M,Q:S_exp. ∀x1,x2:X. (L H M) → (L H Q) → (x1 ≟ x2) = false →
1028             apartb x1 Q = true → (H x1 M ≟ H x1 (subst_X M x2 Q)) = true
1029 }.
1030 coercion H 2.
1031
1032 record xheight : Type ≝
1033 {
1034   XH  : X → S_exp → Y;
1035   XHE : ∀M:S_exp. ∀x:X. ∀pi:Pi. XH x M = XH (pi x) (pi · M);
1036   XHF : ∀M:S_exp. ∀x:X. XH x M ∉ E x M;
1037   XHP : ∀M,Q:S_exp. ∀x1,x2:X.(x1 ≟ x2) = false →
1038             apartb x1 Q = true → (XH x1 M ≟ XH x1 (subst_X M x2 Q)) = true
1039 }.
1040 coercion XH 2.
1041
1042 include "logic/coimplication.ma".
1043
1044 definition coincl : ∀A.list A → list A → Prop ≝  λA,l1,l2.∀x.x ∈ l1 ↔ x ∈ l2.
1045
1046 notation > "hvbox(a break ≡ b)"
1047   non associative with precedence 45
1048 for @{'equiv $a $b}.
1049
1050 notation < "hvbox(term 46 a break ≡ term 46 b)"
1051   non associative with precedence 45
1052 for @{'equiv $a $b}.
1053
1054 interpretation "list coinclusion" 'equiv x y = (coincl ? x y).
1055
1056 lemma refl_coincl : ∀A.∀l:list A.l ≡ l.
1057 intros;intro;split;intro;assumption;
1058 qed.
1059
1060 lemma filter_append : ∀A,l1,l2,p.filter A (l1@l2) p = filter A l1 p @ filter A l2 p.
1061 intros;elim l1
1062 [reflexivity
1063 |simplify;cases (p a);simplify;rewrite < H;reflexivity]
1064 qed.
1065
1066 lemma GV_subst_X_Var :
1067   ∀M,x,y. GV (subst_X M x (Var y)) ≡ filter ? (GV M) (λz.¬(x ≟ z)).
1068 intros;elim M;simplify
1069 [cases (x ≟ c);simplify;autobatch
1070 |autobatch
1071 |intro;split;intro
1072  [rewrite > filter_append;cases (in_list_append_to_or_in_list ???? H2)
1073   [cases (H x1);autobatch
1074   |cases (H1 x1);autobatch]
1075  |rewrite > filter_append in H2;cases (in_list_append_to_or_in_list ???? H2)
1076   [cases (H x1);autobatch
1077   |cases (H1 x1);autobatch]]
1078 |intro;split;intro;cases (H x1);autobatch]
1079 qed.
1080
1081 lemma swap_GV : ∀x,M. x ∈ GV M → ∀x1,x2.swap X x1 x2 x ∈ GV (pi_swap X x1 x2 · M).
1082 intros;elim M in H
1083 [simplify;simplify in H;rewrite > (in_list_singleton_to_eq ??? H);autobatch
1084 |simplify in H;elim (not_in_list_nil ?? H)
1085 |simplify in H2;simplify;cases (in_list_append_to_or_in_list ???? H2);autobatch
1086 |simplify in H1;simplify;autobatch]
1087 qed.
1088
1089 (* easy to prove, but not needed *)
1090 lemma L_swap : ∀F:xheight.∀M.L F M →
1091                ∀x1,x2.L F (pi_swap ? x1 x2 · M).
1092 intros;elim H
1093 [simplify;autobatch
1094 |simplify;autobatch
1095 |simplify;rewrite > pi_lemma1;simplify;
1096  rewrite > (?: F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s))
1097  [apply LAbs;assumption
1098  |autobatch;]]
1099 qed.
1100
1101 lemma LL_swap : ∀F:xheight.∀M.LL F M →
1102                 ∀x1,x2.LL F (pi_swap ? x1 x2 · M).
1103 intros;elim H
1104 [simplify;autobatch
1105 |simplify;autobatch
1106 |simplify;rewrite > pi_lemma1;simplify;
1107  rewrite > (?: F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s))
1108  [apply LLAbs;intros;lapply (H2 (pi_swap ? x1 x2 x))
1109   [rewrite > (?: Par x = pi_swap ? x1 x2 · (Par (pi_swap ? x1 x2 x)))
1110    [autobatch
1111    |elim daemon (*involution*)]
1112   |intro;rewrite < (swap_inv ? x1 x2 c);
1113    rewrite < eq_swap_pi;apply eq_f;rewrite > eq_swap_pi;apply H3;
1114    rewrite < (swap_inv ? x1 x2 x);autobatch]
1115  |autobatch]]
1116 qed.
1117
1118 (*lemma LL_subst_X : ∀F:xheight.∀M.LL F M →
1119                    ∀x1,x2.LL F (subst_X M x1 (Par x2)).
1120 intros 2;apply (S_len_ind ?? M);intro;cases M1;simplify;intros
1121 [cases (x1 ≟ c);simplify;autobatch
1122 |inversion H1;simplify;intros;destruct
1123 |inversion H1;simplify;intros;destruct;
1124  clear H3 H5;apply LLApp;apply H;try assumption
1125  [(* len *)elim daemon
1126  |(* len *)elim daemon]
1127 |inversion H1;simplify;intros;destruct;
1128    unfold lam in H4;clear H3;destruct;
1129    apply (bool_elim ? (x1 ≟ c1));intro
1130    [rewrite > subst_X_apart
1131     [assumption
1132     |intro;rewrite > (?: (x1 ≟ c1) = false) in H3
1133      [destruct
1134      |elim (GV_subst_X_Var s1 c1 (F c1 s1) x1);
1135       lapply (H5 H4);lapply (in_list_filter_to_p_true ???? Hletin);
1136       apply p_eqb4;intro;rewrite > H7 in Hletin1;
1137       rewrite > Neqb_n_n in Hletin1;simplify in Hletin1;destruct]]
1138    |letin c2 ≝ (N_fresh ? (x1::x2::c1::GV s1));
1139     cut (c2 ∉ (x1::x2::c1::GV s1)) as Hc2 [|apply p_fresh]
1140     clearbody c2;
1141     rewrite > (? : s1 = subst_X (subst_X s1 c1 (Par c2)) c2 (Par c1)) in ⊢ (? ? (? ? (? (? % ? ?) ? ?)))
1142     [|rewrite > subst_X_merge
1143      [autobatch
1144      |intro;apply Hc2;autobatch depth=4]]
1145     rewrite > (? : F c1 s1 = F c2 (subst_X s1 c1 (Par c2)))
1146     [|rewrite > subst_X_fp
1147      [rewrite < (swap_left ? c1 c2) in ⊢ (? ? ? (? ? % ?));
1148       rewrite > eq_swap_pi;autobatch
1149      |intro;elim Hc2;autobatch depth=4]]
1150     rewrite > subst_X_merge
1151     [|intro;apply Hc2;do 2 apply in_list_cons;generalize in match H4;
1152       elim s1 0;simplify;intros
1153       [apply (bool_elim ? (c1 ≟ c));intro;
1154        rewrite > H6 in H5;simplify in H5;
1155        lapply (in_list_singleton_to_eq ??? H5)
1156        [rewrite > Hletin;autobatch
1157        |rewrite > Hletin in H6;rewrite > Neqb_n_n in H6;destruct]
1158       |elim (not_in_list_nil ?? H5)
1159       |cases (in_list_append_to_or_in_list ???? H7)
1160        [cases (in_list_cons_case ???? (H5 H8));autobatch
1161        |cases (in_list_cons_case ???? (H6 H8));autobatch]
1162       |autobatch]]
1163     rewrite > (subst_X_lemma c2 x1 ? ??)
1164     [simplify;rewrite > (? : F c2 (subst_X s1 c1 (Par c2)) = F c2 (subst_X (subst_X s1 c1 (Par c2)) x1 (Par x2)))
1165      [|apply p_eqb1;apply XHP;
1166       [apply p_eqb4;intro;apply Hc2;autobatch
1167       |simplify;rewrite > (? : (c2 ≟ x2) = false)
1168        [reflexivity
1169        |apply p_eqb4;intro;apply Hc2;autobatch]]]
1170      apply LLAbs;
1171      intros (x3);
1172      apply H
1173      [(*len*)elim daemon
1174      |3:assumption
1175      |apply H
1176       [(*len*)elim daemon
1177       |apply H2;intro;elim Hc2;autobatch depth=4]]
1178     |intro;apply Hc2;autobatch
1179     |simplify;intro;elim Hc2;rewrite > (? : c2 = x2);autobatch]]]
1180 qed.*)
1181
1182 lemma L_to_LL : ∀M.∀F:xheight.L F M → LL F M.
1183 intros;elim H
1184 [autobatch
1185 |autobatch
1186 |apply LLAbs;intros;rewrite > subst_X_fp;autobatch]
1187 qed.
1188
1189 lemma LL_to_L : ∀M.∀F:xheight.LL F M → L F M.
1190 intros;elim H
1191 [1,2:autobatch
1192 |apply LAbs;lapply (H2 c)
1193  [rewrite > subst_X_x_x in Hletin;assumption
1194  |intro;reflexivity]]
1195 qed.
1196
1197 lemma subst_X_decompose :
1198   ∀x,y,M,N.y ∉ LV M → y ∉ E x M →
1199     subst_X M x N = subst_Y (subst_X M x (Var y)) y N.
1200 intros 3;elim M
1201 [simplify;cases (x ≟ c);simplify;
1202  [rewrite > p_eqb3;autobatch
1203  |reflexivity]
1204 |simplify;simplify in H;
1205  rewrite > p_eqb4;
1206  [reflexivity
1207  |intro;apply H;autobatch]
1208 |simplify;rewrite < H
1209  [rewrite < H1
1210   [reflexivity
1211   |intro;apply H2;simplify;autobatch
1212   |intro;apply H3;simplify;autobatch]
1213  |intro;apply H2;simplify;autobatch
1214  |intro;apply H3;simplify;autobatch]
1215 |simplify;apply (bool_elim ? (y ≟ c));intros;
1216  [simplify;apply (bool_elim ? (apartb x s))
1217   [intro;simplify;
1218    lapply (apartb_true_to_apart ?? H4);
1219    rewrite > subst_X_apart
1220    [rewrite > subst_X_apart
1221     [reflexivity
1222     |assumption]
1223    |assumption]
1224   |intro;simplify in H2;rewrite > H4 in H2;
1225    simplify in H2;elim H2;
1226    rewrite > (p_eqb1 ??? H3);autobatch]
1227  |simplify;rewrite < H;
1228   [reflexivity
1229   |generalize in match H1;simplify;elim (LV s)
1230    [autobatch
1231    |intro;cases (in_list_cons_case ???? H6)
1232     [elim H5;simplify;rewrite < H7;rewrite > H3;simplify;autobatch
1233     |elim (H4 ? H7);intro;apply H5;simplify;cases (¬ (a ≟ c));simplify;autobatch]]
1234   |intro;apply H2;simplify;apply (bool_elim ? (apartb x s));intro
1235    [simplify;rewrite > E_fresh in H4
1236     [assumption
1237     |autobatch]
1238    |simplify;autobatch]]]]
1239 qed.
1240
1241 lemma subst_Y_decompose :
1242   ∀x,y,M,N.x # M →
1243     subst_Y M y N = subst_X (subst_Y M y (Par x)) x N.
1244 intros 3;elim M
1245 [simplify;simplify in H;rewrite > p_eqb4
1246  [reflexivity
1247  |intro;apply H;autobatch]
1248 |simplify;apply (bool_elim ? (y ≟ c));simplify;intro
1249  [rewrite > Neqb_n_n;reflexivity
1250  |reflexivity]
1251 |simplify;rewrite < H
1252  [rewrite < H1
1253   [reflexivity
1254   |intro;apply H2;simplify;autobatch]
1255  |intro;apply H2;simplify;autobatch]
1256 |simplify;simplify in H1;apply (bool_elim ? (y ≟ c));simplify;intro
1257  [simplify;rewrite > subst_X_apart
1258   [reflexivity
1259   |assumption]
1260  |rewrite < H
1261   [reflexivity
1262   |apply H1]]]
1263 qed.
1264
1265 lemma pre_height : ∀x1,x2,y,M.y ∉ E x1 M → y ∉ LV M →
1266   subst_X M x1 (Par x2) = subst_Y (subst_X M x1 (Var y)) y (Par x2).
1267 intros;apply subst_X_decompose;assumption;
1268 qed.
1269
1270 lemma HL_conv : ∀x,y,M.y ∈ E x M → M ≠ subst_Y (subst_X M x (Var y)) y (Par x).
1271 intros 3;elim M
1272 [simplify in H;elim (not_in_list_nil ?? H);
1273 |simplify in H;elim (not_in_list_nil ?? H)
1274 |simplify;intro;simplify in H2;destruct;
1275  cases (in_list_append_to_or_in_list ???? H2);autobatch
1276 |simplify;simplify in H1;
1277  cut (apartb x s = false)
1278  [rewrite > Hcut in H1;simplify in H1;apply (bool_elim ? (y ≟ c));intro
1279   [simplify;intro;cut (¬ x # s)
1280    [apply Hcut1;generalize in match H3;elim s 0;simplify;
1281     [intro;apply (bool_elim ? (x ≟ c1));simplify;intros;
1282      [destruct
1283      |autobatch]
1284     |intros;autobatch
1285     |intros;destruct;intro;cases (in_list_append_to_or_in_list ???? H3)
1286      [apply H4
1287       [demodulate all
1288       |assumption]
1289      |apply H5
1290       [demodulate all
1291       |assumption]]
1292     |intros;destruct;apply H4;demodulate all]
1293    |intro;rewrite > (apart_to_apartb_true ?? H4) in Hcut;destruct]
1294   |simplify;intro;apply H
1295    [cases (in_list_cons_case ???? H1)
1296     [rewrite > p_eqb3 in H2
1297      [destruct
1298      |assumption]
1299     |assumption]
1300    |destruct;assumption]]
1301  |generalize in match H1;cases (apartb x s);simplify;intro
1302   [elim (not_in_list_nil ?? H2)
1303   |reflexivity]]]
1304 qed.
1305
1306 let rec BV t ≝ match t with
1307   [ Par _ ⇒ []
1308   | Var _ ⇒ []
1309   | App t1 t2 ⇒ BV t1 @ BV t2
1310   | Abs y u ⇒ y::BV u ].
1311
1312 lemma E_BV : ∀x,M.E x M ⊆ BV M.
1313 intros;elim M;simplify
1314 [1,2:unfold;intros;assumption
1315 |unfold;intros;cases (in_list_append_to_or_in_list ???? H2);autobatch
1316 |cases (apartb x s);simplify
1317  [unfold;intros;elim (not_in_list_nil ?? H1)
1318  |autobatch]]
1319 qed.
1320
1321 (*
1322 let rec L_check (F:xheight) M on M ≝ match M with
1323   [ Par _ ⇒ true
1324   | Var _ ⇒ false
1325   | App N P ⇒ andb (L_check F N) (L_check F P)
1326   | Abs y N ⇒ let X ≝ (N_fresh ? (GV M)) in
1327               andb (y ≟ F X (subst_Y N y (Par X)))
1328                    (L_check F (subst_Y N y (Par X))) ].
1329 *)
1330
1331 let rec L_check_aux (F:xheight) M n on n ≝ match n with
1332 [ O   ⇒ false (* vacuous *)
1333 | S m ⇒ match M with
1334   [ Par _ ⇒ true
1335   | Var _ ⇒ false
1336   | App N P ⇒ andb (L_check_aux F N m) (L_check_aux F P m)
1337   | Abs y N ⇒ let X ≝ (N_fresh ? (GV M)) in
1338               andb (y ≟ F X (subst_Y N y (Par X)))
1339                    (L_check_aux F (subst_Y N y (Par X)) m) ]].
1340
1341 lemma L_check_aux_sound :
1342   ∀F,M,n.S_len M ≤ n → L_check_aux F M (S n) = true → L F M.
1343 intros 2;apply (S_len_ind ?? M);intro;cases M1;intros
1344 [autobatch
1345 |simplify in H2;destruct
1346 |simplify in H2;generalize in match H2;
1347  apply (andb_elim (L_check_aux F s n) (L_check_aux F s1 n));
1348  apply (bool_elim ? (L_check_aux F s n));simplify;intros
1349  [apply LApp
1350   [apply (H ?? (pred n))
1351    [simplify;(*len*)elim daemon
1352    |simplify in H1;generalize in match H1;cases n;intros
1353     [elim (not_le_Sn_O ? H5)
1354     |simplify;elim daemon (* H5 *)]
1355    |(* H3 *) elim daemon]
1356   |apply (H ?? (pred n))
1357    [simplify;(*len*) elim daemon
1358    |simplify in H1;generalize in match H1;cases n;intros
1359     [elim (not_le_Sn_O ? H5)
1360     |simplify;elim daemon (* H5 *)]
1361    |(* H4 *) elim daemon]]
1362  |destruct]
1363 |simplify in H2;generalize in match H2;clear H2;
1364  apply (andb_elim (c ≟ F (N_fresh X (GV s)) (subst_Y s c (Par (N_fresh X (GV s)))))
1365                   (L_check_aux F (subst_Y s c (Par (N_fresh X (GV s)))) n));
1366  apply (bool_elim ? (c≟F (N_fresh X (GV s)) (subst_Y s c (Par (N_fresh X (GV s))))));
1367  simplify;intros
1368  [rewrite > (p_eqb1 ??? H2);
1369   rewrite > (? : s =
1370                  subst_X
1371                    (subst_Y s c
1372                      (Par (N_fresh X (GV s))))
1373                    (N_fresh X (GV s))
1374                    (Var (F (N_fresh X (GV s)) (subst_Y s c (Par (N_fresh X (GV s)))))))
1375           in ⊢ (?? (?? %))
1376   [apply LAbs;apply (H ?? (pred n))
1377    [simplify;(*len*)elim daemon
1378    |simplify in H1;generalize in match H1;cases n;intros
1379     [elim (not_le_Sn_O ? H4)
1380     |simplify;elim daemon (* H4 *)]
1381    |rewrite > (? : S (pred n) = n)
1382     [assumption
1383     |(*arith*)elim daemon]]
1384   |rewrite < subst_Y_decompose
1385    [rewrite < (p_eqb1 ??? H2);autobatch
1386    |apply p_fresh]]
1387  |destruct]]
1388 qed.
1389
1390 lemma LV_subst_X : ∀s,x,y. LV (subst_X s x (Var y)) ⊆ y::LV s.
1391 intros 3;elim s
1392 [simplify;cases (x ≟ c);simplify;
1393  [autobatch
1394  |unfold;intros;elim (not_in_list_nil ?? H)]
1395 |simplify;unfold;intros;autobatch
1396 |simplify;unfold;intros;
1397  cases (in_list_append_to_or_in_list ???? H2)
1398  [lapply (H ? H3);autobatch
1399  |lapply (H1 ? H3);cases (in_list_cons_case ???? Hletin)
1400   [applyS in_list_head
1401   |autobatch]]
1402 |simplify;unfold;intros;
1403  lapply (in_list_filter ???? H1);
1404  lapply (H ? Hletin);
1405  cases (in_list_cons_case ???? Hletin1)
1406  [rewrite > H2;autobatch
1407  |apply in_list_cons;apply in_list_filter_r
1408   [assumption
1409   |apply (in_list_filter_to_p_true ???? H1)]]]
1410 qed.
1411
1412 lemma eq_list_nil : ∀A.∀l:list A.(∀x.x ∉ l) → l = [].
1413 intros 2;cases l;intro
1414 [reflexivity
1415 |elim (H a);autobatch]
1416 qed.
1417
1418 (* to be revised *)
1419 lemma L_to_closed : ∀F:xheight.∀M.L F M → LV M = [].
1420 intros;elim H
1421 [reflexivity
1422 |simplify;autobatch paramodulation
1423 |simplify;generalize in match H2;generalize in match (F c s);elim s
1424  [simplify;apply (bool_elim ? (c ≟ c1));simplify;intro
1425   [rewrite > p_eqb3;reflexivity
1426   |reflexivity]
1427  |simplify in H3;destruct
1428  |simplify in H5;simplify;
1429   rewrite > (? :
1430     filter Y (LV (subst_X s1 c (Var c1))@LV (subst_X s2 c (Var c1))) (λz.¬(z≟c1)) =
1431     filter Y (LV (subst_X s1 c (Var c1))) (λz.¬(z≟c1))@ filter Y (LV (subst_X s2 c (Var c1))) (λz.¬(z≟c1)))
1432   [rewrite > H3
1433    [rewrite > H4
1434     [reflexivity
1435     |generalize in match H5;cases (LV s2);simplify;
1436      [intro;reflexivity
1437      |cases (LV s1);simplify;intro;destruct]]
1438    |generalize in match H5;cases (LV s1);simplify;intro
1439     [reflexivity
1440     |destruct]]
1441   |elim (LV (subst_X s1 c (Var c1)));simplify
1442    [reflexivity
1443    |cases (a ≟ c1);simplify;rewrite > H6;reflexivity]]
1444  |simplify;apply eq_list_nil;intro;intro;
1445   lapply (in_list_filter ???? H5) as H6;
1446   lapply (in_list_filter ???? H6) as H7;
1447   lapply (in_list_filter_to_p_true ???? H5) as H8;
1448   lapply (in_list_filter_to_p_true ???? H6) as H9;
1449   lapply (LV_subst_X ???? H7);
1450   cut (LV s1 ⊆ [c1])
1451   [cases (in_list_cons_case ???? Hletin)
1452    [rewrite > (p_eqb3 ??? H10) in H8;simplify in H8;destruct
1453    |lapply (Hcut ? H10);lapply (in_list_singleton_to_eq ??? Hletin1);
1454     rewrite > (p_eqb3 ??? Hletin2) in H9;simplify in H9;destruct]
1455   |simplify in H4;generalize in match H4;elim (LV s1) 0;simplify
1456    [intro;unfold;intros;elim (not_in_list_nil ?? H11)
1457    |intros 2;apply (bool_elim ? (a ≟ c1));simplify;intros
1458     [unfold;intros;cases (in_list_cons_case ???? H13)
1459      [rewrite > H14;rewrite > (p_eqb1 ??? H10);autobatch
1460      |apply H11;autobatch]
1461     |destruct]]]]]
1462 qed.
1463
1464 lemma fresh_GV_subst_X_Var : ∀s,c,y.
1465   N_fresh X (GV (subst_X s c (Var y))) ∈ GV s →
1466     N_fresh X (GV (subst_X s c (Var y))) = c.
1467 intros;apply p_eqb1;
1468 apply (bool_elim ? (N_fresh X (GV (subst_X s c (Var y)))≟c));intro
1469 [reflexivity
1470 |lapply (p_eqb2 ??? H1);lapply (p_fresh ? (GV (subst_X s c (Var y))));
1471  lapply (GV_subst_X_Var s c y);
1472  elim Hletin1;cases (Hletin2 (N_fresh X (GV (subst_X s c (Var y)))));
1473  apply H3;apply in_list_filter_r
1474  [assumption
1475  |change in ⊢ (???%) with (¬false);apply eq_f;
1476   apply p_eqb4;intro;elim (p_eqb2 ??? H1);autobatch]]
1477 qed.
1478
1479 lemma L_check_aux_complete :
1480   ∀F:xheight.∀M.LL F M → ∀n.S_len M ≤ n → L_check_aux F M (S n) = true.
1481 intros 3;elim H
1482 [reflexivity
1483 |simplify;simplify in H5;rewrite > (? : n = S (pred n))
1484  [rewrite > H2
1485   [rewrite > H4
1486    [reflexivity
1487    |(* H5 *) elim daemon]
1488   |(* H5 *) elim daemon]
1489  |(* H5 *) elim daemon]
1490 |simplify;simplify in H3;
1491  rewrite > (? : (F c s ≟ F (N_fresh X (GV (subst_X s c (Var (F c s)))))
1492                           (subst_Y (subst_X s c (Var (F c s))) (F c s)
1493                             (Par (N_fresh X (GV (subst_X s c (Var (F c s))))))))
1494                 = true)
1495  [simplify;
1496   rewrite > (? : subst_Y (subst_X s c (Var (F c s))) (F c s)
1497                   (Par (N_fresh X (GV (subst_X s c (Var (F c s)))))) =
1498                   subst_X s c (Par (N_fresh X (GV (subst_X s c (Var (F c s)))))))
1499   [rewrite > (? : n = S (pred n))
1500    [rewrite > H2
1501     [reflexivity
1502     |autobatch
1503     |(* H3 *) elim daemon]
1504    |(* H3 *) elim daemon]
1505   |rewrite < subst_X_decompose
1506    [reflexivity
1507    |rewrite > (L_to_closed F)
1508     [autobatch
1509     |lapply (H1 c)
1510      [autobatch
1511      |intro;reflexivity]]
1512    |autobatch]]
1513  |rewrite < subst_X_decompose
1514   [rewrite > subst_X_fp
1515    [rewrite < (swap_left X c) in ⊢ (? ? (? ? ? (? ? % ?)) ?);
1516     autobatch
1517    |autobatch]
1518   |rewrite > (L_to_closed F)
1519    [autobatch
1520    |lapply (H1 c)
1521     [autobatch
1522     |intro;reflexivity]]
1523   |autobatch]]]
1524 qed.
1525
1526 inductive typ : Type ≝
1527 | TPar : X → typ
1528 | Fun  : typ → typ → typ.
1529
1530 notation "hvbox(a break ▸ b)"
1531   left associative with precedence 50
1532 for @{ 'blacktriangleright $a $b }.
1533 interpretation "STT arrow type" 'blacktriangleright a b = (Fun a b).
1534
1535 include "datatypes/constructors.ma".
1536
1537 definition DOM : list (X × typ) → list X ≝ λC.map ?? (fst ??) C.
1538
1539 inductive context : list (X × typ) → Prop ≝
1540 | ctx_nil  : context []
1541 | ctx_cons : ∀x,t,C.x ∉ DOM C → context C → context (〈x,t〉::C).
1542
1543 (* ▸ = \rtrif *)
1544 inductive typing (F:xheight): list (X × typ) → S_exp → typ → Prop ≝
1545 | t_axiom : ∀C,x,t.context C → 〈x,t〉 ∈ C → typing F C (Par x) t
1546 | t_App : ∀C,M,N,t,u.typing F C M (t ▸ u) → typing F C N t →
1547           typing F C (App M N) u
1548 | t_Lam : ∀C,x,M,t,u.x ∉ DOM C → typing F (〈x,t〉::C) M u →
1549           typing F C (Abs (F x M) (subst_X M x (Var (F x M)))) (t ▸ u).
1550
1551 inductive typing2 (F:xheight): list (X × typ) → S_exp → typ → Prop ≝
1552 | t2_axiom : ∀C,x,t.context C → 〈x,t〉 ∈ C → typing2 F C (Par x) t
1553 | t2_App : ∀C,M,N,t,u.typing2 F C M (t ▸ u) → typing2 F C N t →
1554           typing2 F C (App M N) u
1555 | t2_Lam : ∀C,x1,M,t,u.
1556           (∀x2.x2 ∉ DOM C → (x2 ∈ GV M → x2 = x1) →
1557             typing2 F (〈x2,t〉::C) (subst_X M x1 (Par x2)) u) →
1558           typing2 F C (Abs (F x1 M) (subst_X M x1 (Var (F x1 M)))) (t ▸ u).
1559
1560 notation > "C ⊢[F] M : t"
1561   non associative with precedence 30 for @{ 'typjudg F $C $M $t }.
1562 notation > "C ⊢ M : t"
1563   non associative with precedence 30 for @{ 'typjudg ? $C $M $t }.
1564 notation < "mstyle color #007f00 (hvbox(C maction (⊢) (⊢ \sub F) break M : break t))"
1565   non associative with precedence 30 for @{ 'typjudg $F $C $M $t }.
1566 interpretation "Fsub subtype judgement" 'typjudg F C M t = (typing F C M t).
1567
1568 notation > "C ⊨[F] M : t"
1569   non associative with precedence 30 for @{ 'typjudg2 F $C $M $t }.
1570 notation > "C ⊨ M : t"
1571   non associative with precedence 30 for @{ 'typjudg2 ? $C $M $t }.
1572 notation < "mstyle color #007f00 (hvbox(C maction (⊨) (⊨ \sub F) break M : break t))"
1573   non associative with precedence 30 for @{ 'typjudg2 $F $C $M $t }.
1574 interpretation "Fsub strong subtype judgement" 'typjudg2 F C M t = (typing2 F C M t).
1575
1576 lemma in_ctx_to_in_DOM : ∀x,t.∀C:list (X × typ).〈x,t〉 ∈ C → x ∈ DOM C.
1577 intros 3;elim C
1578 [elim (not_in_list_nil ?? H)
1579 |elim (in_list_cons_case ???? H1)
1580  [rewrite < H2;simplify;autobatch
1581  |cases a;simplify;autobatch]]
1582 qed.
1583
1584 lemma in_DOM_to_in_ctx : ∀x,C.x ∈ DOM C → ∃t.〈x,t〉 ∈ C.
1585 intros 2;elim C
1586 [elim (not_in_list_nil X ? H)
1587 |elim a in H1;simplify in H1;elim (in_list_cons_case ???? H1)
1588  [rewrite > H2;autobatch
1589  |cases (H H2);autobatch]]
1590 qed.
1591
1592 lemma incl_DOM : ∀l1,l2. l1 ⊆ l2 → DOM l1 ⊆ DOM l2.
1593 intros;unfold in H;unfold;intros;cases (in_DOM_to_in_ctx ?? H1);autobatch;
1594 qed.
1595
1596 lemma typing2_weakening : ∀F,C,M,t.
1597                          C ⊨[F] M : t → ∀D.context D → C ⊆ D → D ⊨[F] M : t.
1598 intros 5;elim H;try autobatch size=7;
1599 apply t2_Lam;intros;apply H2;
1600 [intro;autobatch
1601 |*:autobatch]
1602 qed.
1603
1604 definition swap_list : ∀N:Nset.N → N → list N → list N ≝
1605   λN,a,b,l.map ?? (pi_swap ? a b) l.
1606
1607 lemma in_list_swap : ∀N:Nset.∀x,l.x ∈ l → ∀a,b.swap N a b x ∈ swap_list N a b l.
1608 intros;elim H;simplify;autobatch;
1609 qed.
1610
1611 definition ctx_swap_X : X → X → list (X × typ) → list (X × typ) ≝
1612   λx1,x2,C.map ?? (λp.
1613     match p with
1614     [pair x t ⇒ 〈pi_swap ? x1 x2 x,t〉]) C.
1615
1616 lemma in_ctx_swap : ∀x,t,C.〈x,t〉 ∈ C → ∀a,b.〈swap ? a b x,t〉 ∈ ctx_swap_X a b C.
1617 intros;generalize in match H;elim C;
1618 [elim (not_in_list_nil ?? H1)
1619 |simplify;inversion H2;simplify;intros;destruct;simplify;autobatch]
1620 qed.
1621
1622 lemma ctx_swap_X_swap_list :
1623   ∀C,x1,x2.DOM (ctx_swap_X x1 x2 C) = swap_list ? x1 x2 (DOM C).
1624 intros;elim C
1625 [reflexivity
1626 |cases a;simplify;autobatch]
1627 qed.
1628
1629 lemma swap_list_inv : ∀N,x1,x2,l.swap_list N x1 x2 (swap_list N x1 x2 l) = l.
1630 intros;elim l;simplify;autobatch;
1631 qed.
1632
1633 lemma context_eqv : ∀C.context C → ∀a,b.context (ctx_swap_X a b C).
1634 intros;elim H
1635 [simplify;autobatch
1636 |simplify;apply ctx_cons
1637  [intro;apply H1;rewrite > ctx_swap_X_swap_list in H4;
1638   rewrite < (swap_inv ? a b);
1639   rewrite < (swap_list_inv ? a b);autobatch
1640  |assumption]]
1641 qed.
1642
1643 lemma typing_swap : ∀F:xheight.∀C,M,t,x1,x2.
1644   C ⊨[F] M : t → ctx_swap_X x1 x2 C ⊨[F] (pi_swap ? x1 x2)·M : t.
1645 intros;elim H
1646 [simplify;apply t2_axiom
1647  [autobatch
1648  |rewrite < eq_swap_pi;autobatch]
1649 |simplify;autobatch
1650 |simplify;rewrite > pi_lemma1;simplify;applyS t2_Lam;
1651  intros;rewrite < (swap_inv ? x1 x2 x);
1652  change in ⊢ (? ? ? (? ? ? %) ?) with (pi_swap X x1 x2 · Par (swap X x1 x2 x));
1653  rewrite < pi_lemma1;apply H2
1654  [intro;apply H3;rewrite < (swap_inv ? x1 x2 x);
1655   rewrite > ctx_swap_X_swap_list;autobatch
1656  |intro;rewrite > H4;autobatch]]
1657 qed.
1658
1659 lemma typing_to_typing2 : ∀F:xheight.∀C,M,t.C ⊢[F] M : t → C ⊨[F] M : t.
1660 intros;elim H;try autobatch;
1661 apply t2_Lam;intros;
1662 rewrite > subst_X_fp
1663 [rewrite > (? : 〈x2,t1〉::l = ctx_swap_X c x2 (〈c,t1〉::l))
1664  [autobatch
1665  |simplify;rewrite < eq_swap_pi;rewrite > swap_left;
1666   rewrite < (? : l = ctx_swap_X c x2 l)
1667   [reflexivity
1668   |generalize in match H1;generalize in match H4;elim l 0
1669    [intros;reflexivity
1670    |intro;cases a;simplify;intros;
1671     rewrite < eq_swap_pi;rewrite > swap_other
1672     [rewrite < H6
1673      [reflexivity
1674      |*:intro;autobatch]
1675     |*:intro;autobatch]]]]
1676 |assumption]
1677 qed.
1678
1679 lemma typing2_to_typing : ∀F:xheight.∀C,M,t.C ⊨[F] M : t → C ⊢[F] M : t.
1680 intros;elim H;try autobatch;
1681 generalize in match (p_fresh ? (c::DOM l@GV s));
1682 generalize in match (N_fresh ? (c::DOM l@GV s));
1683 intros (xn f_xn);
1684 lapply (H2 xn)
1685 [rewrite > subst_X_fp in Hletin
1686  [lapply (t_Lam ??????? Hletin)
1687   [intro;apply f_xn;autobatch
1688   |rewrite < subst_X_fp in Hletin1
1689    [rewrite > subst_X_merge in Hletin1
1690     [rewrite < (? : F c s = F xn (subst_X s c (Par xn))) in Hletin1
1691      [assumption
1692      |rewrite > subst_X_fp
1693       [rewrite < (swap_left ? c xn) in ⊢ (? ? ? (? ? % ?));
1694        rewrite > eq_swap_pi;autobatch]]]]]]]
1695 intro;elim f_xn;autobatch;
1696 qed.