From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 24 Jan 2007 19:44:22 +0000 (+0000)
Subject: tactics.mli: regenerated
X-Git-Tag: 0.4.95@7852~649
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=067c2f773a1053cab1d6cd25a92e0bcc1763c305;p=helm.git

tactics.mli: regenerated
LambdaDelta: regenerated with some new theorems
---

diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli
index eb290ff05..d821a3cb2 100644
--- a/components/tactics/tactics.mli
+++ b/components/tactics/tactics.mli
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Sun Jan 14 12:32:17 CET 2007 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Jan 24 20:31:34 CET 2007 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS :
diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ex1/defs.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ex1/defs.ma
new file mode 100644
index 000000000..9786b3779
--- /dev/null
+++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ex1/defs.ma
@@ -0,0 +1,31 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/ex1/defs".
+
+include "C/defs.ma".
+
+definition ex1_c:
+ C
+\def
+ CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
+(Bind Abst) (TLRef O).
+
+definition ex1_t:
+ T
+\def
+ THead (Flat Appl) (TLRef O) (THead (Bind Abst) (TLRef (S (S O))) (TSort O)).
+
diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ex1/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ex1/props.ma
new file mode 100644
index 000000000..b78fe0c92
--- /dev/null
+++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ex1/props.ma
@@ -0,0 +1,540 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/ex1/props".
+
+include "ex1/defs.ma".
+
+include "ty3/fwd.ma".
+
+include "pc3/fwd.ma".
+
+include "nf2/pr3.ma".
+
+include "nf2/props.ma".
+
+include "arity/defs.ma".
+
+include "leq/props.ma".
+
+theorem ex1__leq_sort_SS:
+ \forall (g: G).(\forall (k: nat).(\forall (n: nat).(leq g (ASort k n) (asucc 
+g (asucc g (ASort (S (S k)) n))))))
+\def
+ \lambda (g: G).(\lambda (k: nat).(\lambda (n: nat).(leq_refl g (asucc g 
+(asucc g (ASort (S (S k)) n)))))).
+
+theorem ex1_arity:
+ \forall (g: G).(arity g ex1_c ex1_t (ASort O O))
+\def
+ \lambda (g: G).(arity_appl g (CHead (CHead (CHead (CSort O) (Bind Abst) 
+(TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef O) (ASort (S 
+(S O)) O) (arity_abst g (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) 
+(Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) (TLRef O) O (getl_refl Abst (CHead 
+(CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (TLRef O)) 
+(ASort (S (S O)) O) (arity_abst g (CHead (CHead (CSort O) (Bind Abst) (TSort 
+O)) (Bind Abst) (TSort O)) (CHead (CSort O) (Bind Abst) (TSort O)) (TSort O) 
+O (getl_refl Abst (CHead (CSort O) (Bind Abst) (TSort O)) (TSort O)) (asucc g 
+(ASort (S (S O)) O)) (arity_repl g (CHead (CSort O) (Bind Abst) (TSort O)) 
+(TSort O) (ASort O O) (arity_sort g (CHead (CSort O) (Bind Abst) (TSort O)) 
+O) (asucc g (asucc g (ASort (S (S O)) O))) (ex1__leq_sort_SS g O O)))) (THead 
+(Bind Abst) (TLRef (S (S O))) (TSort O)) (ASort O O) (arity_head g (CHead 
+(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind 
+Abst) (TLRef O)) (TLRef (S (S O))) (ASort (S (S O)) O) (arity_abst g (CHead 
+(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind 
+Abst) (TLRef O)) (CSort O) (TSort O) (S (S O)) (getl_clear_bind Abst (CHead 
+(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind 
+Abst) (TLRef O)) (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
+(TSort O)) (TLRef O) (clear_bind Abst (CHead (CHead (CSort O) (Bind Abst) 
+(TSort O)) (Bind Abst) (TSort O)) (TLRef O)) (CHead (CSort O) (Bind Abst) 
+(TSort O)) (S O) (getl_head (Bind Abst) O (CHead (CSort O) (Bind Abst) (TSort 
+O)) (CHead (CSort O) (Bind Abst) (TSort O)) (getl_refl Abst (CSort O) (TSort 
+O)) (TSort O))) (asucc g (ASort (S (S O)) O)) (arity_repl g (CSort O) (TSort 
+O) (ASort O O) (arity_sort g (CSort O) O) (asucc g (asucc g (ASort (S (S O)) 
+O))) (ex1__leq_sort_SS g O O))) (TSort O) (ASort O O) (arity_sort g (CHead 
+(CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
+(Bind Abst) (TLRef O)) (Bind Abst) (TLRef (S (S O)))) O))).
+
+theorem ex1_ty3:
+ \forall (g: G).(\forall (u: T).((ty3 g ex1_c ex1_t u) \to (\forall (P: 
+Prop).P)))
+\def
+ \lambda (g: G).(\lambda (u: T).(\lambda (H: (ty3 g (CHead (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
+O)) (THead (Flat Appl) (TLRef O) (THead (Bind Abst) (TLRef (S (S O))) (TSort 
+O))) u)).(\lambda (P: Prop).(ex3_2_ind T T (\lambda (u0: T).(\lambda (t: 
+T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
+(TSort O)) (Bind Abst) (TLRef O)) (THead (Flat Appl) (TLRef O) (THead (Bind 
+Abst) u0 t)) u))) (\lambda (u0: T).(\lambda (t: T).(ty3 g (CHead (CHead 
+(CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) 
+(TLRef O)) (THead (Bind Abst) (TLRef (S (S O))) (TSort O)) (THead (Bind Abst) 
+u0 t)))) (\lambda (u0: T).(\lambda (_: T).(ty3 g (CHead (CHead (CHead (CSort 
+O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) 
+(TLRef O) u0))) P (\lambda (x0: T).(\lambda (x1: T).(\lambda (_: (pc3 (CHead 
+(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind 
+Abst) (TLRef O)) (THead (Flat Appl) (TLRef O) (THead (Bind Abst) x0 x1)) 
+u)).(\lambda (H1: (ty3 g (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort 
+O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (THead (Bind Abst) (TLRef 
+(S (S O))) (TSort O)) (THead (Bind Abst) x0 x1))).(\lambda (H2: (ty3 g (CHead 
+(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind 
+Abst) (TLRef O)) (TLRef O) x0)).(or_ind (ex3_3 C T T (\lambda (_: C).(\lambda 
+(_: T).(\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort 
+O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S O) O t) x0)))) 
+(\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
+O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda 
+(t: T).(ty3 g e u0 t))))) (ex3_3 C T T (\lambda (_: C).(\lambda (u0: 
+T).(\lambda (_: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) 
+(Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S O) O u0) x0)))) 
+(\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
+O)) (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda 
+(t: T).(ty3 g e u0 t))))) P (\lambda (H3: (ex3_3 C T T (\lambda (_: 
+C).(\lambda (_: T).(\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S O) O 
+t) x0)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead 
+(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind 
+Abst) (TLRef O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: 
+T).(\lambda (t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T (\lambda (_: 
+C).(\lambda (_: T).(\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S O) O 
+t) x0)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead 
+(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind 
+Abst) (TLRef O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: 
+T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda (x2: C).(\lambda (x3: 
+T).(\lambda (x4: T).(\lambda (_: (pc3 (CHead (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S O) O 
+x4) x0)).(\lambda (H5: (getl O (CHead (CHead (CHead (CSort O) (Bind Abst) 
+(TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead x2 (Bind 
+Abbr) x3))).(\lambda (_: (ty3 g x2 x3 x4)).(ex4_3_ind T T T (\lambda (t2: 
+T).(\lambda (_: T).(\lambda (_: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (THead (Bind 
+Abst) (TLRef (S (S O))) t2) (THead (Bind Abst) x0 x1))))) (\lambda (_: 
+T).(\lambda (t: T).(\lambda (_: T).(ty3 g (CHead (CHead (CHead (CSort O) 
+(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef 
+(S (S O))) t)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(ty3 g 
+(CHead (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
+(TSort O)) (Bind Abst) (TLRef O)) (Bind Abst) (TLRef (S (S O)))) (TSort O) 
+t2)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (t0: T).(ty3 g (CHead (CHead 
+(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind 
+Abst) (TLRef O)) (Bind Abst) (TLRef (S (S O)))) t2 t0)))) P (\lambda (x5: 
+T).(\lambda (x6: T).(\lambda (x7: T).(\lambda (_: (pc3 (CHead (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
+O)) (THead (Bind Abst) (TLRef (S (S O))) x5) (THead (Bind Abst) x0 
+x1))).(\lambda (H8: (ty3 g (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort 
+O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O))) 
+x6)).(\lambda (_: (ty3 g (CHead (CHead (CHead (CHead (CSort O) (Bind Abst) 
+(TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (Bind Abst) (TLRef 
+(S (S O)))) (TSort O) x5)).(\lambda (_: (ty3 g (CHead (CHead (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
+O)) (Bind Abst) (TLRef (S (S O)))) x5 x7)).(or_ind (ex3_3 C T T (\lambda (_: 
+C).(\lambda (_: T).(\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S 
+O))) O t) x6)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S 
+O)) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort 
+O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: 
+C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t))))) (ex3_3 C T T (\lambda 
+(_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CHead (CSort O) 
+(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S 
+(S (S O))) O u0) x6)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: 
+T).(getl (S (S O)) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) 
+(Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0))))) 
+(\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t))))) P 
+(\lambda (H11: (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t: 
+T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
+(TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O t) x6)))) (\lambda 
+(e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O)) (CHead (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
+O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda 
+(t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (_: 
+T).(\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) 
+(Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O t) x6)))) 
+(\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O)) (CHead 
+(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind 
+Abst) (TLRef O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: 
+T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda (x8: C).(\lambda (x9: 
+T).(\lambda (x10: T).(\lambda (_: (pc3 (CHead (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S 
+O))) O x10) x6)).(\lambda (H13: (getl (S (S O)) (CHead (CHead (CHead (CSort 
+O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) 
+(CHead x8 (Bind Abbr) x9))).(\lambda (_: (ty3 g x8 x9 x10)).(let H15 \def 
+(getl_gen_all (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
+(TSort O)) (CHead x8 (Bind Abbr) x9) (r (Bind Abst) (S O)) (getl_gen_S (Bind 
+Abst) (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
+(CHead x8 (Bind Abbr) x9) (TLRef O) (S O) H13)) in (ex2_ind C (\lambda (e: 
+C).(drop (S O) O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
+(TSort O)) e)) (\lambda (e: C).(clear e (CHead x8 (Bind Abbr) x9))) P 
+(\lambda (x: C).(\lambda (_: (drop (S O) O (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) x)).(\lambda (_: (clear x (CHead x8 
+(Bind Abbr) x9))).(let H18 \def (eq_ind C (CHead x2 (Bind Abbr) x3) (\lambda 
+(ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _) 
+\Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return (\lambda 
+(_: K).Prop) with [(Bind b) \Rightarrow (match b in B return (\lambda (_: 
+B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow False | Void 
+\Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
+O)) (clear_gen_bind Abst (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind 
+Abst) (TSort O)) (CHead x2 (Bind Abbr) x3) (TLRef O) (getl_gen_O (CHead 
+(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind 
+Abst) (TLRef O)) (CHead x2 (Bind Abbr) x3) H5))) in (False_ind P H18))))) 
+H15)))))))) H11)) (\lambda (H11: (ex3_3 C T T (\lambda (_: C).(\lambda (u0: 
+T).(\lambda (_: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) 
+(Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O u0) 
+x6)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O)) 
+(CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
+(Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda 
+(u0: T).(\lambda (t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T (\lambda (_: 
+C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S 
+O))) O u0) x6)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S 
+(S O)) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
+(TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0))))) (\lambda (e: 
+C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda (x8: 
+C).(\lambda (x9: T).(\lambda (x10: T).(\lambda (_: (pc3 (CHead (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
+O)) (lift (S (S (S O))) O x9) x6)).(\lambda (H13: (getl (S (S O)) (CHead 
+(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind 
+Abst) (TLRef O)) (CHead x8 (Bind Abst) x9))).(\lambda (_: (ty3 g x8 x9 
+x10)).(let H15 \def (getl_gen_all (CHead (CHead (CSort O) (Bind Abst) (TSort 
+O)) (Bind Abst) (TSort O)) (CHead x8 (Bind Abst) x9) (r (Bind Abst) (S O)) 
+(getl_gen_S (Bind Abst) (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind 
+Abst) (TSort O)) (CHead x8 (Bind Abst) x9) (TLRef O) (S O) H13)) in (ex2_ind 
+C (\lambda (e: C).(drop (S O) O (CHead (CHead (CSort O) (Bind Abst) (TSort 
+O)) (Bind Abst) (TSort O)) e)) (\lambda (e: C).(clear e (CHead x8 (Bind Abst) 
+x9))) P (\lambda (x: C).(\lambda (_: (drop (S O) O (CHead (CHead (CSort O) 
+(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) x)).(\lambda (_: (clear x 
+(CHead x8 (Bind Abst) x9))).(let H18 \def (eq_ind C (CHead x2 (Bind Abbr) x3) 
+(\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _) 
+\Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return (\lambda 
+(_: K).Prop) with [(Bind b) \Rightarrow (match b in B return (\lambda (_: 
+B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow False | Void 
+\Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
+O)) (clear_gen_bind Abst (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind 
+Abst) (TSort O)) (CHead x2 (Bind Abbr) x3) (TLRef O) (getl_gen_O (CHead 
+(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind 
+Abst) (TLRef O)) (CHead x2 (Bind Abbr) x3) H5))) in (False_ind P H18))))) 
+H15)))))))) H11)) (ty3_gen_lref g (CHead (CHead (CHead (CSort O) (Bind Abst) 
+(TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) x6 (S (S O)) 
+H8))))))))) (ty3_gen_bind g Abst (CHead (CHead (CHead (CSort O) (Bind Abst) 
+(TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O))) 
+(TSort O) (THead (Bind Abst) x0 x1) H1)))))))) H3)) (\lambda (H3: (ex3_3 C T 
+T (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
+O)) (lift (S O) O u0) x0)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: 
+T).(getl O (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
+(TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0))))) (\lambda (e: 
+C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T 
+(\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
+O)) (lift (S O) O u0) x0)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: 
+T).(getl O (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
+(TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0))))) (\lambda (e: 
+C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda (x2: 
+C).(\lambda (x3: T).(\lambda (x4: T).(\lambda (H4: (pc3 (CHead (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
+O)) (lift (S O) O x3) x0)).(\lambda (H5: (getl O (CHead (CHead (CHead (CSort 
+O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) 
+(CHead x2 (Bind Abst) x3))).(\lambda (H6: (ty3 g x2 x3 x4)).(ex4_3_ind T T T 
+(\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(pc3 (CHead (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
+O)) (THead (Bind Abst) (TLRef (S (S O))) t2) (THead (Bind Abst) x0 x1))))) 
+(\lambda (_: T).(\lambda (t: T).(\lambda (_: T).(ty3 g (CHead (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
+O)) (TLRef (S (S O))) t)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (_: 
+T).(ty3 g (CHead (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind 
+Abst) (TSort O)) (Bind Abst) (TLRef O)) (Bind Abst) (TLRef (S (S O)))) (TSort 
+O) t2)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (t0: T).(ty3 g (CHead 
+(CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
+(Bind Abst) (TLRef O)) (Bind Abst) (TLRef (S (S O)))) t2 t0)))) P (\lambda 
+(x5: T).(\lambda (x6: T).(\lambda (x7: T).(\lambda (H7: (pc3 (CHead (CHead 
+(CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) 
+(TLRef O)) (THead (Bind Abst) (TLRef (S (S O))) x5) (THead (Bind Abst) x0 
+x1))).(\lambda (H8: (ty3 g (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort 
+O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O))) 
+x6)).(\lambda (_: (ty3 g (CHead (CHead (CHead (CHead (CSort O) (Bind Abst) 
+(TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (Bind Abst) (TLRef 
+(S (S O)))) (TSort O) x5)).(\lambda (_: (ty3 g (CHead (CHead (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
+O)) (Bind Abst) (TLRef (S (S O)))) x5 x7)).(or_ind (ex3_3 C T T (\lambda (_: 
+C).(\lambda (_: T).(\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S 
+O))) O t) x6)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S 
+O)) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort 
+O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: 
+C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t))))) (ex3_3 C T T (\lambda 
+(_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CHead (CSort O) 
+(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S 
+(S (S O))) O u0) x6)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: 
+T).(getl (S (S O)) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) 
+(Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0))))) 
+(\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t))))) P 
+(\lambda (H11: (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t: 
+T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
+(TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O t) x6)))) (\lambda 
+(e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O)) (CHead (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
+O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda 
+(t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (_: 
+T).(\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) 
+(Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O t) x6)))) 
+(\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O)) (CHead 
+(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind 
+Abst) (TLRef O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: 
+T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda (x8: C).(\lambda (x9: 
+T).(\lambda (x10: T).(\lambda (_: (pc3 (CHead (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S 
+O))) O x10) x6)).(\lambda (H13: (getl (S (S O)) (CHead (CHead (CHead (CSort 
+O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) 
+(CHead x8 (Bind Abbr) x9))).(\lambda (_: (ty3 g x8 x9 x10)).(let H15 \def 
+(getl_gen_all (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
+(TSort O)) (CHead x8 (Bind Abbr) x9) (r (Bind Abst) (S O)) (getl_gen_S (Bind 
+Abst) (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
+(CHead x8 (Bind Abbr) x9) (TLRef O) (S O) H13)) in (ex2_ind C (\lambda (e: 
+C).(drop (S O) O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
+(TSort O)) e)) (\lambda (e: C).(clear e (CHead x8 (Bind Abbr) x9))) P 
+(\lambda (x: C).(\lambda (H16: (drop (S O) O (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) x)).(\lambda (H17: (clear x (CHead x8 
+(Bind Abbr) x9))).(let H18 \def (f_equal C C (\lambda (e: C).(match e in C 
+return (\lambda (_: C).C) with [(CSort _) \Rightarrow x2 | (CHead c _ _) 
+\Rightarrow c])) (CHead x2 (Bind Abst) x3) (CHead (CHead (CHead (CSort O) 
+(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) 
+(clear_gen_bind Abst (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind 
+Abst) (TSort O)) (CHead x2 (Bind Abst) x3) (TLRef O) (getl_gen_O (CHead 
+(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind 
+Abst) (TLRef O)) (CHead x2 (Bind Abst) x3) H5))) in ((let H19 \def (f_equal C 
+T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _) 
+\Rightarrow x3 | (CHead _ _ t) \Rightarrow t])) (CHead x2 (Bind Abst) x3) 
+(CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
+(Bind Abst) (TLRef O)) (clear_gen_bind Abst (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead x2 (Bind Abst) x3) (TLRef O) 
+(getl_gen_O (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
+(TSort O)) (Bind Abst) (TLRef O)) (CHead x2 (Bind Abst) x3) H5))) in (\lambda 
+(H20: (eq C x2 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
+(TSort O)))).(let H21 \def (eq_ind T x3 (\lambda (t: T).(ty3 g x2 t x4)) H6 
+(TLRef O) H19) in (let H22 \def (eq_ind T x3 (\lambda (t: T).(pc3 (CHead 
+(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind 
+Abst) (TLRef O)) (lift (S O) O t) x0)) H4 (TLRef O) H19) in (let H23 \def 
+(eq_ind C x2 (\lambda (c: C).(ty3 g c (TLRef O) x4)) H21 (CHead (CHead (CSort 
+O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) H20) in (let H24 \def 
+(eq_ind_r C x (\lambda (c: C).(clear c (CHead x8 (Bind Abbr) x9))) H17 (CHead 
+(CSort O) (Bind Abst) (TSort O)) (drop_gen_refl (CHead (CSort O) (Bind Abst) 
+(TSort O)) x (drop_gen_drop (Bind Abst) (CHead (CSort O) (Bind Abst) (TSort 
+O)) x (TSort O) O H16))) in (let H25 \def (eq_ind C (CHead x8 (Bind Abbr) x9) 
+(\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _) 
+\Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return (\lambda 
+(_: K).Prop) with [(Bind b) \Rightarrow (match b in B return (\lambda (_: 
+B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow False | Void 
+\Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead (CSort O) 
+(Bind Abst) (TSort O)) (clear_gen_bind Abst (CSort O) (CHead x8 (Bind Abbr) 
+x9) (TSort O) H24)) in (False_ind P H25)))))))) H18))))) H15)))))))) H11)) 
+(\lambda (H11: (ex3_3 C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_: 
+T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
+(TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O u0) x6)))) (\lambda 
+(e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O)) (CHead (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
+O)) (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda 
+(t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (u0: 
+T).(\lambda (_: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) 
+(Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O u0) 
+x6)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O)) 
+(CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
+(Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda 
+(u0: T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda (x8: C).(\lambda (x9: 
+T).(\lambda (x10: T).(\lambda (H12: (pc3 (CHead (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S 
+O))) O x9) x6)).(\lambda (H13: (getl (S (S O)) (CHead (CHead (CHead (CSort O) 
+(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead 
+x8 (Bind Abst) x9))).(\lambda (H14: (ty3 g x8 x9 x10)).(let H15 \def 
+(getl_gen_all (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
+(TSort O)) (CHead x8 (Bind Abst) x9) (r (Bind Abst) (S O)) (getl_gen_S (Bind 
+Abst) (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
+(CHead x8 (Bind Abst) x9) (TLRef O) (S O) H13)) in (ex2_ind C (\lambda (e: 
+C).(drop (S O) O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
+(TSort O)) e)) (\lambda (e: C).(clear e (CHead x8 (Bind Abst) x9))) P 
+(\lambda (x: C).(\lambda (H16: (drop (S O) O (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) x)).(\lambda (H17: (clear x (CHead x8 
+(Bind Abst) x9))).(let H18 \def (f_equal C C (\lambda (e: C).(match e in C 
+return (\lambda (_: C).C) with [(CSort _) \Rightarrow x2 | (CHead c _ _) 
+\Rightarrow c])) (CHead x2 (Bind Abst) x3) (CHead (CHead (CHead (CSort O) 
+(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) 
+(clear_gen_bind Abst (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind 
+Abst) (TSort O)) (CHead x2 (Bind Abst) x3) (TLRef O) (getl_gen_O (CHead 
+(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind 
+Abst) (TLRef O)) (CHead x2 (Bind Abst) x3) H5))) in ((let H19 \def (f_equal C 
+T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _) 
+\Rightarrow x3 | (CHead _ _ t) \Rightarrow t])) (CHead x2 (Bind Abst) x3) 
+(CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
+(Bind Abst) (TLRef O)) (clear_gen_bind Abst (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead x2 (Bind Abst) x3) (TLRef O) 
+(getl_gen_O (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
+(TSort O)) (Bind Abst) (TLRef O)) (CHead x2 (Bind Abst) x3) H5))) in (\lambda 
+(H20: (eq C x2 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
+(TSort O)))).(let H21 \def (eq_ind T x3 (\lambda (t: T).(ty3 g x2 t x4)) H6 
+(TLRef O) H19) in (let H22 \def (eq_ind T x3 (\lambda (t: T).(pc3 (CHead 
+(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind 
+Abst) (TLRef O)) (lift (S O) O t) x0)) H4 (TLRef O) H19) in (let H23 \def 
+(eq_ind C x2 (\lambda (c: C).(ty3 g c (TLRef O) x4)) H21 (CHead (CHead (CSort 
+O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) H20) in (let H24 \def 
+(eq_ind_r C x (\lambda (c: C).(clear c (CHead x8 (Bind Abst) x9))) H17 (CHead 
+(CSort O) (Bind Abst) (TSort O)) (drop_gen_refl (CHead (CSort O) (Bind Abst) 
+(TSort O)) x (drop_gen_drop (Bind Abst) (CHead (CSort O) (Bind Abst) (TSort 
+O)) x (TSort O) O H16))) in (let H25 \def (f_equal C C (\lambda (e: C).(match 
+e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow x8 | (CHead c _ 
+_) \Rightarrow c])) (CHead x8 (Bind Abst) x9) (CHead (CSort O) (Bind Abst) 
+(TSort O)) (clear_gen_bind Abst (CSort O) (CHead x8 (Bind Abst) x9) (TSort O) 
+H24)) in ((let H26 \def (f_equal C T (\lambda (e: C).(match e in C return 
+(\lambda (_: C).T) with [(CSort _) \Rightarrow x9 | (CHead _ _ t) \Rightarrow 
+t])) (CHead x8 (Bind Abst) x9) (CHead (CSort O) (Bind Abst) (TSort O)) 
+(clear_gen_bind Abst (CSort O) (CHead x8 (Bind Abst) x9) (TSort O) H24)) in 
+(\lambda (H27: (eq C x8 (CSort O))).(let H28 \def (eq_ind T x9 (\lambda (t: 
+T).(ty3 g x8 t x10)) H14 (TSort O) H26) in (let H29 \def (eq_ind T x9 
+(\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) 
+(Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O t) x6)) 
+H12 (TSort O) H26) in (let H30 \def (eq_ind C x8 (\lambda (c: C).(ty3 g c 
+(TSort O) x10)) H28 (CSort O) H27) in (or_ind (ex3_3 C T T (\lambda (_: 
+C).(\lambda (_: T).(\lambda (t: T).(pc3 (CHead (CHead (CSort O) (Bind Abst) 
+(TSort O)) (Bind Abst) (TSort O)) (lift (S O) O t) x4)))) (\lambda (e: 
+C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead e (Bind Abbr) u0))))) (\lambda 
+(e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t))))) (ex3_3 C T T 
+(\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CSort O) 
+(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (lift (S O) O u0) x4)))) 
+(\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead (CHead (CSort 
+O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead e (Bind Abst) u0))))) 
+(\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t))))) P 
+(\lambda (H31: (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t: 
+T).(pc3 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
+(lift (S O) O t) x4)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: 
+T).(getl O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort 
+O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda 
+(t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (_: 
+T).(\lambda (t: T).(pc3 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind 
+Abst) (TSort O)) (lift (S O) O t) x4)))) (\lambda (e: C).(\lambda (u0: 
+T).(\lambda (_: T).(getl O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) 
+(Bind Abst) (TSort O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda 
+(u0: T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda (x11: C).(\lambda (x12: 
+T).(\lambda (x13: T).(\lambda (_: (pc3 (CHead (CHead (CSort O) (Bind Abst) 
+(TSort O)) (Bind Abst) (TSort O)) (lift (S O) O x13) x4)).(\lambda (H33: 
+(getl O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
+(CHead x11 (Bind Abbr) x12))).(\lambda (_: (ty3 g x11 x12 x13)).(let H35 \def 
+(eq_ind C (CHead x11 (Bind Abbr) x12) (\lambda (ee: C).(match ee in C return 
+(\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) 
+\Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind b) 
+\Rightarrow (match b in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow 
+True | Abst \Rightarrow False | Void \Rightarrow False]) | (Flat _) 
+\Rightarrow False])])) I (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind 
+Abst) (TSort O)) (clear_gen_bind Abst (CHead (CSort O) (Bind Abst) (TSort O)) 
+(CHead x11 (Bind Abbr) x12) (TSort O) (getl_gen_O (CHead (CHead (CSort O) 
+(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead x11 (Bind Abbr) x12) 
+H33))) in (False_ind P H35)))))))) H31)) (\lambda (H31: (ex3_3 C T T (\lambda 
+(_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) (lift (S O) O u0) x4)))) (\lambda (e: 
+C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead e (Bind Abst) u0))))) (\lambda 
+(e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T 
+(\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CSort O) 
+(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (lift (S O) O u0) x4)))) 
+(\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead (CHead (CSort 
+O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead e (Bind Abst) u0))))) 
+(\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda 
+(x11: C).(\lambda (x12: T).(\lambda (x13: T).(\lambda (H32: (pc3 (CHead 
+(CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (lift (S O) O 
+x12) x4)).(\lambda (H33: (getl O (CHead (CHead (CSort O) (Bind Abst) (TSort 
+O)) (Bind Abst) (TSort O)) (CHead x11 (Bind Abst) x12))).(\lambda (H34: (ty3 
+g x11 x12 x13)).(let H35 \def (f_equal C C (\lambda (e: C).(match e in C 
+return (\lambda (_: C).C) with [(CSort _) \Rightarrow x11 | (CHead c _ _) 
+\Rightarrow c])) (CHead x11 (Bind Abst) x12) (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) (clear_gen_bind Abst (CHead (CSort O) 
+(Bind Abst) (TSort O)) (CHead x11 (Bind Abst) x12) (TSort O) (getl_gen_O 
+(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead 
+x11 (Bind Abst) x12) H33))) in ((let H36 \def (f_equal C T (\lambda (e: 
+C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow x12 | 
+(CHead _ _ t) \Rightarrow t])) (CHead x11 (Bind Abst) x12) (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (clear_gen_bind Abst 
+(CHead (CSort O) (Bind Abst) (TSort O)) (CHead x11 (Bind Abst) x12) (TSort O) 
+(getl_gen_O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort 
+O)) (CHead x11 (Bind Abst) x12) H33))) in (\lambda (H37: (eq C x11 (CHead 
+(CSort O) (Bind Abst) (TSort O)))).(let H38 \def (eq_ind T x12 (\lambda (t: 
+T).(ty3 g x11 t x13)) H34 (TSort O) H36) in (let H39 \def (eq_ind T x12 
+(\lambda (t: T).(pc3 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind 
+Abst) (TSort O)) (lift (S O) O t) x4)) H32 (TSort O) H36) in (let H40 \def 
+(eq_ind C x11 (\lambda (c: C).(ty3 g c (TSort O) x13)) H38 (CHead (CSort O) 
+(Bind Abst) (TSort O)) H37) in (and_ind (pc3 (CHead (CHead (CHead (CSort O) 
+(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef 
+(S (S O))) x0) (\forall (b: B).(\forall (u0: T).(pc3 (CHead (CHead (CHead 
+(CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) 
+(TLRef O)) (Bind b) u0) x5 x1))) P (\lambda (H41: (pc3 (CHead (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
+O)) (TLRef (S (S O))) x0)).(\lambda (_: ((\forall (b: B).(\forall (u0: 
+T).(pc3 (CHead (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind 
+Abst) (TSort O)) (Bind Abst) (TLRef O)) (Bind b) u0) x5 x1))))).(let H43 \def 
+(eq_ind T (lift (S O) O (TLRef O)) (\lambda (t: T).(pc3 (CHead (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
+O)) (TLRef (S (S O))) t)) (pc3_t x0 (CHead (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S 
+O))) H41 (lift (S O) O (TLRef O)) (pc3_s (CHead (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) x0 (lift (S O) 
+O (TLRef O)) H22)) (TLRef (plus O (S O))) (lift_lref_ge O (S O) O (le_n O))) 
+in (let H44 \def H43 in (ex2_ind T (\lambda (t: T).(pr3 (CHead (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
+O)) (TLRef (S (S O))) t)) (\lambda (t: T).(pr3 (CHead (CHead (CHead (CSort O) 
+(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef 
+(S O)) t)) P (\lambda (x14: T).(\lambda (H45: (pr3 (CHead (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
+O)) (TLRef (S (S O))) x14)).(\lambda (H46: (pr3 (CHead (CHead (CHead (CSort 
+O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) 
+(TLRef (S O)) x14)).(let H47 \def (eq_ind_r T x14 (\lambda (t: T).(eq T 
+(TLRef (S (S O))) t)) (nf2_pr3_unfold (CHead (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S 
+O))) x14 H45 (nf2_lref_abst (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort 
+O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CSort O) (TSort O) (S (S 
+O)) (getl_clear_bind Abst (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort 
+O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead (CHead (CSort O) 
+(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (TLRef O) (clear_bind Abst 
+(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (TLRef 
+O)) (CHead (CSort O) (Bind Abst) (TSort O)) (S O) (getl_head (Bind Abst) O 
+(CHead (CSort O) (Bind Abst) (TSort O)) (CHead (CSort O) (Bind Abst) (TSort 
+O)) (getl_refl Abst (CSort O) (TSort O)) (TSort O))))) (TLRef (S O)) 
+(nf2_pr3_unfold (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind 
+Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S O)) x14 H46 (nf2_lref_abst 
+(CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
+(Bind Abst) (TLRef O)) (CHead (CSort O) (Bind Abst) (TSort O)) (TSort O) (S 
+O) (getl_head (Bind Abst) O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) 
+(Bind Abst) (TSort O)) (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind 
+Abst) (TSort O)) (getl_refl Abst (CHead (CSort O) (Bind Abst) (TSort O)) 
+(TSort O)) (TLRef O))))) in (let H48 \def (eq_ind T (TLRef (S (S O))) 
+(\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) 
+\Rightarrow False | (TLRef n) \Rightarrow (match n in nat return (\lambda (_: 
+nat).Prop) with [O \Rightarrow False | (S n0) \Rightarrow (match n0 in nat 
+return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow 
+True])]) | (THead _ _ _) \Rightarrow False])) I (TLRef (S O)) H47) in 
+(False_ind P H48)))))) H44))))) (pc3_gen_abst (CHead (CHead (CHead (CSort O) 
+(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef 
+(S (S O))) x0 x5 x1 H7))))))) H35)))))))) H31)) (ty3_gen_lref g (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) x4 O H23))))))) 
+H25)))))))) H18))))) H15)))))))) H11)) (ty3_gen_lref g (CHead (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
+O)) x6 (S (S O)) H8))))))))) (ty3_gen_bind g Abst (CHead (CHead (CHead (CSort 
+O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) 
+(TLRef (S (S O))) (TSort O) (THead (Bind Abst) x0 x1) H1)))))))) H3)) 
+(ty3_gen_lref g (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind 
+Abst) (TSort O)) (Bind Abst) (TLRef O)) x0 O H2))))))) (ty3_gen_appl g (CHead 
+(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind 
+Abst) (TLRef O)) (TLRef O) (THead (Bind Abst) (TLRef (S (S O))) (TSort O)) u 
+H))))).
+
diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc1/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc1/props.ma
index f670f0eaf..980c1ae50 100644
--- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc1/props.ma
+++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc1/props.ma
@@ -25,13 +25,13 @@ theorem pc1_pr0_r:
 \def
  \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr0 t1 t2)).(ex_intro2 T 
 (\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t2 t)) t2 (pr1_pr0 t1 t2 H) 
