helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/arity.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/arity".
  18
  19 include "ceqc/props.ma".
  20
  21 theorem sc3_arity:
  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)))))
  24 \def
  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))))).
  82