X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fcr%2Flambda.ma;h=a5c769a38f84859eac1e38093f8d2ae530bc6247;hb=f38fd769279794d0ca73c8945eac30e8b42e59be;hp=f368613c72ff4ef57bba5c9451c14e4353b5363e;hpb=a95a1f6ca434470d5ba385557ab3de392fbbccc0;p=helm.git

diff --git a/weblib/cr/lambda.ma b/weblib/cr/lambda.ma
index f368613c7..a5c769a38 100644
--- a/weblib/cr/lambda.ma
+++ b/weblib/cr/lambda.ma
@@ -57,7 +57,7 @@ lemma list_ind2 :
   ∀T1,T2:Type[0].∀l1:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a T1.∀l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a T2.∀P:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a T1 → a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a T2 → Prop.
   a href="cic:/matita/basics/list/length.fix(0,1,1)"length/a ? l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/list/length.fix(0,1,1)"length/a ? l2 →
   (P (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a ?) (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a ?)) → 
-  (∀hd1,hd2,tl1,tl2. P tl1 tl2 → P (hd1a title="cons" href="cic:/fakeuri.def(1)":/a:tl1) (hd2a title="cons" href="cic:/fakeuri.def(1)":/a:tl2)) → 
+  (∀hd1,hd2,tl1,tl2. P tl1 tl2 → P (hd1a title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/atl1) (hd2a title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/atl2)) → 
   P l1 l2.
 #T1 #T2 #l1 #l2 #P #Hl #Pnil #Pcons
 generalize in match Hl; generalize in match l2;
@@ -92,8 +92,8 @@ lemma length_append : ∀A,l,m.a href="cic:/matita/basics/list/length.fix(0,1,1
 qed.
 
 inductive in_list (A:Type[0]): A → (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) → Prop ≝
-| in_list_head : ∀ x,l.(in_list A x (xa title="cons" href="cic:/fakeuri.def(1)":/a:l))
-| in_list_cons : ∀ x,y,l.(in_list A x l) → (in_list A x (ya title="cons" href="cic:/fakeuri.def(1)":/a:l)).
+| in_list_head : ∀ x,l.(in_list A x (xa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al))
+| in_list_cons : ∀ x,y,l.(in_list A x l) → (in_list A x (ya title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al)).
 
 definition incl : ∀A.(a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) → (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) → Prop ≝
   λA,l,m.∀x.a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x l → a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x m.
@@ -105,13 +105,13 @@ interpretation "list member" 'mem x l = (in_list ? x l).
 interpretation "list not member" 'notmem x l = (Not (in_list ? x l)).
 interpretation "list inclusion" 'subseteq l1 l2 = (incl ? l1 l2).
   
-axiom not_in_list_nil : ∀A,x.a title="logical not" href="cic:/fakeuri.def(1)"¬/a a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x a title="nil" href="cic:/fakeuri.def(1)"[/a].
+axiom not_in_list_nil : ∀A,x.a title="logical not" href="cic:/fakeuri.def(1)"¬/a a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x [a title="nil" href="cic:/fakeuri.def(1)"]/a.
 (*intros.unfold.intro.inversion H
   [intros;lapply (sym_eq ? ? ? H2);destruct Hletin
   |intros;destruct H4]
 qed.*)
 
-axiom in_list_cons_case : ∀A,x,a,l.a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) →
+axiom in_list_cons_case : ∀A,x,a,l.a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al) →
                           x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a a title="logical or" href="cic:/fakeuri.def(1)"∨/a a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x l.
 (*intros;inversion H;intros
   [destruct H2;left;reflexivity
@@ -119,13 +119,13 @@ axiom in_list_cons_case : ∀A,x,a,l.a href="cic:/matita/cr/lambda/in_list.ind(
 qed.*)
 
 axiom in_list_tail : ∀l,x,y.
-      a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a x (ya title="cons" href="cic:/fakeuri.def(1)":/a:l) → x a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a y → a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a x l.
+      a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a x (ya title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al) → x a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a y → a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a x l.
 (*intros 4;elim (in_list_cons_case ? ? ? ? H)
   [elim (H2 H1)
   |assumption]
 qed.*)
 
-axiom in_list_singleton_to_eq : ∀A,x,y.a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x (ya title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]) → x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y.
+axiom in_list_singleton_to_eq : ∀A,x,y.a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x a title="cons" href="cic:/fakeuri.def(1)"[/aya title="nil" href="cic:/fakeuri.def(1)"]/a → x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y.
 (*intros;elim (in_list_cons_case ? ? ? ? H)
   [assumption
   |elim (not_in_list_nil ? ? H1)]
@@ -161,22 +161,25 @@ lemma in_list_append_elim:
 ]
 qed.
 
+lemma bool_elim : 
+∀P:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → Prop.∀b.(b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → P a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) → (b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → P a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a) → P b.
+#P * /span class="autotactic"2span class="autotrace" trace /span/span/
+qed.
 