-(pr1_r t2)))).
+(pr1_refl t2)))).
 
 theorem pc1_pr0_x:
  \forall (t1: T).(\forall (t2: T).((pr0 t2 t1) \to (pc1 t1 t2)))
 \def
  \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr0 t2 t1)).(ex_intro2 T 
-(\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t2 t)) t1 (pr1_r t1) 
+(\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t2 t)) t1 (pr1_refl t1) 
 (pr1_pr0 t2 t1 H)))).
 
 theorem pc1_pr0_u:
@@ -42,14 +42,14 @@ t3) \to (pc1 t1 t3)))))
 T).(\lambda (H0: (pc1 t2 t3)).(let H1 \def H0 in (ex2_ind T (\lambda (t: 
 T).(pr1 t2 t)) (\lambda (t: T).(pr1 t3 t)) (pc1 t1 t3) (\lambda (x: 
 T).(\lambda (H2: (pr1 t2 x)).(\lambda (H3: (pr1 t3 x)).(ex_intro2 T (\lambda 
-(t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t3 t)) x (pr1_u t2 t1 H x H2) H3)))) 
-H1)))))).
+(t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t3 t)) x (pr1_sing t2 t1 H x H2) 
+H3)))) H1)))))).
 
 theorem pc1_refl:
  \forall (t: T).(pc1 t t)
 \def
  \lambda (t: T).(ex_intro2 T (\lambda (t0: T).(pr1 t t0)) (\lambda (t0: 
-T).(pr1 t t0)) t (pr1_r t) (pr1_r t)).
+T).(pr1 t t0)) t (pr1_refl t) (pr1_refl t)).
 
 theorem pc1_s:
  \forall (t2: T).(\forall (t1: T).((pc1 t1 t2) \to (pc1 t2 t1)))
diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc3/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc3/props.ma
index 2d85fb1ca..3bb6c75c6 100644
--- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc3/props.ma
+++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc3/props.ma
@@ -438,3 +438,23 @@ T).(pr3 e t2 t)) (pc3 c (lift h d t1) (lift h d t2)) (\lambda (x: T).(\lambda
 (lift h d x) (pr3_lift c e h d H t1 x H2) (lift h d t2) (pr3_lift c e h d H 
 t2 x H3))))) H1))))))))).
 
+theorem pc3_eta:
+ \forall (c: C).(\forall (t: T).(\forall (w: T).(\forall (u: T).((pc3 c t 
+(THead (Bind Abst) w u)) \to (\forall (v: T).((pc3 c v w) \to (pc3 c (THead 
+(Bind Abst) v (THead (Flat Appl) (TLRef O) (lift (S O) O t))) t)))))))
+\def
+ \lambda (c: C).(\lambda (t: T).(\lambda (w: T).(\lambda (u: T).(\lambda (H: 
+(pc3 c t (THead (Bind Abst) w u))).(\lambda (v: T).(\lambda (H0: (pc3 c v 
+w)).(pc3_t (THead (Bind Abst) w (THead (Flat Appl) (TLRef O) (lift (S O) O 
+(THead (Bind Abst) w u)))) c (THead (Bind Abst) v (THead (Flat Appl) (TLRef 
+O) (lift (S O) O t))) (pc3_head_21 c v w H0 (Bind Abst) (THead (Flat Appl) 
+(TLRef O) (lift (S O) O t)) (THead (Flat Appl) (TLRef O) (lift (S O) O (THead 
+(Bind Abst) w u))) (pc3_thin_dx (CHead c (Bind Abst) v) (lift (S O) O t) 
+(lift (S O) O (THead (Bind Abst) w u)) (pc3_lift (CHead c (Bind Abst) v) c (S 
+O) O (drop_drop (Bind Abst) O c c (drop_refl c) v) t (THead (Bind Abst) w u) 
+H) (TLRef O) Appl)) t (pc3_t (THead (Bind Abst) w u) c (THead (Bind Abst) w 
+(THead (Flat Appl) (TLRef O) (lift (S O) O (THead (Bind Abst) w u)))) 
+(pc3_pr3_r c (THead (Bind Abst) w (THead (Flat Appl) (TLRef O) (lift (S O) O 
+(THead (Bind Abst) w u)))) (THead (Bind Abst) w u) (pr3_eta c w u w (pr3_refl 
+c w))) t (pc3_s c (THead (Bind Abst) w u) t H))))))))).
+
diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr1/defs.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr1/defs.ma
index 2b5d1c3c0..c843e2da1 100644
--- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr1/defs.ma
+++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr1/defs.ma
@@ -19,7 +19,7 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr1/defs".
 include "pr0/defs.ma".
 
 inductive pr1: T \to (T \to Prop) \def
