(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/blt/defs".
-
include "preamble.ma".
definition blt:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/blt/props".
-
include "blt/defs.ma".
theorem lt_blt:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/definitions".
-
include "types/defs.ma".
include "blt/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith".
-
include "preamble.ma".
theorem nat_dec:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics".
-
include "preamble.ma".
theorem insert_eq:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/plist/defs".
-
include "preamble.ma".
inductive PList: Set \def
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/plist/props".
-
include "plist/defs.ma".
theorem papp_ss:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/spare".
-
include "theory.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/theory".
-
include "ext/tactics.ma".
include "ext/arith.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/types/defs".
-
include "preamble.ma".
inductive and3 (P0: Prop) (P1: Prop) (P2: Prop): Prop \def
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/types/props".
-
include "types/defs.ma".
theorem ex2_sym:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/A/defs".
-
include "preamble.ma".
inductive A: Set \def
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/C/defs".
-
include "T/defs.ma".
inductive C: Set \def
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/C/props".
-
include "C/defs.ma".
include "T/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/G/defs".
-
include "preamble.ma".
record G : Set \def {
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/dec".
-
include "T/defs.ma".
theorem terms_props__bind_dec:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs".
-
include "preamble.ma".
inductive B: Set \def
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/props".
-
include "T/defs.ma".
theorem not_abbr_abst:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/aplus/defs".
-
include "asucc/defs.ma".
definition aplus:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/aplus/props".
-
include "aplus/defs.ma".
include "next_plus/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/aprem/defs".
-
include "A/defs.ma".
inductive aprem: nat \to (A \to (A \to Prop)) \def
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/aprem/props".
-
include "aprem/defs.ma".
include "leq/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/aprem".
-
include "arity/props.ma".
include "arity/cimp.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/cimp".
-
include "arity/defs.ma".
include "cimp/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/defs".
-
include "leq/defs.ma".
include "getl/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/fwd".
-
include "arity/defs.ma".
include "leq/asucc.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/lift1".
-
include "arity/props.ma".
include "drop1/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/pr3".
-
include "csuba/arity.ma".
include "pr3/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/props".
-
include "arity/fwd.ma".
theorem node_inh:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/subst0".
-
include "arity/props.ma".
include "fsubst0/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/asucc/defs".
-
include "A/defs.ma".
include "G/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/asucc/fwd".
-
include "asucc/defs.ma".
theorem asucc_gen_sort:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/cimp/defs".
-
include "getl/defs.ma".
definition cimp:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/cimp/props".
-
include "cimp/defs.ma".
include "getl/getl.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/clear/defs".
-
include "C/defs.ma".
inductive clear: C \to (C \to Prop) \def
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/clear/drop".
-
include "clear/fwd.ma".
include "drop/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/clear/fwd".
-
include "clear/defs.ma".
theorem clear_gen_sort:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/clear/props".
-
include "clear/fwd.ma".
theorem clear_clear:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/clen/defs".
-
include "C/defs.ma".
include "s/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/clen/getl".
-
include "clen/defs.ma".
include "getl/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/cnt/defs".
-
include "T/defs.ma".
inductive cnt: T \to Prop \def
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/cnt/props".
-
include "cnt/defs.ma".
include "lift/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/arity".
-
include "csuba/getl.ma".
include "csuba/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/clear".
-
include "csuba/defs.ma".
include "clear/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/defs".
-
include "arity/defs.ma".
inductive csuba (g: G): C \to (C \to Prop) \def
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/drop".
-
include "csuba/fwd.ma".
include "drop/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/fwd".
-
include "csuba/defs.ma".
theorem csuba_gen_abbr:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/getl".
-
include "csuba/drop.ma".
include "csuba/clear.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/props".
-
include "csuba/defs.ma".
theorem csuba_refl:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/arity".
-
include "csubc/csuba.ma".
include "arity/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/clear".
-
include "csubc/defs.ma".
theorem csubc_clear_conf:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/csuba".
-
include "csubc/defs.ma".
include "sc3/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/defs".
-
include "sc3/defs.ma".
inductive csubc (g: G): C \to (C \to Prop) \def
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/drop".
-
include "csubc/defs.ma".
include "sc3/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/drop1".
-
include "csubc/drop.ma".
theorem drop1_csubc_trans:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/getl".
-
include "csubc/drop.ma".
include "csubc/clear.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/props".
-
include "csubc/defs.ma".
include "sc3/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst0/clear".
-
include "csubst0/fwd.ma".
include "clear/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst0/defs".
-
include "subst0/defs.ma".
include "C/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst0/drop".
-
include "csubst0/fwd.ma".
include "drop/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst0/fwd".
-
include "csubst0/defs.ma".
theorem csubst0_gen_sort:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst0/getl".
-
include "csubst0/clear.ma".
include "csubst0/drop.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst0/props".
-
include "csubst0/defs.ma".
theorem csubst0_snd_bind:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst1/defs".
-
include "csubst0/defs.ma".
inductive csubst1 (i: nat) (v: T) (c1: C): C \to Prop \def
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst1/fwd".
-
include "csubst1/defs.ma".
include "csubst0/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst1/getl".
-
include "csubst1/props.ma".
include "csubst0/getl.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst1/props".
-
include "csubst1/defs.ma".
include "subst1/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/clear".
-
include "csubt/defs.ma".
include "clear/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/defs".
-
include "ty3/defs.ma".
inductive csubt (g: G): C \to (C \to Prop) \def
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/drop".
-
include "csubt/defs.ma".
include "drop/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/fwd".
-
include "csubt/defs.ma".
theorem csubt_inv_coq:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/getl".
-
include "csubt/fwd.ma".
include "csubt/clear.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/pc3".
-
include "csubt/getl.ma".
include "pc3/left.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/props".
-
include "csubt/defs.ma".
theorem csubt_refl:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/ty3".
-
include "csubt/pc3.ma".
include "csubt/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/definitions".
-
include "tlt/defs.ma".
include "iso/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/drop/defs".
-
include "C/defs.ma".
include "lift/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/drop/fwd".
-
include "drop/defs.ma".
theorem drop_gen_sort:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/drop/props".
-
include "drop/fwd.ma".
include "lift/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/drop1/defs".
-
include "drop/defs.ma".
include "lift1/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/drop1/getl".
-
include "drop1/defs.ma".
include "getl/drop.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/drop1/props".
-
include "drop1/defs.ma".
include "drop/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ex0/defs".
-
include "A/defs.ma".
include "G/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ex0/props".
-
include "ex0/defs.ma".
include "leq/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ex1/defs".
-
include "C/defs.ma".
definition ex1_c:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ex1/props".
-
include "ex1/defs.ma".
include "ty3/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ex2/defs".
-
include "C/defs.ma".
definition ex2_c:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ex2/props".
-
include "ex2/defs.ma".
include "nf2/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/flt/defs".
-
include "C/defs.ma".
definition fweight:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/flt/props".
-
include "flt/defs.ma".
include "C/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/fsubst0/defs".
-
include "csubst0/defs.ma".
include "subst0/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/fsubst0/fwd".
-
include "fsubst0/defs.ma".
theorem fsubst0_gen_base:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/clear".
-
include "getl/props.ma".
include "clear/drop.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/dec".
-
include "getl/props.ma".
theorem getl_dec:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/defs".
-
include "drop/defs.ma".
include "clear/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/drop".
-
include "getl/props.ma".
include "clear/drop.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/flt".
-
include "getl/fwd.ma".
include "clear/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/fwd".
-
include "getl/defs.ma".
include "drop/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/getl".
-
include "getl/drop.ma".
include "getl/clear.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/props".
-
include "getl/fwd.ma".
include "drop/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/iso/defs".
-
include "T/defs.ma".
inductive iso: T \to (T \to Prop) \def
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/iso/fwd".
-
include "iso/defs.ma".
include "tlist/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/iso/props".
-
include "iso/fwd.ma".
theorem iso_refl:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/leq/asucc".
-
include "leq/props.ma".
include "aplus/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/leq/defs".
-
include "aplus/defs.ma".
inductive leq (g: G): A \to (A \to Prop) \def
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/leq/fwd".
-
include "leq/defs.ma".
theorem leq_gen_sort:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/leq/props".
-
include "leq/defs.ma".
include "aplus/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift/defs".
-
include "T/defs.ma".
include "tlist/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift/fwd".
-
include "lift/defs.ma".
theorem lift_sort:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift/props".
-
include "tlist/defs.ma".
include "lift/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift/tlt".
-
include "lift/fwd.ma".
include "tlt/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift1/defs".
-
include "lift/defs.ma".
definition trans:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift1/fwd".
-
include "lift1/defs.ma".
include "lift/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift1/props".
-
include "lift1/defs.ma".
include "lift/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/llt/defs".
-
include "A/defs.ma".
definition lweight:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/llt/props".
-
include "llt/defs.ma".
include "leq/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/next_plus/defs".
-
include "G/defs.ma".
definition next_plus:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/next_plus/props".
-
include "next_plus/defs.ma".
theorem next_plus_assoc:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/arity".
-
include "nf2/fwd.ma".
include "arity/subst0.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/dec".
-
include "nf2/defs.ma".
include "pr2/clen.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/defs".
-
include "pr2/defs.ma".
definition nf2:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/fwd".
-
include "nf2/defs.ma".
include "pr2/clen.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/iso".
-
include "nf2/pr3.ma".
include "pr3/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/lift1".
-
include "nf2/props.ma".
include "drop1/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/pr3".
-
include "nf2/defs.ma".
include "pr3/pr3.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/props".
-
include "nf2/defs.ma".
include "pr2/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc1/defs".
-
include "pr1/defs.ma".
definition pc1:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc1/props".
-
include "pc1/defs.ma".
include "pr1/pr1.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/dec".
-
include "ty3/arity_props.ma".
include "ty3/pr3.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/defs".
-
include "pr3/defs.ma".
definition pc3:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/fsubst0".
-
include "pc3/left.ma".
include "fsubst0/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/fwd".
-
include "pc3/props.ma".
include "pr3/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/left".
-
include "pc3/props.ma".
theorem pc3_ind_left__pc3_left_pr3:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/nf2".
-
include "pc3/defs.ma".
include "nf2/pr3.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/pc1".
-
include "pc3/defs.ma".
include "pc1/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/props".
-
include "pc3/defs.ma".
include "pr3/pr3.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/subst1".
-
include "pc3/props.ma".
include "pr3/subst1.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/wcpr0".
-
include "pc3/props.ma".
include "wcpr0/getl.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr0/dec".
-
include "pr0/fwd.ma".
include "subst0/dec.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr0/defs".
-
include "subst0/defs.ma".
inductive pr0: T \to (T \to Prop) \def
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr0/fwd".
-
include "pr0/props.ma".
theorem pr0_inv_coq:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr0/pr0".
-
include "pr0/fwd.ma".
include "lift/tlt.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr0/props".
-
include "pr0/defs.ma".
include "subst0/subst0.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr0/subst1".
-
include "pr0/props.ma".
include "subst1/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr1/defs".
-
include "pr0/defs.ma".
inductive pr1: T \to (T \to Prop) \def
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr1/pr1".
-
include "pr1/props.ma".
include "pr0/pr0.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr1/props".
-
include "pr1/defs.ma".
include "pr0/subst1.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr2/clen".
-
include "pr2/props.ma".
include "clen/getl.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr2/defs".
-
include "pr0/defs.ma".
include "getl/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr2/fwd".
-
include "pr2/defs.ma".
include "pr0/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr2/pr2".
-
include "pr2/defs.ma".
include "pr0/pr0.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr2/props".
-
include "pr2/defs.ma".
include "pr0/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr2/subst1".
-
include "pr2/defs.ma".
include "pr0/subst1.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/defs".
-
include "pr2/defs.ma".
inductive pr3 (c: C): T \to (T \to Prop) \def
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/fwd".
-
include "pr3/props.ma".
include "pr2/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/iso".
-
include "pr3/fwd.ma".
include "iso/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/pr1".
-
include "pr3/defs.ma".
include "pr1/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/pr3".
-
include "pr3/props.ma".
include "pr2/pr2.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/props".
-
include "pr3/pr1.ma".
include "pr2/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/subst1".
-
include "pr3/defs.ma".
include "pr2/subst1.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/wcpr0".
-
include "pr3/props.ma".
include "wcpr0/getl.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/r/defs".
-
include "T/defs.ma".
definition r:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/r/props".
-
include "r/defs.ma".
include "s/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/s/defs".
-
include "T/defs.ma".
definition s:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/s/props".
-
include "s/defs.ma".
theorem s_S:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sc3/arity".
-
include "csubc/arity.ma".
include "csubc/getl.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sc3/defs".
-
include "sn3/defs.ma".
include "arity/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sc3/props".
-
include "sc3/defs.ma".
include "sn3/lift1.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sn3/defs".
-
include "pr3/defs.ma".
inductive sn3 (c: C): T \to Prop \def
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sn3/fwd".
-
include "sn3/defs.ma".
include "pr3/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sn3/lift1".
-
include "sn3/props.ma".
include "drop1/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sn3/nf2".
-
include "sn3/defs.ma".
include "nf2/dec.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sn3/props".
-
include "sn3/nf2.ma".
include "sn3/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/spare".
-
include "theory.ma".
definition cbk:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/dec".
-
include "subst0/defs.ma".
include "lift/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/defs".
-
include "lift/defs.ma".
inductive subst0: nat \to (T \to (T \to (T \to Prop))) \def
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/fwd".
-
include "subst0/defs.ma".
include "lift/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/props".
-
include "subst0/fwd.ma".
include "lift/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/subst0".
-
include "subst0/props.ma".
theorem subst0_subst0:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/tlt".
-
include "subst0/defs.ma".
include "lift/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst1/defs".
-
include "subst0/defs.ma".
inductive subst1 (i: nat) (v: T) (t1: T): T \to Prop \def
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst1/fwd".
-
include "subst1/defs.ma".
include "subst0/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst1/props".
-
include "subst1/defs.ma".
include "subst0/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst1/subst1".
-
include "subst1/fwd.ma".
include "subst0/subst0.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tau0/defs".
-
include "G/defs.ma".
include "getl/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tau0/props".
-
include "tau0/defs.ma".
include "getl/drop.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tau1/cnt".
-
include "tau1/props.ma".
include "cnt/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tau1/defs".
-
include "tau0/defs.ma".
inductive tau1 (g: G) (c: C) (t1: T): T \to Prop \def
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tau1/props".
-
include "tau1/defs.ma".
include "tau0/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/theory".
-
include "subst0/tlt.ma".
include "tau1/cnt.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tlist/defs".
-
include "T/defs.ma".
inductive TList: Set \def
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tlist/props".
-
include "tlist/defs.ma".
theorem tslt_wf__q_ind:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tlt/defs".
-
include "T/defs.ma".
definition wadd:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tlt/props".
-
include "tlt/defs.ma".
theorem wadd_le:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/arity".
-
include "ty3/pr3_props.ma".
include "arity/pr3.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/arity_props".
-
include "ty3/arity.ma".
include "ty3/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/dec".
-
include "ty3/pr3_props.ma".
include "pc3/dec.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/defs".
-
include "G/defs.ma".
include "pc3/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0".
-
include "ty3/props.ma".
include "pc3/fsubst0.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/fwd".
-
include "ty3/defs.ma".
include "pc3/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2".
-
include "ty3/arity.ma".
include "pc3/nf2.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3".
-
include "csubt/ty3.ma".
include "ty3/subst1.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props".
-
include "ty3/pr3.ma".
theorem ty3_cred_pr2:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/props".
-
include "ty3/fwd.ma".
include "pc3/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/subst1".
-
include "ty3/props.ma".
include "pc3/subst1.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0".
-
include "ty3/pr3_props.ma".
include "tau0/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/wcpr0/defs".
-
include "pr0/defs.ma".
include "C/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/wcpr0/fwd".
-
include "wcpr0/defs.ma".
theorem wcpr0_gen_sort:
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/wcpr0/getl".
-
include "wcpr0/defs.ma".
include "getl/props.ma".
projects / helm.git / commitdiff