-(*
-let rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝
+let rec mem (A:Type[0]) (eq: A → A → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a) x (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l ≝
  match l with
-  [ nil ⇒ false
+  [ nil ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a
   | (cons a l') ⇒
     match eq x a with
-     [ true ⇒ true
+     [ true ⇒ a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a
      | false ⇒ mem A eq x l'
      ]
   ].
   
-naxiom mem_true_to_in_list :
-  \forall A,equ.
-  (\forall x,y.equ x y = true \to x = y) \to
-  \forall x,l.mem A equ x l = true \to in_list A x l.
+axiom mem_true_to_in_list :
+  ∀A,equ.
+  (∀x,y.equ x y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y) →
+  ∀x,l.a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"mem/a A equ x l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x l.
 (* intros 5.elim l
   [simplify in H1;destruct H1
   |simplify in H2;apply (bool_elim ? (equ x a))
@@ -185,10 +188,10 @@ naxiom mem_true_to_in_list :
       apply in_list_cons;apply H1;assumption]]
 qed.*)
 
-naxiom in_list_to_mem_true :
-  \forall A,equ.
-  (\forall x.equ x x = true) \to
-  \forall x,l.in_list A x l \to mem A equ x l = true.
+axiom in_list_to_mem_true :
+  ∀A,equ.
+  (∀x.equ x x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) →
+  ∀x,l.a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"in_list/a A x l → a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"mem/a A equ x l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
 (*intros 5.elim l
   [elim (not_in_list_nil ? ? H1)
   |elim H2
@@ -196,8 +199,24 @@ naxiom in_list_to_mem_true :
     |simplify;rewrite > H4;apply (bool_elim ? (equ a1 a2));intro;reflexivity]].
 qed.*)
 
-naxiom in_list_filter_to_p_true : \forall A,l,x,p.
-in_list A x (filter A l p) \to p x = true.
+lemma not_in_list_to_mem_false :
+  ∀A,equ. (∀x,y.equ x y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y) →
+  ∀x,l.x a title="list not member" href="cic:/fakeuri.def(1)"∉/a l → a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"mem/a A equ x l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a.
+#A #equ #H1 #x #l #H2
+@(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a … (a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"mem/a A equ x l)) //
+#H3 cases H2 #H4 cases (H4 ?) @(a href="cic:/matita/cr/lambda/mem_true_to_in_list.dec"mem_true_to_in_list/a … H3) /span class="autotactic"2span class="autotrace" trace /span/span/
+qed.
+
+lemma mem_false_to_not_in_list :
+  ∀A,equ. (∀x.equ x x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) →
+  ∀x,l.a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"mem/a A equ x l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → x a title="list not member" href="cic:/fakeuri.def(1)"∉/a l.
+#A #equ #H1 #x #l #H2 % #H3
+>(a href="cic:/matita/cr/lambda/in_list_to_mem_true.dec"in_list_to_mem_true/a ????? H3) in H2; /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/
+qed.
+
+(*
+axiom in_list_filter_to_p_true : ∀A,l,x,p.
+in_list A x (filter A l p) → p x = true.
 (* intros 4;elim l
   [simplify in H;elim (not_in_list_nil ? ? H)
   |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
@@ -229,26 +248,24 @@ naxiom in_list_filter_r : \forall A,l,p,x.
         [apply in_list_cons;apply H;assumption
         |apply H;assumption]]]
 qed.*)
+*)
 
-naxiom incl_A_A: ∀T,A.incl T A A.
+axiom incl_A_A: ∀T,A.a href="cic:/matita/cr/lambda/incl.def(1)"incl/a T A A.
 (*intros.unfold incl.intros.assumption.
 qed.*)
 
-naxiom incl_append_l : ∀T,A,B.incl T A (A @ B).
+axiom incl_append_l : ∀T,A,B.a href="cic:/matita/cr/lambda/incl.def(1)"incl/a T A (A a title="append" href="cic:/fakeuri.def(1)"@/a B).
 (*unfold incl; intros;autobatch.
 qed.*)
 
-naxiom incl_append_r : ∀T,A,B.incl T B (A @ B).
+axiom incl_append_r : ∀T,A,B.a href="cic:/matita/cr/lambda/incl.def(1)"incl/a T B (A a title="append" href="cic:/fakeuri.def(1)"@/a B).
 (*unfold incl; intros;autobatch.
 qed.*)
 
-naxiom incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B).
+axiom incl_cons : ∀T,A,B,x.a href="cic:/matita/cr/lambda/incl.def(1)"incl/a T A B → a href="cic:/matita/cr/lambda/incl.def(1)"incl/a T (x:a title="cons" href="cic:/fakeuri.def(1)":/aA) (x:a title="cons" href="cic:/fakeuri.def(1)":/aB).
 (*unfold incl; intros;elim (in_list_cons_case ? ? ? ? H1);autobatch.
 qed.*)
 
-*)
-
-
 record Nset : Type[1] ≝
 {
   (* carrier is specified as a coercion: when an object X of type Nset is
@@ -262,11 +279,6 @@ record Nset : Type[1] ≝
   p_fresh : ∀l.N_fresh l a title="list not member" href="cic:/fakeuri.def(1)"∉/a l
 }.
 
-lemma bool_elim : 
-∀P:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → Prop.∀b.(b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → P a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) → (b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → P a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a) → P b.
-#P * /span class="autotactic"2span class="autotrace" trace /span/span/
-qed.
-
 lemma p_eqb3 : ∀X,x,y.x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y → a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"N_eqb/a X x y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
 #X #x #y @(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"N_eqb/a X x y)) //
 #H1 cases (a href="cic:/matita/cr/lambda/p_eqb2.fix(0,0,3)"p_eqb2/a ??? H1) #H2 #H3 cases (H2 H3)
@@ -356,8 +368,8 @@ let rec vclose t xl k on t ≝
 
 let rec GV t ≝
   match t with
-  [ Par x ⇒ xa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a] 
-  | Var _ ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a]
+  [ Par x ⇒ a title="cons" href="cic:/fakeuri.def(1)"[/axa title="nil" href="cic:/fakeuri.def(1)"]/a
+  | Var _ ⇒ [a title="nil" href="cic:/fakeuri.def(1)"]/a
   | App u v ⇒ GV u a title="append" href="cic:/fakeuri.def(1)"@/a GV v
   | Abs u ⇒ GV u ].
 
@@ -479,7 +491,7 @@ lemma swap_surj : ∀N,u,v.a href="cic:/matita/basics/relations/surjective.def(
 qed.
 
 lemma swap_finite : ∀N,u,v.a title="exists" href="cic:/fakeuri.def(1)"∃/al.∀x.x a title="list not member" href="cic:/fakeuri.def(1)"∉/a l → (a href="cic:/matita/cr/lambda/swap.def(3)"swap/a N u v) x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x.
-#N #u #v %[@ (ua title="cons" href="cic:/fakeuri.def(1)":/a:va title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a])]
+#N #u #v %[@ a title="cons" href="cic:/fakeuri.def(1)"[/au;va title="nil" href="cic:/fakeuri.def(1)"]/a]
 #x #H1 @a href="cic:/matita/cr/lambda/swap_other.def(5)"swap_other/a % #H2 cases H1 #H3 @H3 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/cr/lambda/in_list.con(0,1,1)"in_list_head/a, a href="cic:/matita/cr/lambda/in_list.con(0,2,1)"in_list_cons/a/span/span/
 qed.
 
@@ -653,17 +665,17 @@ intros;elim M
 qed.
 *)
 
-definition Lam ≝ λx:a href="cic:/matita/cr/lambda/X.dec"X/a.λM:a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a.a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a (a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"vclose/a M (xa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]) a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a).
+definition Lam ≝ λx:a href="cic:/matita/cr/lambda/X.dec"X/a.λM:a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a.a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a (a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"vclose/a M a title="cons" href="cic:/fakeuri.def(1)"[/axa title="nil" href="cic:/fakeuri.def(1)"]/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a).
 
 definition Judg ≝ λG,M.a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"vclose/a M G a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a.
 
 definition body ≝ λx,M.match M with
- [ Abs M0 ⇒ a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"vopen/a M (xa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]) a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a
+ [ Abs M0 ⇒ a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"vopen/a M0 a title="cons" href="cic:/fakeuri.def(1)"[/axa title="nil" href="cic:/fakeuri.def(1)"]/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a
  | _  ⇒ M ].
 
 inductive dupfree (A:Type[0]) : a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A → Prop ≝
-| df_nil  : dupfree A a title="nil" href="cic:/fakeuri.def(1)"[/a]
-| df_cons : ∀x,xl.x a title="list not member" href="cic:/fakeuri.def(1)"∉/a xl → dupfree A xl → dupfree A (xa title="cons" href="cic:/fakeuri.def(1)":/a:xl).
+| df_nil  : dupfree A [a title="nil" href="cic:/fakeuri.def(1)"]/a
+| df_cons : ∀x,xl.x a title="list not member" href="cic:/fakeuri.def(1)"∉/a xl → dupfree A xl → dupfree A (xa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/axl).
 
 record df_list (A:Type[0]) : Type[0] ≝ {
   list_of_dfl :> a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A;
@@ -674,283 +686,68 @@ record df_list (A:Type[0]) : Type[0] ≝ {
 inductive tm : a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → Prop ≝
 | tm_Par : ∀xl:a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"df_list/a a href="cic:/matita/cr/lambda/X.dec"X/a.∀x.x a title="list member" href="cic:/fakeuri.def(1)"∈/a xl → tm (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl (a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a x))
 | tm_App : ∀xl:a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"df_list/a a href="cic:/matita/cr/lambda/X.dec"X/a.∀M1,M2:a href="cic:/matita/cr/lambda/ext_tm.ind(1,0,1)"ext_tm/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a.tm (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl M1) → tm (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl M2) → tm (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl (a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a M1 M2))
-| tm_Lam : ∀xl:a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"df_list/a a href="cic:/matita/cr/lambda/X.dec"X/a.∀x.∀M:a href="cic:/matita/cr/lambda/ext_tm.ind(1,0,1)"ext_tm/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a.x a title="list not member" href="cic:/fakeuri.def(1)"∉/a xl → tm (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a (xa title="cons" href="cic:/fakeuri.def(1)":/a:xl) M) → tm (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl (a href="cic:/matita/cr/lambda/Lam.def(5)"Lam/a x M)).
+| tm_Lam : ∀xl:a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"df_list/a a href="cic:/matita/cr/lambda/X.dec"X/a.∀x.∀M:a href="cic:/matita/cr/lambda/ext_tm.ind(1,0,1)"ext_tm/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a.x a title="list not member" href="cic:/fakeuri.def(1)"∉/a xl → tm (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a (xa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/axl) M) → tm (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl (a href="cic:/matita/cr/lambda/Lam.def(5)"Lam/a x M)).
 
-
-inductive tm2 : pre_tm → Prop ≝
-| tm2_Par : ∀xl:df_list X.∀x.x ∈ xl → tm2 (Judg xl (Par x))
-| tm2_App : ∀xl:df_list X.∀M1,M2.tm2 (Judg xl M1) → tm2 (Judg xl M2) → tm2 (Judg xl (App M1 M2))
-| tm2_Lam : ∀xl:df_list X.∀M,C.(∀x.x ∉ xl@C → tm2 (Judg (x::xl) (body x M))) → tm2 (Judg xl (Abs M)).
-
-
-
-
-inductive L (F:X → S_exp → Y) : S_exp → Prop \def
-| LPar : ∀x:X.L F (Par x)
-| LApp : ∀M,N:S_exp. (L F M) → (L F N) → L F (App M N)
-| LAbs : ∀M:S_exp. ∀x:X. (L F M) →
-   L F (Abs (F x M) (subst_X M x (Var (F x M)))).
-   
-definition apartb : X → S_exp → bool ≝
-  λx,M.notb (mem X (N_eqb X) x (GV M)).
+(* I see no point in using cofinite quantification here *)
+inductive tm2 : a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → Prop ≝
+| tm2_Par : ∀xl:a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"df_list/a a href="cic:/matita/cr/lambda/X.dec"X/a.∀x.x a title="list member" href="cic:/fakeuri.def(1)"∈/a xl → tm2 (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl (a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a x))
+| tm2_App : ∀xl:a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"df_list/a a href="cic:/matita/cr/lambda/X.dec"X/a.∀M1,M2.tm2 (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl M1) → tm2 (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl M2) → tm2 (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl (a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a M1 M2))
+| tm2_Lam : ∀xl:a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"df_list/a a href="cic:/matita/cr/lambda/X.dec"X/a.∀M.(∀x.x a title="list not member" href="cic:/fakeuri.def(1)"∉/a xl → tm2 (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a (x:a title="cons" href="cic:/fakeuri.def(1)":/axl) (a href="cic:/matita/cr/lambda/body.def(3)"body/a x (a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a M)))) → tm2 (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl (a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a M)).
    
-let rec E (x:X) (M:S_exp) on M : list Y ≝
-  match M with
-    [ Par x ⇒ []
-    | Var _ ⇒ []
-    | App u v ⇒ E x u @ E x v
-    | Abs y u ⇒ match apartb x u with
-        [ true ⇒ []
-        | false ⇒ y :: E x u ]].
-
-definition apart : X → S_exp → Prop ≝ 
-  λx,M.¬ x ∈ GV M.
+definition apartb : a href="cic:/matita/cr/lambda/X.dec"X/a → a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a ≝
+  λx,M.a href="cic:/matita/basics/bool/notb.def(1)"notb/a (a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"mem/a a href="cic:/matita/cr/lambda/X.dec"X/a (a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"N_eqb/a a href="cic:/matita/cr/lambda/X.dec"X/a) x (a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"GV/a M)).
 
-interpretation "name apartness wrt GV" 'apart x s = (apart x s). 
-
-lemma apartb_true_to_apart : ∀x,s.apartb x s = true → x # s.
-intros;intro;
-lapply (in_list_to_mem_true ? (N_eqb X) ??? H1)
-[simplify;intro;generalize in match (p_eqb2 ? x1 x1);
- cases (x1 ≟ x1);intro;try autobatch;
- elim H2;reflexivity;
-|unfold apartb in H;rewrite > Hletin in H;simplify in H;destruct]
-qed.
+definition apart : a href="cic:/matita/cr/lambda/X.dec"X/a → a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → Prop ≝ 
+  λx,M.x a title="list not member" href="cic:/fakeuri.def(1)"∉/a a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"GV/a M.
 
-lemma apart_to_apartb_true : ∀x,s.x # s → apartb x s = true.
-intros;cut (¬ (mem X (N_eqb X) x (GV s)) = true)
-[unfold apartb;generalize in match Hcut;
- cases (mem X (N_eqb X) x (GV s));intro;
- [elim H1;reflexivity
- |reflexivity]
-|intro;apply H;autobatch]
-qed.
-
-lemma E_fresh : ∀x,M.x # M → E x M = [].
-intros 2;elim M;simplify
-[1,2:reflexivity
-|rewrite > H
- [rewrite > H1
-  [reflexivity
-  |elim s1 in H2;simplify;
-   [simplify in H2;intro;apply H2;autobatch
-   |autobatch
-   |simplify in H4;intro;apply H4;autobatch
-   |simplify in H3;intro;apply H3;autobatch]]
- |elim s in H2;simplify;
-   [simplify in H2;intro;apply H2;lapply (in_list_singleton_to_eq ??? H3);
-    autobatch
-   |autobatch
-   |simplify in H4;intro;apply H4;autobatch
-   |simplify in H3;intro;apply H3;autobatch]]
-|rewrite > H
- [rewrite > (apart_to_apartb_true ?? H1);simplify;reflexivity
- |apply H1]]
-qed.
-
-lemma mem_false_to_not_in_list :
-  ∀A,equ.(∀x,y.x = y → equ x y = true) →
-  ∀x,l.mem A equ x l = false → x ∉ l.
-intros 5;elim l
-[autobatch
-|intro;apply (bool_elim ? (equ x a));intros
- [simplify in H2;rewrite > H4 in H2;simplify in H2;destruct
- |cases (in_list_cons_case ???? H3)
-  [rewrite > H in H4
-   [destruct
-   |assumption]
-  |apply H1;
-   [generalize in match H2;simplify;rewrite > H4;simplify;
-    intro;assumption
-   |assumption]]]]
-qed.
-
-lemma mem_append : ∀A,equ.
- (∀x,y. x = y → equ x y = true) → 
- (∀x,y. equ x y = true → x = y) →
-  ∀x,l1,l2.mem A equ x (l1@l2) = orb (mem A equ x l1) (mem A equ x l2).
-intros;apply (bool_elim ? (mem A equ x (l1@l2)));intro
-[cut (x ∈ l1@l2)
- [cases (in_list_append_to_or_in_list ???? Hcut)
-  [rewrite > in_list_to_mem_true
-   [reflexivity
-   |intro;apply H;reflexivity
-   |assumption]
-  |cases (mem A equ x l1);simplify;try reflexivity;
-   rewrite > in_list_to_mem_true
-   [reflexivity
-   |intro;apply H;reflexivity
-   |assumption]]
- |autobatch]
-|lapply (mem_false_to_not_in_list ????? H2)
- [assumption
- |apply orb_elim;apply (bool_elim ? (mem A equ x l1));intro;simplify
-  [lapply (mem_true_to_in_list ????? H3);try assumption;
-   elim Hletin;autobatch
-  |apply (bool_elim ? (mem A equ x l2));intro;simplify
-   [lapply (mem_true_to_in_list ????? H4);try assumption;
-    elim Hletin;autobatch
-   |reflexivity]]]]
-qed.
-   
-(* lemma apartb_App_apart1 : ∀x,M,N.apartb x (App M N) = true → apartb x M = true.
-simplify;intros;unfold apartb;
-apply (bool_elim ? (mem X (N_eqb X) x (GV M)));
-simplify;intro
-[
-
-cut (x ∉ GV M @ GV N)
-[cut (apartb x M = false → False)
- [generalize in match Hcut1;cases (apartb x M);simplify;intro;
-  [reflexivity|elim H1;reflexivity]
- |intro;apply Hcut;
-
-
-lemma apartb_App_apart1 : ∀x,M,N.apartb x (App M N) = true → apartb x M = true.
-
-lemma apartb_App_apart1 : ∀x,M,N.apartb x (App M N) = true → apartb x M = true.*)
-
-axiom daemon : False.
-
-lemma Ep : ∀x1,x2,M,Q.x1 ≠ x2 → x1 # Q → E x1 M = E x1 (subst_X M x2 Q).
-intros;elim M
-[simplify;cases (x2 ≟ c);simplify;autobatch
-|reflexivity
-|simplify;autobatch
-|whd in ⊢ (??%?);rewrite > H2;
- simplify in ⊢ (???%);
- rewrite > (? : apartb x1 s = apartb x1 (subst_X s x2 Q))
- [reflexivity
- |elim s
-  [simplify;simplify in H2;apply (bool_elim ? (x1 ≟ c1));simplify;intro
-   [apply (bool_elim ? (x2 ≟ c1));simplify;intro
-    [lapply (p_eqb1 ??? H3);elim H;autobatch;
-    |rewrite > H3;reflexivity]
-   |apply (bool_elim ? (x2 ≟ c1));simplify;intro
-    [autobatch
-    |rewrite > H3;reflexivity]]
-  |reflexivity
-  |simplify;rewrite > mem_append
-   [rewrite > mem_append
-    [unfold apartb in H3;unfold apartb in H4;autobatch paramodulation
-    |*:autobatch]
-   |*:autobatch]
-  |apply H3]]]
-qed.
+interpretation "name apartness wrt GV" 'apart x s = (apart x s). 
 
-lemma pi_Abs : ∀pi,x,M.pi · Abs x M = Abs x (pi · M).
-intros;reflexivity;
+lemma apartb_true_to_apart : ∀x,s.a href="cic:/matita/cr/lambda/apartb.def(3)"apartb/a x s a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → x a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"#/a s.
+#x #s #H1 % #H2
+lapply (a href="cic:/matita/cr/lambda/in_list_to_mem_true.dec"in_list_to_mem_true/a ? (a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"N_eqb/a a href="cic:/matita/cr/lambda/X.dec"X/a) … H2) //
+#Hletin normalize in H1; >Hletin in H1;
+normalize #Hfalse destruct (Hfalse)
 qed.
 
-lemma E_Abs : ∀x,y,v,M.y ∈ E x (Abs v M) → y ∈ v::E x M.
-intros 4;simplify;cases (apartb x M);simplify;intro
-[elim (not_in_list_nil ?? H)
-|assumption]
+lemma apart_to_apartb_true : ∀x,s.x a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"#/a s → a href="cic:/matita/cr/lambda/apartb.def(3)"apartb/a x s a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
+#x #s #H1 normalize 
+>(a href="cic:/matita/cr/lambda/not_in_list_to_mem_false.def(4)"not_in_list_to_mem_false/a ????? H1) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a/span/span/
 qed.
 
-lemma E_all_fresh : ∀x1,x2,x3,M.
-  x3 ≠ x1 → x3 ≠ x2 → E x3 M = E x3 (subst_X M x1 (Par x2)).
-intros;elim M;simplify
-[cases (x1 ≟ c);reflexivity
-|reflexivity
-|autobatch paramodulation
-|rewrite > (? : apartb x3 s = apartb x3 (subst_X s x1 (Par x2)))
- [rewrite > H2;reflexivity
- |elim s
-  [simplify;simplify in H2;apply (bool_elim ? (x1 ≟ c1));simplify;intro
-   [lapply (p_eqb1 ??? H3);rewrite < Hletin;
-    rewrite > p_eqb4 [|assumption]
-    rewrite > p_eqb4 [|assumption]
-     reflexivity
-   |reflexivity]
-  |reflexivity
-  |simplify;rewrite > mem_append
-   [rewrite > mem_append
-    [unfold apartb in H3;unfold apartb in H4;
-     autobatch paramodulation
-    |*:autobatch]
-   |*:autobatch]
-  |apply H3]]]
+lemma pi_Abs : ∀pi,M.pi a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"·/a a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a M a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"Abs/a (pi a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"·/a M).
+#pi #M %
 qed.
 
-lemma E_fresh_subst_Y :
-  ∀x1,x2,y,S.x1 ≠ x2 → E x1 S = E x1 (subst_Y S y (Par x2)).
-intros;elim S
-[reflexivity
-|simplify;cases (y ≟ c);simplify;reflexivity
-|simplify;autobatch paramodulation
-|simplify;apply (bool_elim ? (y ≟ c));intro;simplify
- [reflexivity
- |rewrite < H1;rewrite < (? : apartb x1 s = apartb x1 (subst_Y s y (Par x2)))
-  [reflexivity
-  |elim s;simplify
-   [reflexivity
-   |cases (y ≟ c1);simplify
-    [rewrite > p_eqb4;autobatch
-    |reflexivity]
-   |rewrite > mem_append [|*:autobatch]
-    rewrite > mem_append [|*:autobatch]
-    unfold apartb in H3;unfold apartb in H4;
-    autobatch paramodulation
-   |cases (y ≟ c1); simplify
-    [reflexivity
-    |apply H3]]]]]
-qed.
-
-lemma subst_X_apart : ∀x,M,N. x # M → subst_X M x N = M.
-intros 2;
-elim M
-[simplify;simplify in H;
- rewrite > p_eqb4
- [reflexivity
- |intro;apply H;autobatch]
-|reflexivity
-|simplify;rewrite > H
- [rewrite > H1
-  [reflexivity
-  |intro;apply H2;simplify;autobatch]
- |intro;apply H2;simplify;autobatch]
-|simplify;rewrite >H
- [reflexivity
- |apply H1]]
-qed.
-
-lemma subst_Y_not_dangling : ∀y,M,N. y ∉ LV M → subst_Y M y N = M.
-intros 2;
-elim M
-[reflexivity
-|simplify;simplify in H;
- rewrite > p_eqb4
- [reflexivity
- |intro;apply H;autobatch]
-|simplify;rewrite > H
- [rewrite > H1
-  [reflexivity
-  |intro;apply H2;simplify;autobatch]
- |intro;apply H2;simplify;autobatch]
-|simplify;simplify in H1;apply (bool_elim ? (y ≟ c));simplify;intro
- [reflexivity
- |rewrite > H
-  [reflexivity
-  |intro;apply H1;apply in_list_filter_r;autobatch]]]
+lemma subst_apart : ∀x,M,N. x a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"#/a M → a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a M x N a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a M.
+#x #M elim M
+[ normalize #x0 #N #H1 >a href="cic:/matita/cr/lambda/p_eqb4.def(4)"p_eqb4/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a, a href="cic:/matita/cr/lambda/in_list.con(0,1,1)"in_list_head/a/span/span/
+| #n #N #H1 %
+| normalize #M1 #M2 #IH1 #IH2 #N #H1 >IH1 /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a, a href="cic:/matita/cr/lambda/incl_append_l.dec"incl_append_l/a/span/span/ >IH2 /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a, a href="cic:/matita/cr/lambda/incl_append_r.dec"incl_append_r/a/span/span/
+| normalize #M0 #IH #N #H1 >IH /span class="autotactic"3span class="autotrace" trace /span/span/
+]
 qed.
 
-lemma subst_X_lemma : 
-  ∀x1,x2,M,P,Q.x1 ≠ x2 → x1 # Q → 
-    subst_X (subst_X M x1 P) x2 Q = subst_X (subst_X M x2 Q) x1 (subst_X P x2 Q).
-intros;elim M
-[simplify;apply (bool_elim ? (x1 ≟ c));simplify;intro
- [rewrite > p_eqb4
-  [simplify;rewrite > H2;reflexivity
-  |intro;autobatch]
- |apply (bool_elim ? (x2 ≟ c));simplify;intro
-  [rewrite > subst_X_apart;autobatch
-  |rewrite > H2;reflexivity]]
-|reflexivity
-|*:simplify;autobatch paramodulation]
+lemma subst_lemma : 
+  ∀x1,x2,M,P,Q.x1 a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a x2 → x1 a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"#/a Q → 
+    a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a (a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a M x1 P) x2 Q a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a (a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a M x2 Q) x1 (a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a P x2 Q).
+#x1 #x2 #M #P #Q #H1 #H2 elim M
+[ #x0 normalize @(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (x1 a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a x0)) normalize #H3
+  [ >a href="cic:/matita/cr/lambda/p_eqb4.def(4)"p_eqb4/a
+    [ normalize >H3 normalize %
+    | @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … H1) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"p_eqb1/a/span/span/
+    ]
+  | @(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (x2 a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a x0)) normalize #H4 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/cr/lambda/subst_apart.def(5)"subst_apart/a/span/span/
+    >H3 normalize %
+  ]
+| *: // normalize /span class="autotactic"2span class="autotrace" trace /span/span/
+]
 qed.
 
-lemma subst_cancel : ∀x,y,M.x # M → M = subst_X (subst_Y M y (Par x)) x (Var y).
+(* was: subst_cancel *)
+(* won't prove it now because it's unsure if we need a more general version,
+   with a list xl instead of [x], and/or with a generic n instead of O *)
+axiom vopen_vclose_cancel : ∀x,M.x a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"#/a M → M a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"vclose/a (a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"vopen/a M a title="cons" href="cic:/fakeuri.def(1)"[/axa title="nil" href="cic:/fakeuri.def(1)"]/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a) a title="cons" href="cic:/fakeuri.def(1)"[/axa title="nil" href="cic:/fakeuri.def(1)"]/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a.
+(*
 intros 3;elim M
 [simplify;simplify in H;rewrite > p_eqb4
  [reflexivity
@@ -972,749 +769,85 @@ intros 3;elim M
  |rewrite < H
   [reflexivity
   |apply H1]]]
-qed.
-
-lemma subst_X_merge : ∀M,N,x1,x2.x2 # M →
-  subst_X (subst_X M x1 (Par x2)) x2 N = subst_X M x1 N.
-intros 4;elim M
-[simplify;apply (bool_elim ? (x1 ≟ c));simplify;intro
- [rewrite > Neqb_n_n;reflexivity
- |rewrite > p_eqb4
-  [reflexivity
-  |intro;elim H;simplify;autobatch]]
-|reflexivity
-|simplify;simplify in H2;rewrite > H
- [rewrite > H1
-  [reflexivity
-  |intro;autobatch]
- |intro;autobatch]
-|simplify;rewrite > H
- [reflexivity
- |apply H1]]
-qed.
-
-lemma subst_X_Y_commute : ∀x1,x2,y,M,N. x1 ≠ x2 → y ∉ LV N → 
-  subst_Y (subst_X M x1 N) y (Par x2) = subst_X (subst_Y M y (Par x2)) x1 N.
-intros;elim M
-[simplify;apply (bool_elim ? (x1 ≟ c));simplify;intro
- [rewrite > subst_Y_not_dangling;autobatch
- |reflexivity]
-|simplify;apply (bool_elim ? (y ≟ c));simplify;intro
- [rewrite > p_eqb4
-  [reflexivity
-  |assumption]
- |reflexivity]
-|simplify;autobatch paramodulation
-|simplify;apply (bool_elim ? (y ≟ c));simplify;intro
- [reflexivity
- |rewrite < H2;reflexivity]]
-qed.
-
-inductive LL (F : X → S_exp → Y) : S_exp → Prop ≝ 
-| LLPar : ∀x.LL F (Par x)
-| LLApp : ∀M,N.LL F M → LL F N → LL F (App M N)
-| LLAbs : ∀x1,M.(∀x2.(x2 ∈ GV M → x2 = x1) → LL F (subst_X M x1 (Par x2))) → 
-          LL F (Abs (F x1 M) (subst_X M x1 (Var (F x1 M)))).
-
-include "nat/compare.ma".
-
-definition max : nat → nat → nat ≝
-  λx,y.match leb x y with
-  [ true ⇒ y
-  | false ⇒ x ].
-
-let rec S_len M ≝ match M with
-[ Par _ ⇒ O
-| Var _ ⇒ O
-| App N P ⇒ S (max (S_len N) (S_len P))
-| Abs x N ⇒ S (S_len N) ].
-
-lemma S_len_ind : 
-  ∀P:S_exp → Prop.
-    (∀M.(∀N.S_len N < S_len M → P N) → P M)
-    → ∀M.P M.
-intros;
-cut (∀N.S_len N ≤ S_len M → P N)
-[|elim M 0;simplify;intros
-  [1,2:apply H;intros;elim (not_le_Sn_O (S_len N1));autobatch
-  |apply H;intros;generalize in match (trans_le ??? H4 H3);unfold max;
-   apply (bool_elim ? (leb (S_len s) (S_len s1)));simplify;intros;autobatch
-  |apply H;intros;apply H1;apply le_S_S_to_le;autobatch]]
-apply H;intros;autobatch;
-qed.
-
-record height : Type ≝
-{
-  H : X → S_exp → Y;
-  HE : ∀M:S_exp. ∀x:X. ∀pi:Pi. (L H M) → H x M = H (pi x) (pi · M);
-  HF : ∀M:S_exp. ∀x:X. (L H M) → H x M ∉ E x M;
-  HP : ∀M,Q:S_exp. ∀x1,x2:X. (L H M) → (L H Q) → (x1 ≟ x2) = false → 
-            apartb x1 Q = true → (H x1 M ≟ H x1 (subst_X M x2 Q)) = true
-}.
-coercion H 2.
-
-record xheight : Type ≝
-{
-  XH  : X → S_exp → Y;
-  XHE : ∀M:S_exp. ∀x:X. ∀pi:Pi. XH x M = XH (pi x) (pi · M);
-  XHF : ∀M:S_exp. ∀x:X. XH x M ∉ E x M;
-  XHP : ∀M,Q:S_exp. ∀x1,x2:X.(x1 ≟ x2) = false → 
-            apartb x1 Q = true → (XH x1 M ≟ XH x1 (subst_X M x2 Q)) = true
-}.
-coercion XH 2.
-
-include "logic/coimplication.ma".
-
-definition coincl : ∀A.list A → list A → Prop ≝  λA,l1,l2.∀x.x ∈ l1 ↔ x ∈ l2.
-
-notation > "hvbox(a break ≡ b)"
-  non associative with precedence 45
-for @{'equiv $a $b}.
-
-notation < "hvbox(term 46 a break ≡ term 46 b)"
-  non associative with precedence 45
-for @{'equiv $a $b}.
-
-interpretation "list coinclusion" 'equiv x y = (coincl ? x y).
-
-lemma refl_coincl : ∀A.∀l:list A.l ≡ l.
-intros;intro;split;intro;assumption;
-qed.
-
-lemma filter_append : ∀A,l1,l2,p.filter A (l1@l2) p = filter A l1 p @ filter A l2 p.
-intros;elim l1
-[reflexivity
-|simplify;cases (p a);simplify;rewrite < H;reflexivity]
-qed.
+qed. *)
 
-lemma GV_subst_X_Var : 
-  ∀M,x,y. GV (subst_X M x (Var y)) ≡ filter ? (GV M) (λz.¬(x ≟ z)).
-intros;elim M;simplify
-[cases (x ≟ c);simplify;autobatch
-|autobatch
-|intro;split;intro
- [rewrite > filter_append;cases (in_list_append_to_or_in_list ???? H2)
-  [cases (H x1);autobatch
-  |cases (H1 x1);autobatch]
- |rewrite > filter_append in H2;cases (in_list_append_to_or_in_list ???? H2)
-  [cases (H x1);autobatch
-  |cases (H1 x1);autobatch]]
-|intro;split;intro;cases (H x1);autobatch]
+lemma subst_merge : ∀M,N,x1,x2.x2 a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"#/a M →
+  a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a (a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a M x1 (a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a x2)) x2 N a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a M x1 N.
+#M #N #x1 #x2 elim M
+[normalize #x0 @(a href="cic:/matita/cr/lambda/bool_elim.def(1)"bool_elim/a ? (x1 a title="name decidable equality" href="cic:/fakeuri.def(1)"≟/a x0)) normalize #H1
+ [ >a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"Neqb_n_n/a normalize //
+ | #H2 >a href="cic:/matita/cr/lambda/p_eqb4.def(4)"p_eqb4/a normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a, a href="cic:/matita/cr/lambda/in_list.con(0,1,1)"in_list_head/a/span/span/
+ ]
+|#n #H1 %
+|#M1 #M2 #IH1 #IH2 normalize #H1 >IH1 /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a, a href="cic:/matita/cr/lambda/incl_append_l.dec"incl_append_l/a/span/span/ >IH2 /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a, a href="cic:/matita/cr/lambda/incl_append_r.dec"incl_append_r/a/span/span/
+|#M0 #IH normalize #H1 >IH /span class="autotactic"3span class="autotrace" trace /span/span/
+]
 qed.
 
-lemma swap_GV : ∀x,M. x ∈ GV M → ∀x1,x2.swap X x1 x2 x ∈ GV (pi_swap X x1 x2 · M).
-intros;elim M in H
-[simplify;simplify in H;rewrite > (in_list_singleton_to_eq ??? H);autobatch
-|simplify in H;elim (not_in_list_nil ?? H)
-|simplify in H2;simplify;cases (in_list_append_to_or_in_list ???? H2);autobatch
-|simplify in H1;simplify;autobatch]
-qed.
+(* was: subst_X_Y_commute
+   won't prove it now, it's not easy to understand if it's needed and in which form *)
+axiom subst_vopen_commute : ∀x1,x2,M,N. x1 a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a x2 →
+  a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"vopen/a (a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a M x1 N) a title="cons" href="cic:/fakeuri.def(1)"[/ax2a title="nil" href="cic:/fakeuri.def(1)"]/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"subst/a (a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"vopen/a M a title="cons" href="cic:/fakeuri.def(1)"[/ax2a title="nil" href="cic:/fakeuri.def(1)"]/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a) x1 N.
 
-(* easy to prove, but not needed *)
-lemma L_swap : ∀F:xheight.∀M.L F M →
-               ∀x1,x2.L F (pi_swap ? x1 x2 · M).
-intros;elim H
-[simplify;autobatch
-|simplify;autobatch
-|simplify;rewrite > pi_lemma1;simplify;
- rewrite > (?: F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s))
- [apply LAbs;assumption
- |autobatch;]]
-qed.
+axiom daemon : ∀P:Prop.P.
 
-lemma LL_swap : ∀F:xheight.∀M.LL F M →
-                ∀x1,x2.LL F (pi_swap ? x1 x2 · M).
-intros;elim H
-[simplify;autobatch
-|simplify;autobatch
-|simplify;rewrite > pi_lemma1;simplify;
- rewrite > (?: F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s))
- [apply LLAbs;intros;lapply (H2 (pi_swap ? x1 x2 x))
-  [rewrite > (?: Par x = pi_swap ? x1 x2 · (Par (pi_swap ? x1 x2 x)))
-   [autobatch
-   |elim daemon (*involution*)]
-  |intro;rewrite < (swap_inv ? x1 x2 c);
-   rewrite < eq_swap_pi;apply eq_f;rewrite > eq_swap_pi;apply H3;
-   rewrite < (swap_inv ? x1 x2 x);autobatch]
- |autobatch]]
+lemma GV_tm_nil : ∀I.a href="cic:/matita/cr/lambda/tm.ind(1,0,0)"tm/a I → a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"GV/a I a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a [a title="nil" href="cic:/fakeuri.def(1)"]/a.
+#I #H1 elim H1 normalize
+[ #xl #x #Hx (* posn_in_elim *) @a href="cic:/matita/cr/lambda/daemon.dec"daemon/a
+| #xl #M1 #M2 #H1 #H2 #IH1 #IH2 >IH1 >IH2 %
+| #xl #x #M #H1 #H2 #IH1
+  (* prove  vclose (vclose M xl n) yl |xl| = vclose M (xl@yl) n *)
+  @a href="cic:/matita/cr/lambda/daemon.dec"daemon/a
+]
 qed.
 
-(*lemma LL_subst_X : ∀F:xheight.∀M.LL F M → 
-                   ∀x1,x2.LL F (subst_X M x1 (Par x2)).
-intros 2;apply (S_len_ind ?? M);intro;cases M1;simplify;intros
-[cases (x1 ≟ c);simplify;autobatch
-|inversion H1;simplify;intros;destruct
-|inversion H1;simplify;intros;destruct;
- clear H3 H5;apply LLApp;apply H;try assumption
- [(* len *)elim daemon
- |(* len *)elim daemon]
-|inversion H1;simplify;intros;destruct;
-   unfold lam in H4;clear H3;destruct;
-   apply (bool_elim ? (x1 ≟ c1));intro
-   [rewrite > subst_X_apart
-    [assumption
-    |intro;rewrite > (?: (x1 ≟ c1) = false) in H3
-     [destruct
-     |elim (GV_subst_X_Var s1 c1 (F c1 s1) x1);
-      lapply (H5 H4);lapply (in_list_filter_to_p_true ???? Hletin);
-      apply p_eqb4;intro;rewrite > H7 in Hletin1;
-      rewrite > Neqb_n_n in Hletin1;simplify in Hletin1;destruct]]
-   |letin c2 ≝ (N_fresh ? (x1::x2::c1::GV s1));
-    cut (c2 ∉ (x1::x2::c1::GV s1)) as Hc2 [|apply p_fresh]
-    clearbody c2;
-    rewrite > (? : s1 = subst_X (subst_X s1 c1 (Par c2)) c2 (Par c1)) in ⊢ (? ? (? ? (? (? % ? ?) ? ?)))
-    [|rewrite > subst_X_merge
-     [autobatch
-     |intro;apply Hc2;autobatch depth=4]]
-    rewrite > (? : F c1 s1 = F c2 (subst_X s1 c1 (Par c2)))
-    [|rewrite > subst_X_fp
-     [rewrite < (swap_left ? c1 c2) in ⊢ (? ? ? (? ? % ?));
-      rewrite > eq_swap_pi;autobatch
-     |intro;elim Hc2;autobatch depth=4]]
-    rewrite > subst_X_merge
-    [|intro;apply Hc2;do 2 apply in_list_cons;generalize in match H4;
-      elim s1 0;simplify;intros
-      [apply (bool_elim ? (c1 ≟ c));intro;
-       rewrite > H6 in H5;simplify in H5;
-       lapply (in_list_singleton_to_eq ??? H5)
-       [rewrite > Hletin;autobatch
-       |rewrite > Hletin in H6;rewrite > Neqb_n_n in H6;destruct]
-      |elim (not_in_list_nil ?? H5)
-      |cases (in_list_append_to_or_in_list ???? H7)
-       [cases (in_list_cons_case ???? (H5 H8));autobatch
-       |cases (in_list_cons_case ???? (H6 H8));autobatch]
-      |autobatch]]
-    rewrite > (subst_X_lemma c2 x1 ? ??)
-    [simplify;rewrite > (? : F c2 (subst_X s1 c1 (Par c2)) = F c2 (subst_X (subst_X s1 c1 (Par c2)) x1 (Par x2)))
-     [|apply p_eqb1;apply XHP;
-      [apply p_eqb4;intro;apply Hc2;autobatch
-      |simplify;rewrite > (? : (c2 ≟ x2) = false)
-       [reflexivity
-       |apply p_eqb4;intro;apply Hc2;autobatch]]]
-     apply LLAbs;
-     intros (x3);
-     apply H
-     [(*len*)elim daemon
-     |3:assumption
-     |apply H
-      [(*len*)elim daemon
-      |apply H2;intro;elim Hc2;autobatch depth=4]]
-    |intro;apply Hc2;autobatch
-    |simplify;intro;elim Hc2;rewrite > (? : c2 = x2);autobatch]]]
-qed.*)
-
-lemma L_to_LL : ∀M.∀F:xheight.L F M → LL F M.
-intros;elim H
-[autobatch
-|autobatch
-|apply LLAbs;intros;rewrite > subst_X_fp;autobatch]
+definition fp_list ≝ λpi:a href="cic:/matita/cr/lambda/fp.ind(1,0,1)"fp/a a href="cic:/matita/cr/lambda/X.dec"X/a.λxl:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a a href="cic:/matita/cr/lambda/X.dec"X/a.a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a ?? pi xl.
+interpretation "apply fp list" 'middot pi xl = (fp_list pi xl).
+
+(* is it really necessary? *)
+lemma pi_no_support : ∀pi,M.a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"GV/a M a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a [a title="nil" href="cic:/fakeuri.def(1)"]/a → pia title="permutation of pre_tm" href="cic:/fakeuri.def(1)"·/aM a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a M.
+#pi #M elim M
+[ normalize #x0 #H1 destruct (H1)
+| normalize //
+| #M1 #M2 #IH1 #IH2 normalize #H1 >IH1
+  [ >IH2 //
+    cases (a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"GV/a M1) in H1; normalize //
+    #x0 #xl0 #H1 destruct (H1)
+  | cases (a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"GV/a M1) in H1; //
+    #x0 #xl0 normalize #H1 destruct (H1)
+  ]
+| normalize #M0 #IH0 #H1 >IH0 //
+]
 qed.
 
-lemma LL_to_L : ∀M.∀F:xheight.LL F M → L F M.
-intros;elim H
-[1,2:autobatch
-|apply LAbs;lapply (H2 c)
- [rewrite > subst_X_x_x in Hletin;assumption
- |intro;reflexivity]]
+lemma posn_eqv : ∀pi,xl,x.a href="cic:/matita/cr/lambda/posn.fix(0,1,3)"posn/a ? (pia title="apply fp list" href="cic:/fakeuri.def(1)"·/axl) (pi x) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/cr/lambda/posn.fix(0,1,3)"posn/a ? xl x.
+#pi #xl #x @a href="cic:/matita/cr/lambda/daemon.dec"daemon/a
 qed.
 
-lemma subst_X_decompose : 
-  ∀x,y,M,N.y ∉ LV M → y ∉ E x M → 
-    subst_X M x N = subst_Y (subst_X M x (Var y)) y N.
-intros 3;elim M
-[simplify;cases (x ≟ c);simplify;
- [rewrite > p_eqb3;autobatch
- |reflexivity]
-|simplify;simplify in H;
- rewrite > p_eqb4;
- [reflexivity
- |intro;apply H;autobatch]
-|simplify;rewrite < H
- [rewrite < H1
-  [reflexivity
-  |intro;apply H2;simplify;autobatch
-  |intro;apply H3;simplify;autobatch]
- |intro;apply H2;simplify;autobatch
- |intro;apply H3;simplify;autobatch]
-|simplify;apply (bool_elim ? (y ≟ c));intros;
- [simplify;apply (bool_elim ? (apartb x s))
-  [intro;simplify;
-   lapply (apartb_true_to_apart ?? H4);
-   rewrite > subst_X_apart
-   [rewrite > subst_X_apart
-    [reflexivity
-    |assumption]
-   |assumption]
-  |intro;simplify in H2;rewrite > H4 in H2;
-   simplify in H2;elim H2;
-   rewrite > (p_eqb1 ??? H3);autobatch]
- |simplify;rewrite < H;
-  [reflexivity
-  |generalize in match H1;simplify;elim (LV s)
-   [autobatch
-   |intro;cases (in_list_cons_case ???? H6)
-    [elim H5;simplify;rewrite < H7;rewrite > H3;simplify;autobatch
-    |elim (H4 ? H7);intro;apply H5;simplify;cases (¬ (a ≟ c));simplify;autobatch]]
-  |intro;apply H2;simplify;apply (bool_elim ? (apartb x s));intro
-   [simplify;rewrite > E_fresh in H4
-    [assumption
-    |autobatch]
-   |simplify;autobatch]]]]
+lemma vclose_eqv : ∀pi,M,xl,k.pia title="permutation of pre_tm" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"vclose/a M xl k a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"vclose/a (pia title="permutation of pre_tm" href="cic:/fakeuri.def(1)"·/aM) (pia title="apply fp list" href="cic:/fakeuri.def(1)"·/axl) k.
+#pi #M #xl elim M 
+[ #x0 #k normalize >a href="cic:/matita/cr/lambda/posn_eqv.def(4)"posn_eqv/a cases (a href="cic:/matita/cr/lambda/posn.fix(0,1,3)"posn/a a href="cic:/matita/cr/lambda/X.dec"X/a xl x0) normalize //
+| #n0 #k %
+| #M1 #M2 #IH1 #IH2 #k whd in ⊢ (??%%); //
+| #M0 #IH0 #k whd in ⊢ (??%%); //
+]
 qed.
 
-lemma subst_Y_decompose : 
-  ∀x,y,M,N.x # M → 
-    subst_Y M y N = subst_X (subst_Y M y (Par x)) x N.
-intros 3;elim M
-[simplify;simplify in H;rewrite > p_eqb4
- [reflexivity
- |intro;apply H;autobatch]
-|simplify;apply (bool_elim ? (y ≟ c));simplify;intro
- [rewrite > Neqb_n_n;reflexivity
- |reflexivity]
-|simplify;rewrite < H
- [rewrite < H1
-  [reflexivity
-  |intro;apply H2;simplify;autobatch]
- |intro;apply H2;simplify;autobatch]
-|simplify;simplify in H1;apply (bool_elim ? (y ≟ c));simplify;intro
- [simplify;rewrite > subst_X_apart
-  [reflexivity
-  |assumption]
- |rewrite < H
-  [reflexivity
-  |apply H1]]]
-qed.
+lemma tm_eqv : ∀pi,I.a href="cic:/matita/cr/lambda/tm.ind(1,0,0)"tm/a I → pia title="permutation of pre_tm" href="cic:/fakeuri.def(1)"·/aI a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a I.
+#pi #I #H1 elim H1
+[ #xl0 #x0 #Hx0
 
-lemma pre_height : ∀x1,x2,y,M.y ∉ E x1 M → y ∉ LV M → 
-  subst_X M x1 (Par x2) = subst_Y (subst_X M x1 (Var y)) y (Par x2).
-intros;apply subst_X_decompose;assumption;
-qed.
+theorem term_to_term2 : ∀xl,t.a href="cic:/matita/cr/lambda/tm.ind(1,0,0)"tm/a (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl t) → a href="cic:/matita/cr/lambda/tm2.ind(1,0,0)"tm2/a (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl t).
+#xl #t #H elim H /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/cr/lambda/tm2.con(0,1,0)"tm2_Par/a, a href="cic:/matita/cr/lambda/tm2.con(0,2,0)"tm2_App/a/span/span/
+#xl0 #x0 #M #Hx #H1 #IH1 %3 #x1 #Hx1
+normalize in ⊢ (?(??%));
 
-lemma HL_conv : ∀x,y,M.y ∈ E x M → M ≠ subst_Y (subst_X M x (Var y)) y (Par x).
-intros 3;elim M
-[simplify in H;elim (not_in_list_nil ?? H);
-|simplify in H;elim (not_in_list_nil ?? H)
-|simplify;intro;simplify in H2;destruct;
- cases (in_list_append_to_or_in_list ???? H2);autobatch
-|simplify;simplify in H1;
- cut (apartb x s = false)
- [rewrite > Hcut in H1;simplify in H1;apply (bool_elim ? (y ≟ c));intro
-  [simplify;intro;cut (¬ x # s)
-   [apply Hcut1;generalize in match H3;elim s 0;simplify;
-    [intro;apply (bool_elim ? (x ≟ c1));simplify;intros;
-     [destruct
-     |autobatch]
-    |intros;autobatch
-    |intros;destruct;intro;cases (in_list_append_to_or_in_list ???? H3)
-     [apply H4
-      [demodulate all
-      |assumption]
-     |apply H5
-      [demodulate all
-      |assumption]]
-    |intros;destruct;apply H4;demodulate all]
-   |intro;rewrite > (apart_to_apartb_true ?? H4) in Hcut;destruct]
-  |simplify;intro;apply H
-   [cases (in_list_cons_case ???? H1)
-    [rewrite > p_eqb3 in H2
-     [destruct
-     |assumption]
-    |assumption]
-   |destruct;assumption]]
- |generalize in match H1;cases (apartb x s);simplify;intro
-  [elim (not_in_list_nil ?? H2)
-  |reflexivity]]]
-qed.
-
-let rec BV t ≝ match t with
-  [ Par _ ⇒ []
-  | Var _ ⇒ []
-  | App t1 t2 ⇒ BV t1 @ BV t2
-  | Abs y u ⇒ y::BV u ].
-
-lemma E_BV : ∀x,M.E x M ⊆ BV M.
-intros;elim M;simplify
-[1,2:unfold;intros;assumption
-|unfold;intros;cases (in_list_append_to_or_in_list ???? H2);autobatch
-|cases (apartb x s);simplify
- [unfold;intros;elim (not_in_list_nil ?? H1)
- |autobatch]]
-qed.
-     
 (*
-let rec L_check (F:xheight) M on M ≝ match M with
-  [ Par _ ⇒ true
-  | Var _ ⇒ false
-  | App N P ⇒ andb (L_check F N) (L_check F P)
-  | Abs y N ⇒ let X ≝ (N_fresh ? (GV M)) in 
-              andb (y ≟ F X (subst_Y N y (Par X)))
-                   (L_check F (subst_Y N y (Par X))) ]. 
-*)
-
-let rec L_check_aux (F:xheight) M n on n ≝ match n with
-[ O   ⇒ false (* vacuous *)
-| S m ⇒ match M with
-  [ Par _ ⇒ true
-  | Var _ ⇒ false
-  | App N P ⇒ andb (L_check_aux F N m) (L_check_aux F P m)
-  | Abs y N ⇒ let X ≝ (N_fresh ? (GV M)) in 
-              andb (y ≟ F X (subst_Y N y (Par X)))
-                   (L_check_aux F (subst_Y N y (Par X)) m) ]].
-
-lemma L_check_aux_sound : 
-  ∀F,M,n.S_len M ≤ n → L_check_aux F M (S n) = true → L F M.
-intros 2;apply (S_len_ind ?? M);intro;cases M1;intros
-[autobatch
-|simplify in H2;destruct
-|simplify in H2;generalize in match H2;
- apply (andb_elim (L_check_aux F s n) (L_check_aux F s1 n));
- apply (bool_elim ? (L_check_aux F s n));simplify;intros
- [apply LApp
-  [apply (H ?? (pred n))
-   [simplify;(*len*)elim daemon
-   |simplify in H1;generalize in match H1;cases n;intros
-    [elim (not_le_Sn_O ? H5)
-    |simplify;elim daemon (* H5 *)]
-   |(* H3 *) elim daemon]
-  |apply (H ?? (pred n))
-   [simplify;(*len*) elim daemon
-   |simplify in H1;generalize in match H1;cases n;intros
-    [elim (not_le_Sn_O ? H5)
-    |simplify;elim daemon (* H5 *)]
-   |(* H4 *) elim daemon]]
- |destruct]
-|simplify in H2;generalize in match H2;clear H2;
- apply (andb_elim (c ≟ F (N_fresh X (GV s)) (subst_Y s c (Par (N_fresh X (GV s))))) 
-                  (L_check_aux F (subst_Y s c (Par (N_fresh X (GV s)))) n));
- apply (bool_elim ? (c≟F (N_fresh X (GV s)) (subst_Y s c (Par (N_fresh X (GV s))))));
- simplify;intros
- [rewrite > (p_eqb1 ??? H2);
-  rewrite > (? : s = 
-                 subst_X 
-                   (subst_Y s c
-                     (Par (N_fresh X (GV s))))
-                   (N_fresh X (GV s))
-                   (Var (F (N_fresh X (GV s)) (subst_Y s c (Par (N_fresh X (GV s)))))))
-          in ⊢ (?? (?? %))
-  [apply LAbs;apply (H ?? (pred n))
-   [simplify;(*len*)elim daemon
-   |simplify in H1;generalize in match H1;cases n;intros
-    [elim (not_le_Sn_O ? H4)
-    |simplify;elim daemon (* H4 *)]
-   |rewrite > (? : S (pred n) = n)
-    [assumption
-    |(*arith*)elim daemon]]
-  |rewrite < subst_Y_decompose
-   [rewrite < (p_eqb1 ??? H2);autobatch
-   |apply p_fresh]]
- |destruct]]
-qed.
-
-lemma LV_subst_X : ∀s,x,y. LV (subst_X s x (Var y)) ⊆ y::LV s.
-intros 3;elim s
-[simplify;cases (x ≟ c);simplify;
- [autobatch
- |unfold;intros;elim (not_in_list_nil ?? H)]
-|simplify;unfold;intros;autobatch
-|simplify;unfold;intros;
- cases (in_list_append_to_or_in_list ???? H2)
- [lapply (H ? H3);autobatch
- |lapply (H1 ? H3);cases (in_list_cons_case ???? Hletin)
-  [applyS in_list_head
-  |autobatch]]
-|simplify;unfold;intros;
- lapply (in_list_filter ???? H1);
- lapply (H ? Hletin);
- cases (in_list_cons_case ???? Hletin1)
- [rewrite > H2;autobatch
- |apply in_list_cons;apply in_list_filter_r
-  [assumption
-  |apply (in_list_filter_to_p_true ???? H1)]]]
-qed.
-
-lemma eq_list_nil : ∀A.∀l:list A.(∀x.x ∉ l) → l = [].
-intros 2;cases l;intro
-[reflexivity
-|elim (H a);autobatch]
-qed.
-
-(* to be revised *)
-lemma L_to_closed : ∀F:xheight.∀M.L F M → LV M = [].
-intros;elim H
-[reflexivity
-|simplify;autobatch paramodulation
-|simplify;generalize in match H2;generalize in match (F c s);elim s
- [simplify;apply (bool_elim ? (c ≟ c1));simplify;intro
-  [rewrite > p_eqb3;reflexivity
-  |reflexivity]
- |simplify in H3;destruct
- |simplify in H5;simplify;
-  rewrite > (? : 
-    filter Y (LV (subst_X s1 c (Var c1))@LV (subst_X s2 c (Var c1))) (λz.¬(z≟c1)) =
-    filter Y (LV (subst_X s1 c (Var c1))) (λz.¬(z≟c1))@ filter Y (LV (subst_X s2 c (Var c1))) (λz.¬(z≟c1)))
-  [rewrite > H3
-   [rewrite > H4
-    [reflexivity
-    |generalize in match H5;cases (LV s2);simplify;
-     [intro;reflexivity
-     |cases (LV s1);simplify;intro;destruct]]
-   |generalize in match H5;cases (LV s1);simplify;intro
-    [reflexivity
-    |destruct]]
-  |elim (LV (subst_X s1 c (Var c1)));simplify
-   [reflexivity
-   |cases (a ≟ c1);simplify;rewrite > H6;reflexivity]]
- |simplify;apply eq_list_nil;intro;intro;
-  lapply (in_list_filter ???? H5) as H6;
-  lapply (in_list_filter ???? H6) as H7;
-  lapply (in_list_filter_to_p_true ???? H5) as H8;
-  lapply (in_list_filter_to_p_true ???? H6) as H9;
-  lapply (LV_subst_X ???? H7);
-  cut (LV s1 ⊆ [c1])
-  [cases (in_list_cons_case ???? Hletin)
-   [rewrite > (p_eqb3 ??? H10) in H8;simplify in H8;destruct
-   |lapply (Hcut ? H10);lapply (in_list_singleton_to_eq ??? Hletin1);
-    rewrite > (p_eqb3 ??? Hletin2) in H9;simplify in H9;destruct]
-  |simplify in H4;generalize in match H4;elim (LV s1) 0;simplify
-   [intro;unfold;intros;elim (not_in_list_nil ?? H11)
-   |intros 2;apply (bool_elim ? (a ≟ c1));simplify;intros
-    [unfold;intros;cases (in_list_cons_case ???? H13)
-     [rewrite > H14;rewrite > (p_eqb1 ??? H10);autobatch
-     |apply H11;autobatch]
-    |destruct]]]]]
-qed.
-
-lemma fresh_GV_subst_X_Var : ∀s,c,y.
-  N_fresh X (GV (subst_X s c (Var y))) ∈ GV s → 
-    N_fresh X (GV (subst_X s c (Var y))) = c.
-intros;apply p_eqb1;
-apply (bool_elim ? (N_fresh X (GV (subst_X s c (Var y)))≟c));intro
-[reflexivity
-|lapply (p_eqb2 ??? H1);lapply (p_fresh ? (GV (subst_X s c (Var y))));
- lapply (GV_subst_X_Var s c y);
- elim Hletin1;cases (Hletin2 (N_fresh X (GV (subst_X s c (Var y)))));
- apply H3;apply in_list_filter_r
- [assumption
- |change in ⊢ (???%) with (¬false);apply eq_f;
-  apply p_eqb4;intro;elim (p_eqb2 ??? H1);autobatch]]
-qed.
-
-lemma L_check_aux_complete :
-  ∀F:xheight.∀M.LL F M → ∀n.S_len M ≤ n → L_check_aux F M (S n) = true.
-intros 3;elim H
-[reflexivity
-|simplify;simplify in H5;rewrite > (? : n = S (pred n))
- [rewrite > H2
-  [rewrite > H4
-   [reflexivity
-   |(* H5 *) elim daemon]
-  |(* H5 *) elim daemon]
- |(* H5 *) elim daemon]
-|simplify;simplify in H3;
- rewrite > (? : (F c s ≟ F (N_fresh X (GV (subst_X s c (Var (F c s)))))
-                          (subst_Y (subst_X s c (Var (F c s))) (F c s)
-                            (Par (N_fresh X (GV (subst_X s c (Var (F c s))))))))
-                = true)
- [simplify;
-  rewrite > (? : subst_Y (subst_X s c (Var (F c s))) (F c s)
-                  (Par (N_fresh X (GV (subst_X s c (Var (F c s)))))) =
-                  subst_X s c (Par (N_fresh X (GV (subst_X s c (Var (F c s)))))))
-  [rewrite > (? : n = S (pred n))
-   [rewrite > H2
-    [reflexivity
-    |autobatch
-    |(* H3 *) elim daemon]
-   |(* H3 *) elim daemon]
-  |rewrite < subst_X_decompose
-   [reflexivity
-   |rewrite > (L_to_closed F)
-    [autobatch
-    |lapply (H1 c)
-     [autobatch
-     |intro;reflexivity]]
-   |autobatch]]
- |rewrite < subst_X_decompose
-  [rewrite > subst_X_fp
-   [rewrite < (swap_left X c) in ⊢ (? ? (? ? ? (? ? % ?)) ?);
-    autobatch
-   |autobatch]
-  |rewrite > (L_to_closed F)
-   [autobatch
-   |lapply (H1 c)
-    [autobatch
-    |intro;reflexivity]]
-  |autobatch]]]
-qed.
-
-inductive typ : Type ≝ 
-| TPar : X → typ
-| Fun  : typ → typ → typ.
-
-notation "hvbox(a break ▸ b)" 
-  left associative with precedence 50
-for @{ 'blacktriangleright $a $b }.
-interpretation "STT arrow type" 'blacktriangleright a b = (Fun a b).
-
-include "datatypes/constructors.ma".
-
-definition DOM : list (X × typ) → list X ≝ λC.map ?? (fst ??) C.
-
-inductive context : list (X × typ) → Prop ≝ 
-| ctx_nil  : context []
-| ctx_cons : ∀x,t,C.x ∉ DOM C → context C → context (〈x,t〉::C).
-
-(* ▸ = \rtrif *)
-inductive typing (F:xheight): list (X × typ) → S_exp → typ → Prop ≝
-| t_axiom : ∀C,x,t.context C → 〈x,t〉 ∈ C → typing F C (Par x) t
-| t_App : ∀C,M,N,t,u.typing F C M (t ▸ u) → typing F C N t → 
-          typing F C (App M N) u
-| t_Lam : ∀C,x,M,t,u.x ∉ DOM C → typing F (〈x,t〉::C) M u → 
-          typing F C (Abs (F x M) (subst_X M x (Var (F x M)))) (t ▸ u).
-
-inductive typing2 (F:xheight): list (X × typ) → S_exp → typ → Prop ≝
-| t2_axiom : ∀C,x,t.context C → 〈x,t〉 ∈ C → typing2 F C (Par x) t
-| t2_App : ∀C,M,N,t,u.typing2 F C M (t ▸ u) → typing2 F C N t → 
-          typing2 F C (App M N) u
-| t2_Lam : ∀C,x1,M,t,u.
-          (∀x2.x2 ∉ DOM C → (x2 ∈ GV M → x2 = x1) → 
-            typing2 F (〈x2,t〉::C) (subst_X M x1 (Par x2)) u) → 
-          typing2 F C (Abs (F x1 M) (subst_X M x1 (Var (F x1 M)))) (t ▸ u).
-
-notation > "C ⊢[F] M : t" 
-  non associative with precedence 30 for @{ 'typjudg F $C $M $t }.  
-notation > "C ⊢ M : t" 
-  non associative with precedence 30 for @{ 'typjudg ? $C $M $t }.  
-notation < "mstyle color #007f00 (hvbox(C maction (⊢) (⊢ \sub F) break M : break t))" 
-  non associative with precedence 30 for @{ 'typjudg $F $C $M $t }.  
-interpretation "Fsub subtype judgement" 'typjudg F C M t = (typing F C M t).
-
-notation > "C ⊨[F] M : t" 
-  non associative with precedence 30 for @{ 'typjudg2 F $C $M $t }.  
-notation > "C ⊨ M : t" 
-  non associative with precedence 30 for @{ 'typjudg2 ? $C $M $t }.  
-notation < "mstyle color #007f00 (hvbox(C maction (⊨) (⊨ \sub F) break M : break t))" 
-  non associative with precedence 30 for @{ 'typjudg2 $F $C $M $t }.  
-interpretation "Fsub strong subtype judgement" 'typjudg2 F C M t = (typing2 F C M t).
-
-lemma in_ctx_to_in_DOM : ∀x,t.∀C:list (X × typ).〈x,t〉 ∈ C → x ∈ DOM C.
-intros 3;elim C
-[elim (not_in_list_nil ?? H)
-|elim (in_list_cons_case ???? H1)
- [rewrite < H2;simplify;autobatch
- |cases a;simplify;autobatch]]
-qed.
-
-lemma in_DOM_to_in_ctx : ∀x,C.x ∈ DOM C → ∃t.〈x,t〉 ∈ C.
-intros 2;elim C
-[elim (not_in_list_nil X ? H)
-|elim a in H1;simplify in H1;elim (in_list_cons_case ???? H1)
- [rewrite > H2;autobatch
- |cases (H H2);autobatch]]
-qed.
-
-lemma incl_DOM : ∀l1,l2. l1 ⊆ l2 → DOM l1 ⊆ DOM l2.
-intros;unfold in H;unfold;intros;cases (in_DOM_to_in_ctx ?? H1);autobatch;
-qed.
-
-lemma typing2_weakening : ∀F,C,M,t.
-                         C ⊨[F] M : t → ∀D.context D → C ⊆ D → D ⊨[F] M : t.
-intros 5;elim H;try autobatch size=7;
-apply t2_Lam;intros;apply H2;
-[intro;autobatch
-|*:autobatch]
-qed.
-
-definition swap_list : ∀N:Nset.N → N → list N → list N ≝
-  λN,a,b,l.map ?? (pi_swap ? a b) l.
-
-lemma in_list_swap : ∀N:Nset.∀x,l.x ∈ l → ∀a,b.swap N a b x ∈ swap_list N a b l.
-intros;elim H;simplify;autobatch;
-qed.
-
-definition ctx_swap_X : X → X → list (X × typ) → list (X × typ) ≝ 
-  λx1,x2,C.map ?? (λp.
-    match p with 
-    [pair x t ⇒ 〈pi_swap ? x1 x2 x,t〉]) C.
-
-lemma in_ctx_swap : ∀x,t,C.〈x,t〉 ∈ C → ∀a,b.〈swap ? a b x,t〉 ∈ ctx_swap_X a b C.
-intros;generalize in match H;elim C;
-[elim (not_in_list_nil ?? H1)
-|simplify;inversion H2;simplify;intros;destruct;simplify;autobatch]
-qed.
 
-lemma ctx_swap_X_swap_list : 
-  ∀C,x1,x2.DOM (ctx_swap_X x1 x2 C) = swap_list ? x1 x2 (DOM C).
-intros;elim C
-[reflexivity
-|cases a;simplify;autobatch]
-qed.
-
-lemma swap_list_inv : ∀N,x1,x2,l.swap_list N x1 x2 (swap_list N x1 x2 l) = l.
-intros;elim l;simplify;autobatch;
-qed.
-
-lemma context_eqv : ∀C.context C → ∀a,b.context (ctx_swap_X a b C).
-intros;elim H
-[simplify;autobatch
-|simplify;apply ctx_cons
- [intro;apply H1;rewrite > ctx_swap_X_swap_list in H4;
-  rewrite < (swap_inv ? a b);
-  rewrite < (swap_list_inv ? a b);autobatch
- |assumption]]
-qed.
-
-lemma typing_swap : ∀F:xheight.∀C,M,t,x1,x2.
-  C ⊨[F] M : t → ctx_swap_X x1 x2 C ⊨[F] (pi_swap ? x1 x2)·M : t.
-intros;elim H
-[simplify;apply t2_axiom
- [autobatch
- |rewrite < eq_swap_pi;autobatch]
-|simplify;autobatch
-|simplify;rewrite > pi_lemma1;simplify;applyS t2_Lam;
- intros;rewrite < (swap_inv ? x1 x2 x);
- change in ⊢ (? ? ? (? ? ? %) ?) with (pi_swap X x1 x2 · Par (swap X x1 x2 x));
- rewrite < pi_lemma1;apply H2
- [intro;apply H3;rewrite < (swap_inv ? x1 x2 x);
-  rewrite > ctx_swap_X_swap_list;autobatch
- |intro;rewrite > H4;autobatch]]
-qed.
-
-lemma typing_to_typing2 : ∀F:xheight.∀C,M,t.C ⊢[F] M : t → C ⊨[F] M : t.
-intros;elim H;try autobatch;
-apply t2_Lam;intros;
-rewrite > subst_X_fp
-[rewrite > (? : 〈x2,t1〉::l = ctx_swap_X c x2 (〈c,t1〉::l))
- [autobatch
- |simplify;rewrite < eq_swap_pi;rewrite > swap_left;
-  rewrite < (? : l = ctx_swap_X c x2 l)
-  [reflexivity
-  |generalize in match H1;generalize in match H4;elim l 0
-   [intros;reflexivity
-   |intro;cases a;simplify;intros;
-    rewrite < eq_swap_pi;rewrite > swap_other
-    [rewrite < H6
-     [reflexivity
-     |*:intro;autobatch]
-    |*:intro;autobatch]]]]
-|assumption]
-qed.
+1) dimostrare che GV di un term judgment (debole) è vuoto
+2) dimostrare che pi*T = T se GV(T) = []
+3) term judgment forte -> term judgment debole
+4) allora per 1+2 => term judgment equivariante (entrambi)
+5) 4) => term judgment debole
 
-lemma typing2_to_typing : ∀F:xheight.∀C,M,t.C ⊨[F] M : t → C ⊢[F] M : t.
-intros;elim H;try autobatch;
-generalize in match (p_fresh ? (c::DOM l@GV s));
-generalize in match (N_fresh ? (c::DOM l@GV s));
-intros (xn f_xn);
-lapply (H2 xn)
-[rewrite > subst_X_fp in Hletin
- [lapply (t_Lam ??????? Hletin)
-  [intro;apply f_xn;autobatch
-  |rewrite < subst_X_fp in Hletin1
-   [rewrite > subst_X_merge in Hletin1
-    [rewrite < (? : F c s = F xn (subst_X s c (Par xn))) in Hletin1
-     [assumption
-     |rewrite > subst_X_fp
-      [rewrite < (swap_left ? c xn) in ⊢ (? ? ? (? ? % ?));
-       rewrite > eq_swap_pi;autobatch]]]]]]]
-intro;elim f_xn;autobatch;
-qed.
\ No newline at end of file
+*)
\ No newline at end of file