1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/getl/getl".
19 include "getl/drop.ma".
21 include "getl/clear.ma".
24 \forall (i: nat).(\forall (a: C).(\forall (c: C).((getl i c a) \to (\forall
25 (e: C).(\forall (h: nat).((getl h c e) \to ((le h i) \to (getl (minus i h) e
28 \lambda (i: nat).(\lambda (a: C).(\lambda (c: C).(\lambda (H: (getl i c
29 a)).(\lambda (e: C).(\lambda (h: nat).(\lambda (H0: (getl h c e)).(\lambda
30 (H1: (le h i)).(let H2 \def (getl_gen_all c e h H0) in (ex2_ind C (\lambda
31 (e0: C).(drop h O c e0)) (\lambda (e0: C).(clear e0 e)) (getl (minus i h) e
32 a) (\lambda (x: C).(\lambda (H3: (drop h O c x)).(\lambda (H4: (clear x
33 e)).(getl_clear_conf (minus i h) x a (getl_drop_conf_ge i a c H x h O H3 H1)
37 \forall (i: nat).(\forall (c1: C).(\forall (c2: C).(\forall (h: nat).((getl
38 h c1 c2) \to (\forall (e2: C).((getl i c2 e2) \to (getl (plus i h) c1
41 \lambda (i: nat).(\lambda (c1: C).(\lambda (c2: C).(\lambda (h:
42 nat).(\lambda (H: (getl h c1 c2)).(\lambda (e2: C).(\lambda (H0: (getl i c2
43 e2)).(let H1 \def (getl_gen_all c2 e2 i H0) in (ex2_ind C (\lambda (e:
44 C).(drop i O c2 e)) (\lambda (e: C).(clear e e2)) (getl (plus i h) c1 e2)
45 (\lambda (x: C).(\lambda (H2: (drop i O c2 x)).(\lambda (H3: (clear x
46 e2)).((match i in nat return (\lambda (n: nat).((drop n O c2 x) \to (getl
47 (plus n h) c1 e2))) with [O \Rightarrow (\lambda (H4: (drop O O c2 x)).(let
48 H5 \def (eq_ind_r C x (\lambda (c: C).(clear c e2)) H3 c2 (drop_gen_refl c2 x
49 H4)) in (getl_clear_trans (plus O h) c1 c2 H e2 H5))) | (S n) \Rightarrow
50 (\lambda (H4: (drop (S n) O c2 x)).(let H_y \def (getl_drop_trans c1 c2 h H x
51 n H4) in (getl_intro (plus (S n) h) c1 e2 x H_y H3)))]) H2)))) H1)))))))).