-| pr1_r: \forall (t: T).(pr1 t t)
-| pr1_u: \forall (t2: T).(\forall (t1: T).((pr0 t1 t2) \to (\forall (t3: 
+| pr1_refl: \forall (t: T).(pr1 t t)
+| pr1_sing: \forall (t2: T).(\forall (t1: T).((pr0 t1 t2) \to (\forall (t3: 
 T).((pr1 t2 t3) \to (pr1 t1 t3))))).
 
diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr1/pr1.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr1/pr1.ma
index d0efa9702..cc538838c 100644
--- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr1/pr1.ma
+++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr1/pr1.ma
@@ -28,7 +28,7 @@ t2) \to (ex2 T (\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t2 t)))))))
 (t: T).(\lambda (t2: T).(\forall (t3: T).((pr0 t t3) \to (ex2 T (\lambda (t4: 
 T).(pr1 t2 t4)) (\lambda (t4: T).(pr1 t3 t4))))))) (\lambda (t: T).(\lambda 
 (t2: T).(\lambda (H0: (pr0 t t2)).(ex_intro2 T (\lambda (t3: T).(pr1 t t3)) 
-(\lambda (t3: T).(pr1 t2 t3)) t2 (pr1_pr0 t t2 H0) (pr1_r t2))))) (\lambda 
+(\lambda (t3: T).(pr1 t2 t3)) t2 (pr1_pr0 t t2 H0) (pr1_refl t2))))) (\lambda 
 (t2: T).(\lambda (t3: T).(\lambda (H0: (pr0 t3 t2)).(\lambda (t4: T).(\lambda 
 (_: (pr1 t2 t4)).(\lambda (H2: ((\forall (t5: T).((pr0 t2 t5) \to (ex2 T 
 (\lambda (t: T).(pr1 t4 t)) (\lambda (t: T).(pr1 t5 t))))))).(\lambda (t5: 
@@ -38,7 +38,7 @@ t))) (\lambda (x: T).(\lambda (H4: (pr0 t5 x)).(\lambda (H5: (pr0 t2
 x)).(ex2_ind T (\lambda (t: T).(pr1 t4 t)) (\lambda (t: T).(pr1 x t)) (ex2 T 
 (\lambda (t: T).(pr1 t4 t)) (\lambda (t: T).(pr1 t5 t))) (\lambda (x0: 
 T).(\lambda (H6: (pr1 t4 x0)).(\lambda (H7: (pr1 x x0)).(ex_intro2 T (\lambda 
-(t: T).(pr1 t4 t)) (\lambda (t: T).(pr1 t5 t)) x0 H6 (pr1_u x t5 H4 x0 
+(t: T).(pr1 t4 t)) (\lambda (t: T).(pr1 t5 t)) x0 H6 (pr1_sing x t5 H4 x0 
 H7))))) (H2 x H5))))) (pr0_confluence t3 t5 H3 t2 H0)))))))))) t0 t1 H))).
 
 theorem pr1_confluence:
