matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/fwd.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/csubt/fwd".
  18
  19 include "csubt/defs.ma".
  20
  21 axiom csubt_gen_abbr:
  22  \forall (g: G).(\forall (e1: C).(\forall (c2: C).(\forall (v: T).((csubt g
  23 (CHead e1 (Bind Abbr) v) c2) \to (ex2 C (\lambda (e2: C).(eq C c2 (CHead e2
  24 (Bind Abbr) v))) (\lambda (e2: C).(csubt g e1 e2)))))))
  25 .
  26
  27 axiom csubt_gen_abst:
  28  \forall (g: G).(\forall (e1: C).(\forall (c2: C).(\forall (v1: T).((csubt g
  29 (CHead e1 (Bind Abst) v1) c2) \to (or (ex2 C (\lambda (e2: C).(eq C c2 (CHead
  30 e2 (Bind Abst) v1))) (\lambda (e2: C).(csubt g e1 e2))) (ex3_2 C T (\lambda
  31 (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2:
  32 C).(\lambda (_: T).(csubt g e1 e2))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g
  33 e2 v2 v1)))))))))
  34 .
  35
  36 axiom csubt_gen_bind:
  37  \forall (g: G).(\forall (b1: B).(\forall (e1: C).(\forall (c2: C).(\forall
  38 (v1: T).((csubt g (CHead e1 (Bind b1) v1) c2) \to (ex2_3 B C T (\lambda (b2:
  39 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind b2) v2)))))
  40 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csubt g e1 e2))))))))))
  41 .
  42