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/sc3/arity".
19 include "ceqc/props.ma".
22 \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a: A).((arity g c t
23 a) \to (sc3 g a c t)))))
25 \lambda (g: G).(\lambda (c: C).(\lambda (t: T).(\lambda (a: A).(\lambda (H:
26 (arity g c t a)).(arity_ind g (\lambda (c0: C).(\lambda (t0: T).(\lambda (a0:
27 A).(sc3 g a0 c0 t0)))) (\lambda (c0: C).(\lambda (n: nat).(conj (arity g c0
28 (TSort n) (ASort O n)) (sn3 c0 (TSort n)) (arity_sort g c0 n) (sn3_nf2 c0
29 (TSort n) (nf2_sort c0 n))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (u:
30 T).(\lambda (i: nat).(\lambda (H0: (getl i c0 (CHead d (Bind Abbr)
31 u))).(\lambda (a0: A).(\lambda (_: (arity g d u a0)).(\lambda (H2: (sc3 g a0
32 d u)).(let H_y \def (sc3_abbr g a0 TNil) in (H_y i d u c0 (sc3_lift g a0 d u
33 H2 c0 (S i) O (getl_drop Abbr c0 d u i H0)) H0)))))))))) (\lambda (c0:
34 C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H0: (getl i c0
35 (CHead d (Bind Abst) u))).(\lambda (a0: A).(\lambda (H1: (arity g d u (asucc
36 g a0))).(\lambda (_: (sc3 g (asucc g a0) d u)).(let H3 \def (sc3_abst g a0
37 TNil) in (H3 c0 i (arity_abst g c0 d u i H0 a0 H1) (nf2_lref_abst c0 d u i
38 H0) I)))))))))) (\lambda (b: B).(\lambda (H0: (not (eq B b Abst))).(\lambda
39 (c0: C).(\lambda (u: T).(\lambda (a1: A).(\lambda (_: (arity g c0 u
40 a1)).(\lambda (H2: (sc3 g a1 c0 u)).(\lambda (t0: T).(\lambda (a2:
41 A).(\lambda (_: (arity g (CHead c0 (Bind b) u) t0 a2)).(\lambda (H4: (sc3 g
42 a2 (CHead c0 (Bind b) u) t0)).(let H_y \def (sc3_bind g b H0 a1 a2 TNil) in
43 (H_y c0 u t0 H4 H2))))))))))))) (\lambda (c0: C).(\lambda (u: T).(\lambda
44 (a1: A).(\lambda (H0: (arity g c0 u (asucc g a1))).(\lambda (H1: (sc3 g
45 (asucc g a1) c0 u)).(\lambda (t0: T).(\lambda (a2: A).(\lambda (H2: (arity g
46 (CHead c0 (Bind Abst) u) t0 a2)).(\lambda (H3: (sc3 g a2 (CHead c0 (Bind
47 Abst) u) t0)).(conj (arity g c0 (THead (Bind Abst) u t0) (AHead a1 a2))
48 (\forall (d: C).(\forall (w: T).((sc3 g a1 d w) \to (\forall (is:
49 PList).((drop1 is d c0) \to (sc3 g a2 d (THead (Flat Appl) w (lift1 is (THead
50 (Bind Abst) u t0))))))))) (arity_head g c0 u a1 H0 t0 a2 H2) (\lambda (d:
51 C).(\lambda (w: T).(\lambda (H4: (sc3 g a1 d w)).(\lambda (is:
52 PList).(\lambda (H5: (drop1 is d c0)).(let H6 \def (sc3_appl g a1 a2 TNil) in
53 (eq_ind_r T (THead (Bind Abst) (lift1 is u) (lift1 (Ss is) t0)) (\lambda (t1:
54 T).(sc3 g a2 d (THead (Flat Appl) w t1))) (H6 d w (lift1 (Ss is) t0) (let H_y
55 \def (sc3_bind g Abbr (\lambda (H7: (eq B Abbr Abst)).(not_abbr_abst H7)) a1
56 a2 TNil) in (H_y d w (lift1 (Ss is) t0) (let H7 \def (sc3_ceqc_trans g a2
57 TNil) in (H7 (CHead d (Bind Abst) (lift1 is u)) (lift1 (Ss is) t0) (sc3_lift1
58 g (CHead c0 (Bind Abst) u) a2 (Ss is) (CHead d (Bind Abst) (lift1 is u)) t0
59 H3 (drop1_skip_bind Abst c0 is d u H5)) (CHead d (Bind Abbr) w) (or_intror
60 (csubc g (CHead d (Bind Abbr) w) (CHead d (Bind Abst) (lift1 is u))) (csubc g
61 (CHead d (Bind Abst) (lift1 is u)) (CHead d (Bind Abbr) w)) (csubc_abst g d d
62 (csubc_refl g d) (lift1 is u) a1 (sc3_lift1 g c0 (asucc g a1) is d u H1 H5) w
63 H4)))) H4)) H4 (lift1 is u) (sc3_lift1 g c0 (asucc g a1) is d u H1 H5))
64 (lift1 is (THead (Bind Abst) u t0)) (lift1_bind Abst is u
65 t0)))))))))))))))))) (\lambda (c0: C).(\lambda (u: T).(\lambda (a1:
66 A).(\lambda (_: (arity g c0 u a1)).(\lambda (H1: (sc3 g a1 c0 u)).(\lambda
67 (t0: T).(\lambda (a2: A).(\lambda (_: (arity g c0 t0 (AHead a1 a2))).(\lambda
68 (H3: (sc3 g (AHead a1 a2) c0 t0)).(let H4 \def H3 in (and_ind (arity g c0 t0
69 (AHead a1 a2)) (\forall (d: C).(\forall (w: T).((sc3 g a1 d w) \to (\forall
70 (is: PList).((drop1 is d c0) \to (sc3 g a2 d (THead (Flat Appl) w (lift1 is
71 t0)))))))) (sc3 g a2 c0 (THead (Flat Appl) u t0)) (\lambda (_: (arity g c0 t0
72 (AHead a1 a2))).(\lambda (H6: ((\forall (d: C).(\forall (w: T).((sc3 g a1 d
73 w) \to (\forall (is: PList).((drop1 is d c0) \to (sc3 g a2 d (THead (Flat
74 Appl) w (lift1 is t0)))))))))).(let H_y \def (H6 c0 u H1 PNil) in (H_y
75 (drop1_nil c0))))) H4))))))))))) (\lambda (c0: C).(\lambda (u: T).(\lambda
76 (a0: A).(\lambda (_: (arity g c0 u (asucc g a0))).(\lambda (H1: (sc3 g (asucc
77 g a0) c0 u)).(\lambda (t0: T).(\lambda (_: (arity g c0 t0 a0)).(\lambda (H3:
78 (sc3 g a0 c0 t0)).(let H_y \def (sc3_cast g a0 TNil) in (H_y c0 u H1 t0
79 H3)))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (a1: A).(\lambda (_:
80 (arity g c0 t0 a1)).(\lambda (H1: (sc3 g a1 c0 t0)).(\lambda (a2: A).(\lambda
81 (H2: (leq g a1 a2)).(sc3_repl g a1 c0 t0 H1 a2 H2)))))))) c t a H))))).