@@ -49,10 +49,10 @@ t2) \to (ex2 T (\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t2 t)))))))
 (t: T).(\lambda (t2: T).(\forall (t3: T).((pr1 t t3) \to (ex2 T (\lambda (t4: 
 T).(pr1 t2 t4)) (\lambda (t4: T).(pr1 t3 t4))))))) (\lambda (t: T).(\lambda 
 (t2: T).(\lambda (H0: (pr1 t t2)).(ex_intro2 T (\lambda (t3: T).(pr1 t t3)) 
-(\lambda (t3: T).(pr1 t2 t3)) t2 H0 (pr1_r t2))))) (\lambda (t2: T).(\lambda 
-(t3: T).(\lambda (H0: (pr0 t3 t2)).(\lambda (t4: T).(\lambda (_: (pr1 t2 
-t4)).(\lambda (H2: ((\forall (t5: T).((pr1 t2 t5) \to (ex2 T (\lambda (t: 
-T).(pr1 t4 t)) (\lambda (t: T).(pr1 t5 t))))))).(\lambda (t5: T).(\lambda 
+(\lambda (t3: T).(pr1 t2 t3)) t2 H0 (pr1_refl t2))))) (\lambda (t2: 
+T).(\lambda (t3: T).(\lambda (H0: (pr0 t3 t2)).(\lambda (t4: T).(\lambda (_: 
+(pr1 t2 t4)).(\lambda (H2: ((\forall (t5: T).((pr1 t2 t5) \to (ex2 T (\lambda 
+(t: T).(pr1 t4 t)) (\lambda (t: T).(pr1 t5 t))))))).(\lambda (t5: T).(\lambda 
 (H3: (pr1 t3 t5)).(ex2_ind T (\lambda (t: T).(pr1 t5 t)) (\lambda (t: T).(pr1 
 t2 t)) (ex2 T (\lambda (t: T).(pr1 t4 t)) (\lambda (t: T).(pr1 t5 t))) 
 (\lambda (x: T).(\lambda (H4: (pr1 t5 x)).(\lambda (H5: (pr1 t2 x)).(ex2_ind 
diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr1/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr1/props.ma
index 7b7fa2331..08fd5bf1f 100644
--- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr1/props.ma
+++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr1/props.ma
@@ -18,11 +18,17 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr1/props".
 
 include "pr1/defs.ma".
 
+include "pr0/subst1.ma".
+
+include "subst1/props.ma".
+
+include "T/props.ma".
+
 theorem pr1_pr0:
  \forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (pr1 t1 t2)))
 \def
- \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr0 t1 t2)).(pr1_u t2 t1 H t2 
-(pr1_r t2)))).
+ \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr0 t1 t2)).(pr1_sing t2 t1 H 
+t2 (pr1_refl t2)))).
 
 theorem pr1_t:
  \forall (t2: T).(\forall (t1: T).((pr1 t1 t2) \to (\forall (t3: T).((pr1 t2 
@@ -33,8 +39,8 @@ t3) \to (pr1 t1 t3)))))
 (\lambda (t: T).(\lambda (t3: T).(\lambda (H0: (pr1 t t3)).H0))) (\lambda 
 (t0: T).(\lambda (t3: T).(\lambda (H0: (pr0 t3 t0)).(\lambda (t4: T).(\lambda 
 (_: (pr1 t0 t4)).(\lambda (H2: ((\forall (t5: T).((pr1 t4 t5) \to (pr1 t0 
-t5))))).(\lambda (t5: T).(\lambda (H3: (pr1 t4 t5)).(pr1_u t0 t3 H0 t5 (H2 t5 
-H3)))))))))) t1 t2 H))).
+t5))))).(\lambda (t5: T).(\lambda (H3: (pr1 t4 t5)).(pr1_sing t0 t3 H0 t5 (H2 
+t5 H3)))))))))) t1 t2 H))).
 
 theorem pr1_head_1:
  \forall (u1: T).(\forall (u2: T).((pr1 u1 u2) \to (\forall (t: T).(\forall 
@@ -42,9 +48,9 @@ theorem pr1_head_1:
 \def
  \lambda (u1: T).(\lambda (u2: T).(\lambda (H: (pr1 u1 u2)).(\lambda (t: 
 T).(\lambda (k: K).(pr1_ind (\lambda (t0: T).(\lambda (t1: T).(pr1 (THead k 
-t0 t) (THead k t1 t)))) (\lambda (t0: T).(pr1_r (THead k t0 t))) (\lambda 
+t0 t) (THead k t1 t)))) (\lambda (t0: T).(pr1_refl (THead k t0 t))) (\lambda 
 (t2: T).(\lambda (t1: T).(\lambda (H0: (pr0 t1 t2)).(\lambda (t3: T).(\lambda 
-(_: (pr1 t2 t3)).(\lambda (H2: (pr1 (THead k t2 t) (THead k t3 t))).(pr1_u 
+(_: (pr1 t2 t3)).(\lambda (H2: (pr1 (THead k t2 t) (THead k t3 t))).(pr1_sing 
 (THead k t2 t) (THead k t1 t) (pr0_comp t1 t2 H0 t t (pr0_refl t) k) (THead k 
 t3 t) H2))))))) u1 u2 H))))).
 
@@ -54,9 +60,51 @@ theorem pr1_head_2:
 \def
  \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr1 t1 t2)).(\lambda (u: 
 T).(\lambda (k: K).(pr1_ind (\lambda (t: T).(\lambda (t0: T).(pr1 (THead k u 
-t) (THead k u t0)))) (\lambda (t: T).(pr1_r (THead k u t))) (\lambda (t0: 
+t) (THead k u t0)))) (\lambda (t: T).(pr1_refl (THead k u t))) (\lambda (t0: 
 T).(\lambda (t3: T).(\lambda (H0: (pr0 t3 t0)).(\lambda (t4: T).(\lambda (_: 
-(pr1 t0 t4)).(\lambda (H2: (pr1 (THead k u t0) (THead k u t4))).(pr1_u (THead 
-k u t0) (THead k u t3) (pr0_comp u u (pr0_refl u) t3 t0 H0 k) (THead k u t4) 
-H2))))))) t1 t2 H))))).
+(pr1 t0 t4)).(\lambda (H2: (pr1 (THead k u t0) (THead k u t4))).(pr1_sing 
+(THead k u t0) (THead k u t3) (pr0_comp u u (pr0_refl u) t3 t0 H0 k) (THead k 
+u t4) H2))))))) t1 t2 H))))).
+
+theorem pr1_comp:
+ \forall (v: T).(\forall (w: T).((pr1 v w) \to (\forall (t: T).(\forall (u: 
+T).((pr1 t u) \to (\forall (k: K).(pr1 (THead k v t) (THead k w u))))))))
+\def
+ \lambda (v: T).(\lambda (w: T).(\lambda (H: (pr1 v w)).(pr1_ind (\lambda (t: 
+T).(\lambda (t0: T).(\forall (t1: T).(\forall (u: T).((pr1 t1 u) \to (\forall 
+(k: K).(pr1 (THead k t t1) (THead k t0 u)))))))) (\lambda (t: T).(\lambda 
+(t0: T).(\lambda (u: T).(\lambda (H0: (pr1 t0 u)).(\lambda (k: K).(pr1_head_2 
+t0 u H0 t k)))))) (\lambda (t2: T).(\lambda (t1: T).(\lambda (H0: (pr0 t1 
+t2)).(\lambda (t3: T).(\lambda (H1: (pr1 t2 t3)).(\lambda (_: ((\forall (t: 
+T).(\forall (u: T).((pr1 t u) \to (\forall (k: K).(pr1 (THead k t2 t) (THead 
+k t3 u)))))))).(\lambda (t: T).(\lambda (u: T).(\lambda (H3: (pr1 t 
+u)).(\lambda (k: K).(pr1_ind (\lambda (t0: T).(\lambda (t4: T).(pr1 (THead k 
+t1 t0) (THead k t3 t4)))) (\lambda (t0: T).(pr1_head_1 t1 t3 (pr1_sing t2 t1 
+H0 t3 H1) t0 k)) (\lambda (t0: T).(\lambda (t4: T).(\lambda (H4: (pr0 t4 
+t0)).(\lambda (t5: T).(\lambda (_: (pr1 t0 t5)).(\lambda (H6: (pr1 (THead k 
+t1 t0) (THead k t3 t5))).(pr1_sing (THead k t1 t0) (THead k t1 t4) (pr0_comp 
+t1 t1 (pr0_refl t1) t4 t0 H4 k) (THead k t3 t5) H6))))))) t u H3))))))))))) v 
+w H))).
+
+theorem pr1_eta:
+ \forall (w: T).(\forall (u: T).(let t \def (THead (Bind Abst) w u) in 
+(\forall (v: T).((pr1 v w) \to (pr1 (THead (Bind Abst) v (THead (Flat Appl) 
+(TLRef O) (lift (S O) O t))) t)))))
+\def
+ \lambda (w: T).(\lambda (u: T).(let t \def (THead (Bind Abst) w u) in 
+(\lambda (v: T).(\lambda (H: (pr1 v w)).(eq_ind_r T (THead (Bind Abst) (lift 
+(S O) O w) (lift (S O) (S O) u)) (\lambda (t0: T).(pr1 (THead (Bind Abst) v 
+(THead (Flat Appl) (TLRef O) t0)) (THead (Bind Abst) w u))) (pr1_comp v w H 
+(THead (Flat Appl) (TLRef O) (THead (Bind Abst) (lift (S O) O w) (lift (S O) 
+(S O) u))) u (pr1_sing (THead (Bind Abbr) (TLRef O) (lift (S O) (S O) u)) 
+(THead (Flat Appl) (TLRef O) (THead (Bind Abst) (lift (S O) O w) (lift (S O) 
+(S O) u))) (pr0_beta (lift (S O) O w) (TLRef O) (TLRef O) (pr0_refl (TLRef 
+O)) (lift (S O) (S O) u) (lift (S O) (S O) u) (pr0_refl (lift (S O) (S O) 
+u))) u (pr1_sing (THead (Bind Abbr) (TLRef O) (lift (S O) O u)) (THead (Bind 
+Abbr) (TLRef O) (lift (S O) (S O) u)) (pr0_delta1 (TLRef O) (TLRef O) 
+(pr0_refl (TLRef O)) (lift (S O) (S O) u) (lift (S O) (S O) u) (pr0_refl 
+(lift (S O) (S O) u)) (lift (S O) O u) (subst1_lift_S u O O (le_n O))) u 
+(pr1_pr0 (THead (Bind Abbr) (TLRef O) (lift (S O) O u)) u (pr0_zeta Abbr 
+not_abbr_abst u u (pr0_refl u) (TLRef O))))) (Bind Abst)) (lift (S O) O 
+(THead (Bind Abst) w u)) (lift_bind Abst w u (S O) O)))))).
 
diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/props.ma
index 6916d8d40..8bccde83f 100644
--- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/props.ma
+++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/props.ma
@@ -16,10 +16,12 @@
 
 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/props".
 
-include "pr3/defs.ma".
+include "pr3/pr1.ma".
 
 include "pr2/props.ma".
 
+include "pr1/props.ma".
+
 theorem clear_pr3_trans:
  \forall (c2: C).(\forall (t1: T).(\forall (t2: T).((pr3 c2 t1 t2) \to 
 (\forall (c1: C).((clear c1 c2) \to (pr3 c1 t1 t2))))))
@@ -387,3 +389,27 @@ t4)).(\lambda (H3: (pr3 c (lift h d t0) (lift h d t4))).(pr3_sing c (lift h d
 t0) (lift h d t3) (pr2_lift c e h d H t3 t0 H1) (lift h d t4) H3))))))) t1 t2 
 H0)))))))).
 
+theorem pr3_eta:
+ \forall (c: C).(\forall (w: T).(\forall (u: T).(let t \def (THead (Bind 
+Abst) w u) in (\forall (v: T).((pr3 c v w) \to (pr3 c (THead (Bind Abst) v 
+(THead (Flat Appl) (TLRef O) (lift (S O) O t))) t))))))
+\def
+ \lambda (c: C).(\lambda (w: T).(\lambda (u: T).(let t \def (THead (Bind 
+Abst) w u) in (\lambda (v: T).(\lambda (H: (pr3 c v w)).(eq_ind_r T (THead 
+(Bind Abst) (lift (S O) O w) (lift (S O) (S O) u)) (\lambda (t0: T).(pr3 c 
+(THead (Bind Abst) v (THead (Flat Appl) (TLRef O) t0)) (THead (Bind Abst) w 
+u))) (pr3_head_12 c v w H (Bind Abst) (THead (Flat Appl) (TLRef O) (THead 
+(Bind Abst) (lift (S O) O w) (lift (S O) (S O) u))) u (pr3_pr1 (THead (Flat 
+Appl) (TLRef O) (THead (Bind Abst) (lift (S O) O w) (lift (S O) (S O) u))) u 
+(pr1_sing (THead (Bind Abbr) (TLRef O) (lift (S O) (S O) u)) (THead (Flat 
+Appl) (TLRef O) (THead (Bind Abst) (lift (S O) O w) (lift (S O) (S O) u))) 
+(pr0_beta (lift (S O) O w) (TLRef O) (TLRef O) (pr0_refl (TLRef O)) (lift (S 
+O) (S O) u) (lift (S O) (S O) u) (pr0_refl (lift (S O) (S O) u))) u (pr1_sing 
+(THead (Bind Abbr) (TLRef O) (lift (S O) O u)) (THead (Bind Abbr) (TLRef O) 
+(lift (S O) (S O) u)) (pr0_delta1 (TLRef O) (TLRef O) (pr0_refl (TLRef O)) 
+(lift (S O) (S O) u) (lift (S O) (S O) u) (pr0_refl (lift (S O) (S O) u)) 
+(lift (S O) O u) (subst1_lift_S u O O (le_n O))) u (pr1_pr0 (THead (Bind 
+Abbr) (TLRef O) (lift (S O) O u)) u (pr0_zeta Abbr not_abbr_abst u u 
+(pr0_refl u) (TLRef O))))) (CHead c (Bind Abst) w))) (lift (S O) O (THead 
+(Bind Abst) w u)) (lift_bind Abst w u (S O) O))))))).
+
diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/s/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/s/props.ma
index 1c062bdad..01803231b 100644
--- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/s/props.ma
+++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/s/props.ma
@@ -99,6 +99,14 @@ B).(\lambda (i: nat).(\lambda (j: nat).(\lambda (H: (eq nat (s (Bind b) i) (s
 (Bind b) j))).(eq_add_S i j H))))) (\lambda (f: F).(\lambda (i: nat).(\lambda 
 (j: nat).(\lambda (H: (eq nat (s (Flat f) i) (s (Flat f) j))).H)))) k).
 
