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\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6tl1) (hd2\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6tl2)) →
  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\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l))
  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\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l)).
  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\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l) →
 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\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l) → 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 \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6y\ 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 lemma bool_elim :
 165 ∀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.
 166 #P * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
 167 qed.
 168
 169 let rec mem (A:Type[0]) (eq: A → A → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) x (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l ≝
 170  match l with
 171   [ nil ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6
 172   | (cons a l') ⇒
 173     match eq x a with
 174      [ true ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6
 175      | false ⇒ mem A eq x l'
 176      ]
 177   ].
 178
 179 axiom mem_true_to_in_list :
 180   ∀A,equ.
 181   (∀x,y.equ 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) →
 182   ∀x,l.\ 5a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"\ 6mem\ 5/a\ 6 A equ x l \ 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 → \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x l.
 183 (* intros 5.elim l
 184   [simplify in H1;destruct H1
 185   |simplify in H2;apply (bool_elim ? (equ x a))
 186      [intro;rewrite > (H ? ? H3);apply in_list_head
 187      |intro;rewrite > H3 in H2;simplify in H2;
 188       apply in_list_cons;apply H1;assumption]]
 189 qed.*)
 190
 191 axiom in_list_to_mem_true :
 192   ∀A,equ.
 193   (∀x.equ x x \ 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) →
 194   ∀x,l.\ 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/mem.fix(0,3,1)"\ 6mem\ 5/a\ 6 A equ x l \ 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.
 195 (*intros 5.elim l
 196   [elim (not_in_list_nil ? ? H1)
 197   |elim H2
 198     [simplify;rewrite > H;reflexivity
 199     |simplify;rewrite > H4;apply (bool_elim ? (equ a1 a2));intro;reflexivity]].
 200 qed.*)
 201
 202 lemma not_in_list_to_mem_false :
 203   ∀A,equ. (∀x,y.equ 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) →
 204   ∀x,l.x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 l → \ 5a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"\ 6mem\ 5/a\ 6 A equ x l \ 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.
 205 #A #equ #H1 #x #l #H2
 206 @(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 … (\ 5a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"\ 6mem\ 5/a\ 6 A equ x l)) //
 207 #H3 cases H2 #H4 cases (H4 ?) @(\ 5a href="cic:/matita/cr/lambda/mem_true_to_in_list.dec"\ 6mem_true_to_in_list\ 5/a\ 6 … H3) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
 208 qed.
 209
 210 lemma mem_false_to_not_in_list :
 211   ∀A,equ. (∀x.equ x x \ 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) →
 212   ∀x,l.\ 5a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"\ 6mem\ 5/a\ 6 A equ x l \ 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="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 l.
 213 #A #equ #H1 #x #l #H2 % #H3
 214 >(\ 5a href="cic:/matita/cr/lambda/in_list_to_mem_true.dec"\ 6in_list_to_mem_true\ 5/a\ 6 ????? H3) in H2; /\ 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/
 215 qed.
 216
 217 (*
 218 axiom in_list_filter_to_p_true : ∀A,l,x,p.
 219 in_list A x (filter A l p) → p x = true.
 220 (* intros 4;elim l
 221   [simplify in H;elim (not_in_list_nil ? ? H)
 222   |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
 223    simplify in H1
 224      [elim (in_list_cons_case ? ? ? ? H1)
 225         [rewrite > H3;assumption
 226         |apply (H H3)]
 227      |apply (H H1)]]
 228 qed.*)
 229
 230 naxiom in_list_filter : \forall A,l,p,x.in_list A x (filter A l p) \to in_list A x l.
 231 (*intros 4;elim l
 232   [simplify in H;elim (not_in_list_nil ? ? H)
 233   |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
 234    simplify in H1
 235      [elim (in_list_cons_case ? ? ? ? H1)
 236         [rewrite > H3;apply in_list_head
 237         |apply in_list_cons;apply H;assumption]
 238      |apply in_list_cons;apply H;assumption]]
 239 qed.*)
 240
 241 naxiom in_list_filter_r : \forall A,l,p,x.
 242               in_list A x l \to p x = true \to in_list A x (filter A l p).
 243 (* intros 4;elim l
 244   [elim (not_in_list_nil ? ? H)
 245   |elim (in_list_cons_case ? ? ? ? H1)
 246      [rewrite < H3;simplify;rewrite > H2;simplify;apply in_list_head
 247      |simplify;apply (bool_elim ? (p a));intro;simplify;
 248         [apply in_list_cons;apply H;assumption
 249         |apply H;assumption]]]
 250 qed.*)
 251 *)
 252
 253 axiom incl_A_A: ∀T,A.\ 5a href="cic:/matita/cr/lambda/incl.def(1)"\ 6incl\ 5/a\ 6 T A A.
 254 (*intros.unfold incl.intros.assumption.
 255 qed.*)
 256
 257 axiom incl_append_l : ∀T,A,B.\ 5a href="cic:/matita/cr/lambda/incl.def(1)"\ 6incl\ 5/a\ 6 T A (A \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 B).
 258 (*unfold incl; intros;autobatch.
 259 qed.*)
 260
 261 axiom incl_append_r : ∀T,A,B.\ 5a href="cic:/matita/cr/lambda/incl.def(1)"\ 6incl\ 5/a\ 6 T B (A \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 B).
 262 (*unfold incl; intros;autobatch.
 263 qed.*)
 264
 265 axiom incl_cons : ∀T,A,B,x.\ 5a href="cic:/matita/cr/lambda/incl.def(1)"\ 6incl\ 5/a\ 6 T A B → \ 5a href="cic:/matita/cr/lambda/incl.def(1)"\ 6incl\ 5/a\ 6 T (x:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6A) (x:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6B).
 266 (*unfold incl; intros;elim (in_list_cons_case ? ? ? ? H1);autobatch.
 267 qed.*)
 268
 269 record Nset : Type[1] ≝
 270 {
 271   (* carrier is specified as a coercion: when an object X of type Nset is
 272      given, but something of type Type is expected, Matita will insert a
 273      hidden coercion: the user sees "X", but really means "carrier X"     *)
 274   carrier :> Type[0];
 275   N_eqb   : carrier → carrier → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6;
 276   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;
 277   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;
 278   N_fresh : \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 carrier → carrier;
 279   p_fresh : ∀l.N_fresh l \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 l
 280 }.
 281
 282 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.
 283 #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)) //
 284 #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)
 285 qed.
 286
 287 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.
 288 #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)) //
 289 #H2 cases H1 #H3 cases (H3 (\ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"\ 6p_eqb1\ 5/a\ 6 ??? H2))
 290 qed.
 291
 292 axiom X : \ 5a href="cic:/matita/cr/lambda/Nset.ind(1,0,0)"\ 6Nset\ 5/a\ 6.
 293
 294 inductive pre_tm : Type[0] ≝
 295 | Par : \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6 → pre_tm
 296 | Var : \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → pre_tm
 297 | App : pre_tm → pre_tm → pre_tm
 298 | Abs : pre_tm → pre_tm.
 299
 300 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 ≝
 301 | tml_Par : ∀n,x.tm_level n (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 x)
 302 | 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)
 303 | 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)
 304 | 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).
 305
 306 record ext_tm (l:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) : Type[0] ≝ {
 307   tm_of_etm :> \ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6;
 308   etm_level : \ 5a href="cic:/matita/cr/lambda/tm_level.ind(1,0,0)"\ 6tm_level\ 5/a\ 6 l tm_of_etm
 309 }.
 310
 311 (*
 312  * we don't want to specify "N_eqb X" or "N_eqb Y" for the equality on X or Y,
 313  * so we use a notation "a ? b" to hide the naming structure
 314  * to type ?, write \equest.
 315  *)
 316 notation > "hvbox(a break ≟ b)"
 317   non associative with precedence 40
 318 for @{ 'equiv ? $a $b }.
 319 notation < "hvbox(a break maction (≟) (≟\sub t) b)"
 320   non associative with precedence 40
 321 for @{ 'equiv $t $a $b }.
 322 interpretation "name decidable equality" 'equiv t a b = (N_eqb t a b).
 323
 324 (* valida solo se u è chiuso *)
 325 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 ≝
 326   match t with
 327   [ Par x2 ⇒ match x \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 x2 with
 328     [ true ⇒ u
 329     | false ⇒ t ]
 330   | Var _ ⇒ t
 331   | 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)
 332   | Abs t1 ⇒ \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 (subst t1 x u) ].
 333
 334 let rec nth A (xl:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) n on xl ≝
 335   match xl with
 336   [ nil ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 A
 337   | cons x0 xl0 ⇒ match n with
 338     [ O ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 A x0
 339     | S m ⇒ nth A xl0 m ] ].
 340
 341 (* it's necessary to specify Nset... unification hint? *)
 342 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 ≝
 343   match xl with
 344   [ 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
 345   | cons x0 xl0 ⇒ match x \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 x0 with
 346     [ 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
 347     | false ⇒ match posn A xl0 x with
 348       [ 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
 349       | 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) ] ] ].
 350
 351 let rec vopen t xl k on t ≝
 352   match t with
 353   [ Par _ ⇒ t
 354   | 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
 355     [ None ⇒ t
 356     | Some x ⇒ \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 x ]
 357   | 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)
 358   | 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)) ].
 359
 360 let rec vclose t xl k on t ≝
 361   match t with
 362   [ Par x0 ⇒ match \ 5a href="cic:/matita/cr/lambda/posn.fix(0,1,3)"\ 6posn\ 5/a\ 6 ? xl x0 with
 363     [ None ⇒ t
 364     | 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) ]
 365   | Var n ⇒ t
 366   | 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)
 367   | 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)) ].
 368
 369 let rec GV t ≝
 370   match t with
 371   [ Par x ⇒ \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6x\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6
 372   | Var _ ⇒ [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6
 373   | App u v ⇒ GV u \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 GV v
 374   | Abs u ⇒ GV u ].
 375
 376 (* as above, fp_perm is a coercion
 377  * but being a coercion to FunClass, a different syntax is required
 378  * I'll fix this later *)
 379 record fp (X:\ 5a href="cic:/matita/cr/lambda/Nset.ind(1,0,0)"\ 6Nset\ 5/a\ 6) : Type[0] ≝
 380 {
 381   fp_perm       :1> X → X;
 382   fp_injective  :  \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 ?? fp_perm;
 383   fp_surjective :  \ 5a href="cic:/matita/basics/relations/surjective.def(1)"\ 6surjective\ 5/a\ 6 ?? fp_perm;
 384   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
 385 }.
 386
 387 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.
 388
 389 record fp_pre_tm : Type[0] ≝
 390 {
 391   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;
 392   fppt_injective  :  \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 ?? fppt_perm;
 393   fppt_surjective :  \ 5a href="cic:/matita/basics/relations/surjective.def(1)"\ 6surjective\ 5/a\ 6 ?? fppt_perm
 394 }.
 395
 396 (*coercion fp_perm : ∀N:Nset.∀F:fp N.N → N ≝ fp_perm on _F:(fp N) to ? → ?.
 397 coercion fppt_perm : ∀F:fp_pre_tm.pre_tm → pre_tm ≝ fppt_perm on _F:fp_pre_tm to ? → ?.*)
 398
 399 (* notation "p·x" right associative with precedence 60 for @{'middot $p $x}.
 400 interpretation "apply fp" 'middot p x = (fp_perm ? p x).
 401 interpretation "apply fppt" 'middot p x = (fppt_perm p x).*)
 402
 403 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 ≝
 404   match t with
 405   [ Par x ⇒ \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 (p x)
 406   | Var _ ⇒ t
 407   | 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)
 408   | Abs u ⇒ \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 (mapX p u) ].
 409
 410 definition swap : ∀N:\ 5a href="cic:/matita/cr/lambda/Nset.ind(1,0,0)"\ 6Nset\ 5/a\ 6.N → N → N → N ≝
 411   λN,u,v,x.match (x \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 u) with
 412     [true ⇒ v
 413     |false ⇒ match (x \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 v) with
 414        [true ⇒ u
 415        |false ⇒ x]].
 416
 417 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.
 418 #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/
 419 qed.
 420
 421 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.
 422 #N #x #y whd in ⊢ (??%?); >(\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"\ 6Neqb_n_n\ 5/a\ 6) //
 423 qed.
 424
 425 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.
 426 #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))
 427 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/
 428 qed.
 429
 430 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.
 431 #N #x #y #z #H1 #H2 normalize >(\ 5a href="cic:/matita/cr/lambda/p_eqb4.def(4)"\ 6p_eqb4\ 5/a\ 6 … H1)
 432 normalize >(\ 5a href="cic:/matita/cr/lambda/p_eqb4.def(4)"\ 6p_eqb4\ 5/a\ 6 … H2) %
 433 qed.
 434
 435 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.
 436 #N #u #v #x normalize
 437 @(\ 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
 438 [normalize >\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"\ 6Neqb_n_n\ 5/a\ 6 normalize
 439  @(\ 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
 440  [>(\ 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) %
 441  |>(\ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"\ 6p_eqb1\ 5/a\ 6 … H1) %
 442  ]
 443 |@(\ 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
 444  [>\ 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) %
 445  |>H1 >H2 %
 446  ]
 447 ]
 448 qed.
 449
 450 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).
 451 #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
 452 [@(\ 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
 453  [#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/
 454  |@(\ 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
 455   [>(\ 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/
 456   |#H4 cases (\ 5a href="cic:/matita/cr/lambda/p_eqb2.fix(0,0,3)"\ 6p_eqb2\ 5/a\ 6 ??? H3) #H5 cases (H5 ?) //
 457   ]
 458  ]
 459 |@(\ 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
 460  [@(\ 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
 461   [>H4 in H1; #H1 >H1 in H3;#H3 destruct (H3)
 462   |>H4 in H3; >\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"\ 6Neqb_n_n\ 5/a\ 6 #H5 destruct (H5)
 463   ]
 464  |@(\ 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
 465   [@(\ 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
 466    [>(\ 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/
 467    |>H5 in H2; >\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"\ 6Neqb_n_n\ 5/a\ 6 #H2 destruct (H2)
 468    ]
 469   |cases (y \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 v) normalize #H4
 470    [>H4 in H1; >\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"\ 6Neqb_n_n\ 5/a\ 6 #H1 destruct (H1)
 471    |//
 472    ]
 473   ]
 474  ]
 475 ]
 476 qed.
 477
 478 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).
 479 #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
 480   [%[@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/
 481   |@(\ 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
 482     [%[@v]
 483      >(\ 5a href="cic:/matita/cr/lambda/p_eqb4.def(4)"\ 6p_eqb4\ 5/a\ 6 ? v u)
 484        [>\ 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/
 485        |% #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/
 486        ]
 487     |%[@z]
 488      >H1 >H2 %
 489     ]
 490   ]
 491 qed.
 492
 493 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.
 494 #N #u #v %[@ \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6u;v\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6]
 495 #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/
 496 qed.
 497
 498 definition pi_swap : ∀N,u,v.\ 5a href="cic:/matita/cr/lambda/fp.ind(1,0,1)"\ 6fp\ 5/a\ 6 N ≝
 499 λ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).
 500
 501 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.
 502 #N #u #v #x %
 503 qed.
 504
 505 (* lemma subst_fp :
 506   ∀s,c,x.(x ∈ GV s → x = c) → subst_X s c (Par x) = (pi_swap ? c x)·s.
 507 intros 3;elim s 0;simplify;intros
 508 [rewrite < eq_swap_pi;apply (bool_elim ? (c ≟ c1));simplify;intro
 509  [rewrite > (p_eqb1 ??? H1);autobatch
 510  |apply (bool_elim ? (x ≟ c1));intro
 511   [elim (p_eqb2 ??? H1);rewrite < H
 512    [autobatch
 513    |rewrite > (p_eqb1 ??? H2);autobatch]
 514   |rewrite > swap_other;autobatch]]
 515 |reflexivity
 516 |rewrite > H
 517  [rewrite > H1
 518   [reflexivity
 519   |intro;apply H2;autobatch]
 520  |intro;apply H2;autobatch]
 521 |rewrite > H
 522  [reflexivity
 523  |assumption]]
 524 qed. *)
 525
 526 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.
 527 #M #x elim M normalize
 528 [#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/
 529 |*:/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/]
 530 qed.
 531
 532 lemma pre_tm_inv_Par :
 533  ∀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.
 534  ∀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.
 535 #P #x #H #M cases M
 536 [//
 537 |#n #H1 destruct (H1)
 538 |#M1 #M2 #H1 destruct (H1)
 539 |#M0 #H1 destruct (H1)
 540 ]
 541 qed.
 542
 543 lemma pre_tm_inv_Var :
 544  ∀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.
 545  ∀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.
 546 #P #n #H #M cases M
 547 [2://
 548 |#x #H1 destruct (H1)
 549 |#M1 #M2 #H1 destruct (H1)
 550 |#M0 #H1 destruct (H1)
 551 ]
 552 qed.
 553
 554 lemma pre_tm_inv_Lam :
 555  ∀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.
 556  ∀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.
 557 #P #M #H #N cases N
 558 [4://
 559 |#x #H1 destruct (H1)
 560 |#n #H1 destruct (H1)
 561 |#M1 #M2 #H1 destruct (H1)
 562 ]
 563 qed.
 564
 565 lemma pre_tm_inv_App :
 566  ∀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.
 567  ∀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)) →
 568  ∀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.
 569 #P #M1 #M2 #H #N cases N
 570 [3://
 571 |#x #H1 destruct (H1)
 572 |#n #H1 destruct (H1)
 573 |#M0 #H1 destruct (H1)
 574 ]
 575 qed.
 576
 577 interpretation "permutation of pre_tm" 'middot p M = (mapX p M).
 578
 579 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.
 580 #P #p #x #y cases y
 581 [#x0 #H1 #H2 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
 582 |#n #H1 #H2 normalize in H2; destruct (H2)
 583 |#M1 #M2 #H1 #H2 normalize in H2; destruct (H2)
 584 |#M0 #H1 #H2 normalize in H2; destruct (H2)
 585 ]
 586 qed.
 587
 588 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.
 589 #P #p #n #y cases y
 590 [#x0 #H1 #H2 normalize in H2; destruct (H2)
 591 |#n0 #H1 #H2 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
 592 |#M1 #M2 #H1 #H2 normalize in H2; destruct (H2)
 593 |#M0 #H1 #H2 normalize in H2; destruct (H2)
 594 ]
 595 qed.
 596
 597 lemma Pi_App_elim :
 598   ∀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.
 599 #P #p #M1 #M2 #y cases y
 600 [#x0 #H1 #H2 normalize in H2; destruct (H2)
 601 |#n #H1 #H2 normalize in H2; destruct (H2)
 602 |#M1 #M2 #H1 #H2 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
 603 |#M0 #H1 #H2 normalize in H2; destruct (H2)
 604 ]
 605 qed.
 606
 607 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.
 608 #P #p #M0 #y cases y
 609 [#x0 #H1 #H2 normalize in H2; destruct (H2)
 610 |#n #H1 #H2 normalize in H2; destruct (H2)
 611 |#M1 #M2 #H1 #H2 normalize in H2; destruct (H2)
 612 |#M0 #H1 #H2 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
 613 ]
 614 qed.
 615
 616 (*lemma mapX_elim :
 617   ∀P:pre_tm → Prop.∀p,x,y.(∀z.P (p·z)) → p·x = y → P y.
 618 #P #p #x #y #H1 *)
 619
 620 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.
 621 #p @\ 5a href="cic:/matita/cr/lambda/fp_pre_tm.con(0,1,0)"\ 6mk_fp_pre_tm\ 5/a\ 6
 622 [@(\ 5a href="cic:/matita/cr/lambda/mapX.fix(0,1,3)"\ 6mapX\ 5/a\ 6 p)
 623 |#x elim x
 624  [#x0 #y #H1 @(\ 5a href="cic:/matita/cr/lambda/Pi_Par_elim.def(4)"\ 6Pi_Par_elim\ 5/a\ 6 … H1)
 625   #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/
 626  |#n #y #H1 @(\ 5a href="cic:/matita/cr/lambda/Pi_Var_elim.def(4)"\ 6Pi_Var_elim\ 5/a\ 6 … H1)
 627   #z #H2 >H2 in H1; #H1 @H1
 628  |#M1 #M2 #IH1 #IH2 #y #H1 @(\ 5a href="cic:/matita/cr/lambda/Pi_App_elim.def(4)"\ 6Pi_App_elim\ 5/a\ 6 … H1)
 629   #N1 #N2 #H2 >H2 in H1; #H1 normalize in H1; destruct (H1)
 630   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/
 631  |#M0 #IH0 #y #H1 @(\ 5a href="cic:/matita/cr/lambda/Pi_Abs_elim.def(4)"\ 6Pi_Abs_elim\ 5/a\ 6 … H1)
 632   #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/
 633  ]
 634 |#z elim z
 635  [#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 %
 636  |#n0 %[@(\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"\ 6Var\ 5/a\ 6 n0)] %
 637  |#M1 #M2 * #N1 #IH1 * #N2 #IH2
 638   %[@(\ 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/
 639  |#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/
 640 ]
 641 qed.
 642
 643 lemma pi_lemma1 :
 644   ∀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).
 645 #M #P #x #pi elim M
 646 [#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
 647  [cut (pi x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 pi c);
 648   [/\ 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/
 649   |#H2 >\ 5a href="cic:/matita/cr/lambda/p_eqb3.def(4)"\ 6p_eqb3\ 5/a\ 6 // ]
 650  |cut (pi x \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 pi c)
 651   [% #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)
 652   |#H2 >\ 5a href="cic:/matita/cr/lambda/p_eqb4.def(4)"\ 6p_eqb4\ 5/a\ 6 // ]
 653  ]
 654 |*:normalize //]
 655 qed.
 656
 657 (*
 658 lemma pi_lemma2 :
 659   ∀M,P,y,pi. pi · (subst_Y M y P) = subst_Y (pi · M) y (pi · P).
 660 intros;elim M
 661 [reflexivity
 662 |simplify;apply (bool_elim ? (y ≟ c));simplify;intro;reflexivity
 663 |simplify;autobatch paramodulation
 664 |simplify;apply (bool_elim ? (y ≟ c));simplify;intro;autobatch paramodulation]
 665 qed.
 666 *)
 667
 668 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 \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6x\ 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).
 669
 670 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.
 671
 672 definition body ≝ λx,M.match M with
 673  [ Abs M0 ⇒ \ 5a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"\ 6vopen\ 5/a\ 6 M0 \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6x\ 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
 674  | _  ⇒ M ].
 675
 676 inductive dupfree (A:Type[0]) : \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A → Prop ≝
 677 | df_nil  : dupfree A [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6
 678 | df_cons : ∀x,xl.x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 xl → dupfree A xl → dupfree A (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6xl).
 679
 680 record df_list (A:Type[0]) : Type[0] ≝ {
 681   list_of_dfl :> \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A;
 682   dfl_dupfree : \ 5a href="cic:/matita/cr/lambda/dupfree.ind(1,0,1)"\ 6dupfree\ 5/a\ 6 A list_of_dfl
 683 }.
 684
 685 (* ciascuno dei pre_tm utilizzati nella costruzione deve essere un ext_tm 0 *)
 686 inductive tm : \ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6 → Prop ≝
 687 | tm_Par : ∀xl:\ 5a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"\ 6df_list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.∀x.x \ 5a title="list member" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 xl → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 x))
 688 | tm_App : ∀xl:\ 5a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"\ 6df_list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.∀M1,M2:\ 5a href="cic:/matita/cr/lambda/ext_tm.ind(1,0,1)"\ 6ext_tm\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl M1) → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl M2) → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"\ 6App\ 5/a\ 6 M1 M2))
 689 | tm_Lam : ∀xl:\ 5a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"\ 6df_list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.∀x.∀M:\ 5a href="cic:/matita/cr/lambda/ext_tm.ind(1,0,1)"\ 6ext_tm\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 xl → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6xl) M) → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl (\ 5a href="cic:/matita/cr/lambda/Lam.def(5)"\ 6Lam\ 5/a\ 6 x M)).
 690
 691 (* I see no point in using cofinite quantification here *)
 692 inductive tm2 : \ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6 → Prop ≝
 693 | tm2_Par : ∀xl:\ 5a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"\ 6df_list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.∀x.x \ 5a title="list member" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 xl → tm2 (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 x))
 694 | tm2_App : ∀xl:\ 5a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"\ 6df_list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.∀M1,M2.tm2 (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl M1) → tm2 (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl M2) → tm2 (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"\ 6App\ 5/a\ 6 M1 M2))
 695 | tm2_Lam : ∀xl:\ 5a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"\ 6df_list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.∀M.(∀x.x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 xl → tm2 (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 (x:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6xl) (\ 5a href="cic:/matita/cr/lambda/body.def(3)"\ 6body\ 5/a\ 6 x (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 M)))) → tm2 (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 M)).
 696
 697 definition apartb : \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6 → \ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 ≝
 698   λx,M.\ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"\ 6mem\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"\ 6N_eqb\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6) x (\ 5a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"\ 6GV\ 5/a\ 6 M)).
 699
 700 definition apart : \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6 → \ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6 → Prop ≝
 701   λx,M.x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"\ 6GV\ 5/a\ 6 M.
 702
 703 interpretation "name apartness wrt GV" 'apart x s = (apart x s).
 704
 705 lemma apartb_true_to_apart : ∀x,s.\ 5a href="cic:/matita/cr/lambda/apartb.def(3)"\ 6apartb\ 5/a\ 6 x s \ 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="name apartness wrt GV" href="cic:/fakeuri.def(1)"\ 6#\ 5/a\ 6 s.
 706 #x #s #H1 % #H2
 707 lapply (\ 5a href="cic:/matita/cr/lambda/in_list_to_mem_true.dec"\ 6in_list_to_mem_true\ 5/a\ 6 ? (\ 5a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"\ 6N_eqb\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6) … H2) //
 708 #Hletin normalize in H1; >Hletin in H1;
 709 normalize #Hfalse destruct (Hfalse)
 710 qed.
 711
 712 lemma apart_to_apartb_true : ∀x,s.x \ 5a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"\ 6#\ 5/a\ 6 s → \ 5a href="cic:/matita/cr/lambda/apartb.def(3)"\ 6apartb\ 5/a\ 6 x s \ 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.
 713 #x #s #H1 normalize
 714 >(\ 5a href="cic:/matita/cr/lambda/not_in_list_to_mem_false.def(4)"\ 6not_in_list_to_mem_false\ 5/a\ 6 ????? H1) /\ 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/
 715 qed.
 716
 717 lemma pi_Abs : ∀pi,M.pi \ 5a title="permutation of pre_tm" 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 M \ 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 (pi \ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 M).
 718 #pi #M %
 719 qed.
 720
 721 lemma subst_apart : ∀x,M,N. x \ 5a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"\ 6#\ 5/a\ 6 M → \ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 M x N \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 M.
 722 #x #M elim M
 723 [ normalize #x0 #N #H1 >\ 5a href="cic:/matita/cr/lambda/p_eqb4.def(4)"\ 6p_eqb4\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/in_list.con(0,1,1)"\ 6in_list_head\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 724 | #n #N #H1 %
 725 | normalize #M1 #M2 #IH1 #IH2 #N #H1 >IH1 /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/incl_append_l.dec"\ 6incl_append_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ >IH2 /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/incl_append_r.dec"\ 6incl_append_r\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 726 | normalize #M0 #IH #N #H1 >IH /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
 727 ]
 728 qed.
 729
 730 lemma subst_lemma :
 731   ∀x1,x2,M,P,Q.x1 \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 x2 → x1 \ 5a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"\ 6#\ 5/a\ 6 Q →
 732     \ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 M x1 P) x2 Q \ 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 (\ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 M x2 Q) x1 (\ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 P x2 Q).
 733 #x1 #x2 #M #P #Q #H1 #H2 elim M
 734 [ #x0 normalize @(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (x1 \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 x0)) normalize #H3
 735   [ >\ 5a href="cic:/matita/cr/lambda/p_eqb4.def(4)"\ 6p_eqb4\ 5/a\ 6
 736     [ normalize >H3 normalize %
 737     | @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … H1) /\ 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/
 738     ]
 739   | @(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (x2 \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 x0)) normalize #H4 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/cr/lambda/subst_apart.def(5)"\ 6subst_apart\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 740     >H3 normalize %
 741   ]
 742 | *: // normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
 743 ]
 744 qed.
 745
 746 (* was: subst_cancel *)
 747 (* won't prove it now because it's unsure if we need a more general version,
 748    with a list xl instead of [x], and/or with a generic n instead of O *)
 749 axiom vopen_vclose_cancel : ∀x,M.x \ 5a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"\ 6#\ 5/a\ 6 M → M \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"\ 6vclose\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"\ 6vopen\ 5/a\ 6 M \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6x\ 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) \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6x\ 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.
 750 (*
 751 intros 3;elim M
 752 [simplify;simplify in H;rewrite > p_eqb4
 753  [reflexivity
 754  |intro;autobatch]
 755 |simplify;apply (bool_elim ? (y ≟ c));simplify;intro
 756  [rewrite > p_eqb3 [|reflexivity]
 757   simplify;rewrite > (p_eqb1 ??? H1);reflexivity
 758  |reflexivity]
 759 |simplify;simplify in H2;rewrite < H;
 760  [rewrite < H1
 761   [reflexivity
 762   |intro;apply H2;autobatch]
 763  |intro; apply H2;autobatch]
 764 |simplify;simplify in H1;apply (bool_elim ? (y ≟ c));
 765  simplify;intro;
 766  [rewrite > subst_X_apart
 767   [reflexivity
 768   |apply H1]
 769  |rewrite < H
 770   [reflexivity
 771   |apply H1]]]
 772 qed. *)
 773
 774 lemma subst_merge : ∀M,N,x1,x2.x2 \ 5a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"\ 6#\ 5/a\ 6 M →
 775   \ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 M x1 (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 x2)) x2 N \ 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 M x1 N.
 776 #M #N #x1 #x2 elim M
 777 [normalize #x0 @(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (x1 \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 x0)) normalize #H1
 778  [ >\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"\ 6Neqb_n_n\ 5/a\ 6 normalize //
 779  | #H2 >\ 5a href="cic:/matita/cr/lambda/p_eqb4.def(4)"\ 6p_eqb4\ 5/a\ 6 normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/in_list.con(0,1,1)"\ 6in_list_head\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 780  ]
 781 |#n #H1 %
 782 |#M1 #M2 #IH1 #IH2 normalize #H1 >IH1 /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/incl_append_l.dec"\ 6incl_append_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ >IH2 /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/incl_append_r.dec"\ 6incl_append_r\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 783 |#M0 #IH normalize #H1 >IH /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
 784 ]
 785 qed.
 786
 787 (* was: subst_X_Y_commute
 788    won't prove it now, it's not easy to understand if it's needed and in which form *)
 789 axiom subst_vopen_commute : ∀x1,x2,M,N. x1 \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 x2 →
 790   \ 5a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"\ 6vopen\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 M x1 N) \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6x2\ 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 \ 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 (\ 5a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"\ 6vopen\ 5/a\ 6 M \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6x2\ 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) x1 N.
 791
 792 axiom daemon : ∀P:Prop.P.
 793
 794 lemma GV_tm_nil : ∀I.\ 5a href="cic:/matita/cr/lambda/tm.ind(1,0,0)"\ 6tm\ 5/a\ 6 I → \ 5a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"\ 6GV\ 5/a\ 6 I \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
 795 #I #H1 elim H1 normalize
 796 [ #xl #x #Hx (* posn_in_elim *) @\ 5a href="cic:/matita/cr/lambda/daemon.dec"\ 6daemon\ 5/a\ 6
 797 | #xl #M1 #M2 #H1 #H2 #IH1 #IH2 >IH1 >IH2 %
 798 | #xl #x #M #H1 #H2 #IH1
 799   (* prove  vclose (vclose M xl n) yl |xl| = vclose M (xl@yl) n *)
 800   @\ 5a href="cic:/matita/cr/lambda/daemon.dec"\ 6daemon\ 5/a\ 6
 801 ]
 802 qed.
 803
 804 definition fp_list ≝ λ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.λxl:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.\ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 ?? pi xl.
 805 interpretation "apply fp list" 'middot pi xl = (fp_list pi xl).
 806
 807 (* is it really necessary? *)
 808 lemma pi_no_support : ∀pi,M.\ 5a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"\ 6GV\ 5/a\ 6 M \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 → pi\ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6M \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 M.
 809 #pi #M elim M
 810 [ normalize #x0 #H1 destruct (H1)
 811 | normalize //
 812 | #M1 #M2 #IH1 #IH2 normalize #H1 >IH1
 813   [ >IH2 //
 814     cases (\ 5a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"\ 6GV\ 5/a\ 6 M1) in H1; normalize //
 815     #x0 #xl0 #H1 destruct (H1)
 816   | cases (\ 5a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"\ 6GV\ 5/a\ 6 M1) in H1; //
 817     #x0 #xl0 normalize #H1 destruct (H1)
 818   ]
 819 | normalize #M0 #IH0 #H1 >IH0 //
 820 ]
 821 qed.
 822
 823 lemma posn_eqv : ∀pi,xl,x.\ 5a href="cic:/matita/cr/lambda/posn.fix(0,1,3)"\ 6posn\ 5/a\ 6 ? (pi\ 5a title="apply fp list" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6xl) (pi x) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/posn.fix(0,1,3)"\ 6posn\ 5/a\ 6 ? xl x.
 824 #pi #xl #x @\ 5a href="cic:/matita/cr/lambda/daemon.dec"\ 6daemon\ 5/a\ 6
 825 qed.
 826
 827 lemma vclose_eqv : ∀pi,M,xl,k.pi\ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6\ 5a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"\ 6vclose\ 5/a\ 6 M xl k \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"\ 6vclose\ 5/a\ 6 (pi\ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6M) (pi\ 5a title="apply fp list" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6xl) k.
 828 #pi #M #xl elim M
 829 [ #x0 #k normalize >\ 5a href="cic:/matita/cr/lambda/posn_eqv.def(4)"\ 6posn_eqv\ 5/a\ 6 cases (\ 5a href="cic:/matita/cr/lambda/posn.fix(0,1,3)"\ 6posn\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6 xl x0) normalize //
 830 | #n0 #k %
 831 | #M1 #M2 #IH1 #IH2 #k whd in ⊢ (??%%); //
 832 | #M0 #IH0 #k whd in ⊢ (??%%); //
 833 ]
 834 qed.
 835
 836 lemma tm_eqv : ∀pi,I.\ 5a href="cic:/matita/cr/lambda/tm.ind(1,0,0)"\ 6tm\ 5/a\ 6 I → pi\ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6I \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 I.
 837 #pi #I #H1 elim H1
 838 [ #xl0 #x0 #Hx0
 839
 840 theorem term_to_term2 : ∀xl,t.\ 5a href="cic:/matita/cr/lambda/tm.ind(1,0,0)"\ 6tm\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl t) → \ 5a href="cic:/matita/cr/lambda/tm2.ind(1,0,0)"\ 6tm2\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl t).
 841 #xl #t #H elim H /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/cr/lambda/tm2.con(0,1,0)"\ 6tm2_Par\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/tm2.con(0,2,0)"\ 6tm2_App\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 842 #xl0 #x0 #M #Hx #H1 #IH1 %3 #x1 #Hx1
 843 normalize in ⊢ (?(??%));
 844
 845 (*
 846
 847 1) dimostrare che GV di un term judgment (debole) è vuoto
 848 2) dimostrare che pi*T = T se GV(T) = []
 849 3) term judgment forte -> term judgment debole
 850 4) allora per 1+2 => term judgment equivariante (entrambi)
 851 5) 4) => term judgment debole
 852
 853 *)