From 067c2f773a1053cab1d6cd25a92e0bcc1763c305 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 24 Jan 2007 19:44:22 +0000 Subject: [PATCH] tactics.mli: regenerated LambdaDelta: regenerated with some new theorems --- components/tactics/tactics.mli | 2 +- .../Level-1/LambdaDelta/ex1/defs.ma | 31 + .../Level-1/LambdaDelta/ex1/props.ma | 540 ++++++++++++++++++ .../Level-1/LambdaDelta/pc1/props.ma | 10 +- .../Level-1/LambdaDelta/pc3/props.ma | 20 + .../Level-1/LambdaDelta/pr1/defs.ma | 4 +- .../Level-1/LambdaDelta/pr1/pr1.ma | 12 +- .../Level-1/LambdaDelta/pr1/props.ma | 68 ++- .../Level-1/LambdaDelta/pr3/props.ma | 28 +- .../Level-1/LambdaDelta/s/props.ma | 8 + .../Level-1/LambdaDelta/subst1/props.ma | 55 ++ .../Level-1/LambdaDelta/theory.ma | 8 +- 12 files changed, 759 insertions(+), 27 deletions(-) create mode 100644 matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ex1/defs.ma create mode 100644 matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ex1/props.ma 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". -- 2.39.2