+theorem s_inc:
+ \forall (k: K).(\forall (i: nat).(le i (s k i)))
+\def
+ \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(le i (s k0 i)))) 
+(\lambda (b: B).(\lambda (i: nat).(le_S_n i (s (Bind b) i) (le_S (S i) (s 
+(Bind b) i) (le_n (s (Bind b) i)))))) (\lambda (f: F).(\lambda (i: nat).(le_n 
+(s (Flat f) i)))) k).
+
 theorem s_arith0:
  \forall (k: K).(\forall (i: nat).(eq nat (minus (s k i) (s k O)) i))
 \def
diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst1/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst1/props.ma
index 02251bec2..525424b43 100644
--- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst1/props.ma
+++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst1/props.ma
@@ -109,3 +109,58 @@ d) x0)) (\lambda (t2: T).(subst1 d u (THead k t t0) t2)) (subst1_head u t
 (lift (S O) d x) d H2 k t0 (lift (S O) (s k d) x0) H4) (lift (S O) d (THead k 
 x x0)) (lift_head k x x0 (S O) d))))) H3))))) H1))))))))) t1)).
 
+theorem subst1_lift_S:
+ \forall (u: T).(\forall (i: nat).(\forall (h: nat).((le h i) \to (subst1 i 
+(TLRef h) (lift (S h) (S i) u) (lift (S h) i u)))))
+\def
+ \lambda (u: T).(T_ind (\lambda (t: T).(\forall (i: nat).(\forall (h: 
+nat).((le h i) \to (subst1 i (TLRef h) (lift (S h) (S i) t) (lift (S h) i 
+t)))))) (\lambda (n: nat).(\lambda (i: nat).(\lambda (h: nat).(\lambda (_: 
+(le h i)).(eq_ind_r T (TSort n) (\lambda (t: T).(subst1 i (TLRef h) t (lift 
+(S h) i (TSort n)))) (eq_ind_r T (TSort n) (\lambda (t: T).(subst1 i (TLRef 
+h) (TSort n) t)) (subst1_refl i (TLRef h) (TSort n)) (lift (S h) i (TSort n)) 
+(lift_sort n (S h) i)) (lift (S h) (S i) (TSort n)) (lift_sort n (S h) (S 
+i))))))) (\lambda (n: nat).(\lambda (i: nat).(\lambda (h: nat).(\lambda (H: 
+(le h i)).(lt_eq_gt_e n i (subst1 i (TLRef h) (lift (S h) (S i) (TLRef n)) 
+(lift (S h) i (TLRef n))) (\lambda (H0: (lt n i)).(eq_ind_r T (TLRef n) 
+(\lambda (t: T).(subst1 i (TLRef h) t (lift (S h) i (TLRef n)))) (eq_ind_r T 
+(TLRef n) (\lambda (t: T).(subst1 i (TLRef h) (TLRef n) t)) (subst1_refl i 
+(TLRef h) (TLRef n)) (lift (S h) i (TLRef n)) (lift_lref_lt n (S h) i H0)) 
+(lift (S h) (S i) (TLRef n)) (lift_lref_lt n (S h) (S i) (le_S (S n) i H0)))) 
+(\lambda (H0: (eq nat n i)).(let H1 \def (eq_ind_r nat i (\lambda (n0: 
+nat).(le h n0)) H n H0) in (eq_ind nat n (\lambda (n0: nat).(subst1 n0 (TLRef 
+h) (lift (S h) (S n0) (TLRef n)) (lift (S h) n0 (TLRef n)))) (eq_ind_r T 
+(TLRef n) (\lambda (t: T).(subst1 n (TLRef h) t (lift (S h) n (TLRef n)))) 
+(eq_ind_r T (TLRef (plus n (S h))) (\lambda (t: T).(subst1 n (TLRef h) (TLRef 
+n) t)) (eq_ind nat (S (plus n h)) (\lambda (n0: nat).(subst1 n (TLRef h) 
+(TLRef n) (TLRef n0))) (eq_ind_r nat (plus h n) (\lambda (n0: nat).(subst1 n 
+(TLRef h) (TLRef n) (TLRef (S n0)))) (eq_ind nat (plus h (S n)) (\lambda (n0: 
+nat).(subst1 n (TLRef h) (TLRef n) (TLRef n0))) (eq_ind T (lift (S n) O 
+(TLRef h)) (\lambda (t: T).(subst1 n (TLRef h) (TLRef n) t)) (subst1_single n 
+(TLRef h) (TLRef n) (lift (S n) O (TLRef h)) (subst0_lref (TLRef h) n)) 
+(TLRef (plus h (S n))) (lift_lref_ge h (S n) O (le_O_n h))) (S (plus h n)) 
+(sym_eq nat (S (plus h n)) (plus h (S n)) (plus_n_Sm h n))) (plus n h) 
+(plus_comm n h)) (plus n (S h)) (plus_n_Sm n h)) (lift (S h) n (TLRef n)) 
+(lift_lref_ge n (S h) n (le_n n))) (lift (S h) (S n) (TLRef n)) (lift_lref_lt 
+n (S h) (S n) (le_n (S n)))) i H0))) (\lambda (H0: (lt i n)).(eq_ind_r T 
+(TLRef (plus n (S h))) (\lambda (t: T).(subst1 i (TLRef h) t (lift (S h) i 
+(TLRef n)))) (eq_ind_r T (TLRef (plus n (S h))) (\lambda (t: T).(subst1 i 
+(TLRef h) (TLRef (plus n (S h))) t)) (subst1_refl i (TLRef h) (TLRef (plus n 
+(S h)))) (lift (S h) i (TLRef n)) (lift_lref_ge n (S h) i (le_S_n i n (le_S 
+(S i) n H0)))) (lift (S h) (S i) (TLRef n)) (lift_lref_ge n (S h) (S i) 
+H0)))))))) (\lambda (k: K).(\lambda (t: T).(\lambda (H: ((\forall (i: 
+nat).(\forall (h: nat).((le h i) \to (subst1 i (TLRef h) (lift (S h) (S i) t) 
+(lift (S h) i t))))))).(\lambda (t0: T).(\lambda (H0: ((\forall (i: 
+nat).(\forall (h: nat).((le h i) \to (subst1 i (TLRef h) (lift (S h) (S i) 
+t0) (lift (S h) i t0))))))).(\lambda (i: nat).(\lambda (h: nat).(\lambda (H1: 
+(le h i)).(eq_ind_r T (THead k (lift (S h) (S i) t) (lift (S h) (s k (S i)) 
+t0)) (\lambda (t1: T).(subst1 i (TLRef h) t1 (lift (S h) i (THead k t t0)))) 
+(eq_ind_r T (THead k (lift (S h) i t) (lift (S h) (s k i) t0)) (\lambda (t1: 
+T).(subst1 i (TLRef h) (THead k (lift (S h) (S i) t) (lift (S h) (s k (S i)) 
+t0)) t1)) (subst1_head (TLRef h) (lift (S h) (S i) t) (lift (S h) i t) i (H i 
+h H1) k (lift (S h) (s k (S i)) t0) (lift (S h) (s k i) t0) (eq_ind_r nat (S 
+(s k i)) (\lambda (n: nat).(subst1 (s k i) (TLRef h) (lift (S h) n t0) (lift 
+(S h) (s k i) t0))) (H0 (s k i) h (le_trans h i (s k i) H1 (s_inc k i))) (s k 
+(S i)) (s_S k i))) (lift (S h) i (THead k t t0)) (lift_head k t t0 (S h) i)) 
+(lift (S h) (S i) (THead k t t0)) (lift_head k t t0 (S h) (S i))))))))))) u).
+
diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma
index b632ec9d4..60888280b 100644
--- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma
+++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma
@@ -256,14 +256,14 @@ include "pr2/subst1.ma".
 
 include "pr3/defs.ma".
 
+include "pr3/pr1.ma".
+
 include "pr3/props.ma".
 
 include "pr3/fwd.ma".
 
 include "pr3/wcpr0.ma".
 
-include "pr3/pr1.ma".
-
 include "pr3/pr3.ma".
 
 include "pr3/subst1.ma".
@@ -356,6 +356,10 @@ include "ty3/defs.ma".
 
 include "ty3/fwd.ma".
 
+include "ex1/defs.ma".
+
+include "ex1/props.ma".
+
 include "ty3/props.ma".
 
 include "ty3/fsubst0.ma".