mk_tactic tactic punctation
let mk_apply t punctation =
- let tactic = G.Apply (floc, t) in
+ let tactic = G.ApplyP (floc, t) in
mk_tactic tactic punctation
let mk_change t where pattern punctation =
(* Real tactics *)
| Absurd of loc * 'term
| Apply of loc * 'term
+ | ApplyP of loc * 'term (* apply for procedural reconstruction *)
| ApplyS of loc * 'term * 'term auto_params
| Assumption of loc
| AutoBatch of loc * 'term auto_params
(* First order tactics *)
| Absurd (_, term) -> "absurd" ^ term_pp term
| Apply (_, term) -> "apply " ^ term_pp term
+ | ApplyP (_, term) -> "applyP " ^ term_pp term
| ApplyS (_, term, params) ->
"applyS " ^ term_pp term ^ pp_auto_params ~term_pp params
| AutoBatch (_,params) -> "autobatch " ^
(* First order tactics *)
| GrafiteAst.Absurd (_, term) -> Tactics.absurd term
| GrafiteAst.Apply (_, term) -> Tactics.apply term
+ | GrafiteAst.ApplyP (_, term) -> Tactics.applyP term
| GrafiteAst.ApplyS (_, term, params) ->
Tactics.applyS ~term ~params ~dbd:(LibraryDb.instance ())
~universe:status.GrafiteTypes.universe
| GrafiteAst.Apply (loc, term) ->
let metasenv,cic = disambiguate_term context metasenv term in
metasenv,GrafiteAst.Apply (loc, cic)
+ | GrafiteAst.ApplyP (loc, term) ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.ApplyP (loc, cic)
| GrafiteAst.ApplyS (loc, term, params) ->
let metasenv, params = disambiguate_auto_params metasenv params in
let metasenv,cic = disambiguate_term context metasenv term in
GrafiteAst.Absurd (loc, t)
| IDENT "apply"; t = tactic_term ->
GrafiteAst.Apply (loc, t)
+ | IDENT "applyP"; t = tactic_term ->
+ GrafiteAst.ApplyP (loc, t)
| IDENT "applyS"; t = tactic_term ; params = auto_params ->
GrafiteAst.ApplyS (loc, t, params)
| IDENT "assumption" ->
in
PET.mk_tactic (apply_tac ~term)
+let applyP_tac ~term =
+ let applyP_tac status =
+ let res = PET.apply_tactic (apply_tac ~term) status in res
+ in
+ PET.mk_tactic applyP_tac
+
let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ()=
let intros_tac (proof, goal)
=
val apply_tac:
term: Cic.term -> ProofEngineTypes.tactic
+val applyP_tac: (* apply for procedural reconstruction *)
+ term: Cic.term -> ProofEngineTypes.tactic
val exact_tac:
term: Cic.term -> ProofEngineTypes.tactic
val intros_tac:
let absurd = NegationTactics.absurd_tac
let apply = PrimitiveTactics.apply_tac
+let applyP = PrimitiveTactics.applyP_tac
let applyS = Auto.applyS_tac
let assumption = VariousTactics.assumption_tac
let auto = Auto.auto_tac
-(* GENERATED FILE, DO NOT EDIT. STAMP:Sun Jun 8 15:54:21 CEST 2008 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Jul 2 12:58:59 CEST 2008 *)
val absurd : term:Cic.term -> ProofEngineTypes.tactic
val apply : term:Cic.term -> ProofEngineTypes.tactic
+val applyP : term:Cic.term -> ProofEngineTypes.tactic
val applyS :
dbd:HSql.dbd ->
term:Cic.term ->
--- /dev/null
+LambdaDelta-2/T/defs.ma: LambdaDelta-2/T/defs.mma LambdaDelta-2/preamble.ma
+LambdaDelta-2/T/props.ma: LambdaDelta-2/T/props.mma LambdaDelta-2/T/defs.ma
+LambdaDelta-2/T/dec.ma: LambdaDelta-2/T/dec.mma LambdaDelta-2/T/defs.ma
+LambdaDelta-2/s/defs.ma: LambdaDelta-2/s/defs.mma LambdaDelta-2/T/defs.ma
+LambdaDelta-2/s/props.ma: LambdaDelta-2/s/props.mma LambdaDelta-2/s/defs.ma
+LambdaDelta-2/tlist/defs.ma: LambdaDelta-2/tlist/defs.mma LambdaDelta-2/T/defs.ma
+LambdaDelta-2/tlist/props.ma: LambdaDelta-2/tlist/props.mma LambdaDelta-2/tlist/defs.ma
+LambdaDelta-2/tlt/defs.ma: LambdaDelta-2/tlt/defs.mma LambdaDelta-2/T/defs.ma
+LambdaDelta-2/tlt/props.ma: LambdaDelta-2/tlt/props.mma LambdaDelta-2/tlt/defs.ma
+LambdaDelta-2/iso/defs.ma: LambdaDelta-2/iso/defs.mma LambdaDelta-2/T/defs.ma
+LambdaDelta-2/iso/fwd.ma: LambdaDelta-2/iso/fwd.mma LambdaDelta-2/iso/defs.ma LambdaDelta-2/tlist/defs.ma
+LambdaDelta-2/iso/props.ma: LambdaDelta-2/iso/props.mma LambdaDelta-2/iso/fwd.ma
+LambdaDelta-2/C/defs.ma: LambdaDelta-2/C/defs.mma LambdaDelta-2/T/defs.ma
+LambdaDelta-2/C/props.ma: LambdaDelta-2/C/props.mma LambdaDelta-2/C/defs.ma LambdaDelta-2/T/props.ma
+LambdaDelta-2/r/defs.ma: LambdaDelta-2/r/defs.mma LambdaDelta-2/T/defs.ma
+LambdaDelta-2/r/props.ma: LambdaDelta-2/r/props.mma LambdaDelta-2/r/defs.ma LambdaDelta-2/s/defs.ma
+LambdaDelta-2/clen/defs.ma: LambdaDelta-2/clen/defs.mma LambdaDelta-2/C/defs.ma LambdaDelta-2/s/defs.ma
+LambdaDelta-2/clen/getl.ma: LambdaDelta-2/clen/getl.mma LambdaDelta-2/clen/defs.ma LambdaDelta-2/getl/props.ma
+LambdaDelta-2/flt/defs.ma: LambdaDelta-2/flt/defs.mma LambdaDelta-2/C/defs.ma
+LambdaDelta-2/flt/props.ma: LambdaDelta-2/flt/props.mma LambdaDelta-2/flt/defs.ma LambdaDelta-2/C/props.ma
+LambdaDelta-2/app/defs.ma: LambdaDelta-2/app/defs.mma LambdaDelta-2/C/defs.ma
+LambdaDelta-2/lift/defs.ma: LambdaDelta-2/lift/defs.mma LambdaDelta-2/tlist/defs.ma LambdaDelta-2/s/defs.ma
+LambdaDelta-2/lift/fwd.ma: LambdaDelta-2/lift/fwd.mma LambdaDelta-2/lift/defs.ma
+LambdaDelta-2/lift/props.ma: LambdaDelta-2/lift/props.mma LambdaDelta-2/lift/fwd.ma LambdaDelta-2/s/props.ma
+LambdaDelta-2/lift/tlt.ma: LambdaDelta-2/lift/tlt.mma LambdaDelta-2/lift/fwd.ma LambdaDelta-2/tlt/props.ma
+LambdaDelta-2/lift1/defs.ma: LambdaDelta-2/lift1/defs.mma LambdaDelta-2/lift/defs.ma
+LambdaDelta-2/lift1/fwd.ma: LambdaDelta-2/lift1/fwd.mma LambdaDelta-2/lift1/defs.ma LambdaDelta-2/lift/fwd.ma
+LambdaDelta-2/lift1/props.ma: LambdaDelta-2/lift1/props.mma LambdaDelta-2/lift/props.ma LambdaDelta-2/drop1/defs.ma
+LambdaDelta-2/cnt/defs.ma: LambdaDelta-2/cnt/defs.mma LambdaDelta-2/T/defs.ma
+LambdaDelta-2/cnt/props.ma: LambdaDelta-2/cnt/props.mma LambdaDelta-2/cnt/defs.ma LambdaDelta-2/lift/fwd.ma
+LambdaDelta-2/drop/defs.ma: LambdaDelta-2/drop/defs.mma LambdaDelta-2/C/defs.ma LambdaDelta-2/lift/defs.ma LambdaDelta-2/r/defs.ma
+LambdaDelta-2/drop/fwd.ma: LambdaDelta-2/drop/fwd.mma LambdaDelta-2/drop/defs.ma
+LambdaDelta-2/drop/props.ma: LambdaDelta-2/drop/props.mma LambdaDelta-2/drop/fwd.ma LambdaDelta-2/lift/props.ma LambdaDelta-2/r/props.ma
+LambdaDelta-2/drop1/defs.ma: LambdaDelta-2/drop1/defs.mma LambdaDelta-2/drop/defs.ma LambdaDelta-2/lift1/defs.ma
+LambdaDelta-2/drop1/fwd.ma: LambdaDelta-2/drop1/fwd.mma LambdaDelta-2/drop1/defs.ma
+LambdaDelta-2/drop1/props.ma: LambdaDelta-2/drop1/props.mma LambdaDelta-2/drop1/fwd.ma LambdaDelta-2/drop/props.ma LambdaDelta-2/getl/defs.ma
+LambdaDelta-2/drop1/getl.ma: LambdaDelta-2/drop1/getl.mma LambdaDelta-2/drop1/fwd.ma LambdaDelta-2/getl/drop.ma
+LambdaDelta-2/clear/defs.ma: LambdaDelta-2/clear/defs.mma LambdaDelta-2/C/defs.ma
+LambdaDelta-2/clear/fwd.ma: LambdaDelta-2/clear/fwd.mma LambdaDelta-2/clear/defs.ma
+LambdaDelta-2/clear/props.ma: LambdaDelta-2/clear/props.mma LambdaDelta-2/clear/fwd.ma
+LambdaDelta-2/clear/drop.ma: LambdaDelta-2/clear/drop.mma LambdaDelta-2/clear/fwd.ma LambdaDelta-2/drop/fwd.ma
+LambdaDelta-2/getl/defs.ma: LambdaDelta-2/getl/defs.mma LambdaDelta-2/drop/defs.ma LambdaDelta-2/clear/defs.ma
+LambdaDelta-2/getl/fwd.ma: LambdaDelta-2/getl/fwd.mma LambdaDelta-2/getl/defs.ma LambdaDelta-2/drop/fwd.ma LambdaDelta-2/clear/fwd.ma
+LambdaDelta-2/getl/props.ma: LambdaDelta-2/getl/props.mma LambdaDelta-2/getl/fwd.ma LambdaDelta-2/drop/props.ma LambdaDelta-2/clear/props.ma
+LambdaDelta-2/getl/clear.ma: LambdaDelta-2/getl/clear.mma LambdaDelta-2/getl/props.ma LambdaDelta-2/clear/drop.ma
+LambdaDelta-2/getl/drop.ma: LambdaDelta-2/getl/drop.mma LambdaDelta-2/getl/props.ma LambdaDelta-2/clear/drop.ma
+LambdaDelta-2/getl/getl.ma: LambdaDelta-2/getl/getl.mma LambdaDelta-2/getl/drop.ma LambdaDelta-2/getl/clear.ma
+LambdaDelta-2/getl/dec.ma: LambdaDelta-2/getl/dec.mma LambdaDelta-2/getl/props.ma
+LambdaDelta-2/getl/flt.ma: LambdaDelta-2/getl/flt.mma LambdaDelta-2/getl/fwd.ma LambdaDelta-2/clear/props.ma LambdaDelta-2/flt/props.ma
+LambdaDelta-2/cimp/defs.ma: LambdaDelta-2/cimp/defs.mma LambdaDelta-2/getl/defs.ma
+LambdaDelta-2/cimp/props.ma: LambdaDelta-2/cimp/props.mma LambdaDelta-2/cimp/defs.ma LambdaDelta-2/getl/getl.ma
+LambdaDelta-2/csubv/defs.ma: LambdaDelta-2/csubv/defs.mma LambdaDelta-2/C/defs.ma
+LambdaDelta-2/csubv/props.ma: LambdaDelta-2/csubv/props.mma LambdaDelta-2/csubv/defs.ma LambdaDelta-2/T/props.ma
+LambdaDelta-2/csubv/drop.ma: LambdaDelta-2/csubv/drop.mma LambdaDelta-2/csubv/props.ma LambdaDelta-2/drop/fwd.ma
+LambdaDelta-2/csubv/clear.ma: LambdaDelta-2/csubv/clear.mma LambdaDelta-2/csubv/defs.ma LambdaDelta-2/clear/fwd.ma
+LambdaDelta-2/csubv/getl.ma: LambdaDelta-2/csubv/getl.mma LambdaDelta-2/csubv/clear.ma LambdaDelta-2/csubv/drop.ma LambdaDelta-2/getl/fwd.ma
+LambdaDelta-2/subst0/defs.ma: LambdaDelta-2/subst0/defs.mma LambdaDelta-2/lift/defs.ma
+LambdaDelta-2/subst0/fwd.ma: LambdaDelta-2/subst0/fwd.mma LambdaDelta-2/subst0/defs.ma LambdaDelta-2/lift/props.ma
+LambdaDelta-2/subst0/props.ma: LambdaDelta-2/subst0/props.mma LambdaDelta-2/subst0/fwd.ma
+LambdaDelta-2/subst0/subst0.ma: LambdaDelta-2/subst0/subst0.mma LambdaDelta-2/subst0/props.ma
+LambdaDelta-2/subst0/tlt.ma: LambdaDelta-2/subst0/tlt.mma LambdaDelta-2/subst0/defs.ma LambdaDelta-2/lift/props.ma LambdaDelta-2/lift/tlt.ma
+LambdaDelta-2/subst0/dec.ma: LambdaDelta-2/subst0/dec.mma LambdaDelta-2/subst0/defs.ma LambdaDelta-2/lift/props.ma
+LambdaDelta-2/subst/defs.ma: LambdaDelta-2/subst/defs.mma LambdaDelta-2/lift/defs.ma
+LambdaDelta-2/subst/fwd.ma: LambdaDelta-2/subst/fwd.mma LambdaDelta-2/subst/defs.ma
+LambdaDelta-2/subst/props.ma: LambdaDelta-2/subst/props.mma LambdaDelta-2/subst/fwd.ma LambdaDelta-2/subst0/defs.ma LambdaDelta-2/lift/props.ma
+LambdaDelta-2/subst1/defs.ma: LambdaDelta-2/subst1/defs.mma LambdaDelta-2/subst0/defs.ma
+LambdaDelta-2/subst1/fwd.ma: LambdaDelta-2/subst1/fwd.mma LambdaDelta-2/subst1/defs.ma LambdaDelta-2/subst0/props.ma
+LambdaDelta-2/subst1/props.ma: LambdaDelta-2/subst1/props.mma LambdaDelta-2/subst1/defs.ma LambdaDelta-2/subst0/props.ma
+LambdaDelta-2/subst1/subst1.ma: LambdaDelta-2/subst1/subst1.mma LambdaDelta-2/subst1/fwd.ma LambdaDelta-2/subst0/subst0.ma
+LambdaDelta-2/csubst0/defs.ma: LambdaDelta-2/csubst0/defs.mma LambdaDelta-2/subst0/defs.ma LambdaDelta-2/C/defs.ma
+LambdaDelta-2/csubst0/fwd.ma: LambdaDelta-2/csubst0/fwd.mma LambdaDelta-2/csubst0/defs.ma
+LambdaDelta-2/csubst0/props.ma: LambdaDelta-2/csubst0/props.mma LambdaDelta-2/csubst0/defs.ma
+LambdaDelta-2/csubst0/drop.ma: LambdaDelta-2/csubst0/drop.mma LambdaDelta-2/csubst0/fwd.ma LambdaDelta-2/drop/fwd.ma LambdaDelta-2/s/props.ma
+LambdaDelta-2/csubst0/clear.ma: LambdaDelta-2/csubst0/clear.mma LambdaDelta-2/csubst0/props.ma LambdaDelta-2/csubst0/fwd.ma LambdaDelta-2/clear/fwd.ma
+LambdaDelta-2/csubst0/getl.ma: LambdaDelta-2/csubst0/getl.mma LambdaDelta-2/csubst0/clear.ma LambdaDelta-2/csubst0/drop.ma LambdaDelta-2/getl/fwd.ma
+LambdaDelta-2/csubst1/defs.ma: LambdaDelta-2/csubst1/defs.mma LambdaDelta-2/csubst0/defs.ma
+LambdaDelta-2/csubst1/fwd.ma: LambdaDelta-2/csubst1/fwd.mma LambdaDelta-2/csubst1/defs.ma LambdaDelta-2/csubst0/fwd.ma LambdaDelta-2/subst1/props.ma
+LambdaDelta-2/csubst1/props.ma: LambdaDelta-2/csubst1/props.mma LambdaDelta-2/csubst1/defs.ma LambdaDelta-2/subst1/defs.ma
+LambdaDelta-2/csubst1/getl.ma: LambdaDelta-2/csubst1/getl.mma LambdaDelta-2/csubst1/props.ma LambdaDelta-2/csubst0/getl.ma LambdaDelta-2/subst1/props.ma LambdaDelta-2/drop/props.ma
+LambdaDelta-2/fsubst0/defs.ma: LambdaDelta-2/fsubst0/defs.mma LambdaDelta-2/csubst0/defs.ma
+LambdaDelta-2/fsubst0/fwd.ma: LambdaDelta-2/fsubst0/fwd.mma LambdaDelta-2/fsubst0/defs.ma
+LambdaDelta-2/G/defs.ma: LambdaDelta-2/G/defs.mma LambdaDelta-2/preamble.ma
+LambdaDelta-2/next_plus/defs.ma: LambdaDelta-2/next_plus/defs.mma LambdaDelta-2/G/defs.ma
+LambdaDelta-2/next_plus/props.ma: LambdaDelta-2/next_plus/props.mma LambdaDelta-2/next_plus/defs.ma
+LambdaDelta-2/sty0/defs.ma: LambdaDelta-2/sty0/defs.mma LambdaDelta-2/G/defs.ma LambdaDelta-2/getl/defs.ma
+LambdaDelta-2/sty0/fwd.ma: LambdaDelta-2/sty0/fwd.mma LambdaDelta-2/sty0/defs.ma
+LambdaDelta-2/sty0/props.ma: LambdaDelta-2/sty0/props.mma LambdaDelta-2/sty0/defs.ma LambdaDelta-2/getl/drop.ma
+LambdaDelta-2/sty1/defs.ma: LambdaDelta-2/sty1/defs.mma LambdaDelta-2/sty0/defs.ma
+LambdaDelta-2/sty1/props.ma: LambdaDelta-2/sty1/props.mma LambdaDelta-2/sty1/defs.ma LambdaDelta-2/sty0/props.ma
+LambdaDelta-2/sty1/cnt.ma: LambdaDelta-2/sty1/cnt.mma LambdaDelta-2/sty1/props.ma LambdaDelta-2/cnt/props.ma
+LambdaDelta-2/A/defs.ma: LambdaDelta-2/A/defs.mma LambdaDelta-2/preamble.ma
+LambdaDelta-2/asucc/defs.ma: LambdaDelta-2/asucc/defs.mma LambdaDelta-2/A/defs.ma LambdaDelta-2/G/defs.ma
+LambdaDelta-2/asucc/fwd.ma: LambdaDelta-2/asucc/fwd.mma LambdaDelta-2/asucc/defs.ma
+LambdaDelta-2/aplus/defs.ma: LambdaDelta-2/aplus/defs.mma LambdaDelta-2/asucc/defs.ma
+LambdaDelta-2/aplus/props.ma: LambdaDelta-2/aplus/props.mma LambdaDelta-2/aplus/defs.ma LambdaDelta-2/next_plus/props.ma
+LambdaDelta-2/leq/defs.ma: LambdaDelta-2/leq/defs.mma LambdaDelta-2/aplus/defs.ma
+LambdaDelta-2/leq/fwd.ma: LambdaDelta-2/leq/fwd.mma LambdaDelta-2/leq/defs.ma
+LambdaDelta-2/leq/props.ma: LambdaDelta-2/leq/props.mma LambdaDelta-2/leq/fwd.ma LambdaDelta-2/aplus/props.ma
+LambdaDelta-2/leq/asucc.ma: LambdaDelta-2/leq/asucc.mma LambdaDelta-2/leq/props.ma
+LambdaDelta-2/llt/defs.ma: LambdaDelta-2/llt/defs.mma LambdaDelta-2/A/defs.ma
+LambdaDelta-2/llt/props.ma: LambdaDelta-2/llt/props.mma LambdaDelta-2/llt/defs.ma LambdaDelta-2/leq/defs.ma
+LambdaDelta-2/aprem/defs.ma: LambdaDelta-2/aprem/defs.mma LambdaDelta-2/A/defs.ma
+LambdaDelta-2/aprem/fwd.ma: LambdaDelta-2/aprem/fwd.mma LambdaDelta-2/aprem/defs.ma
+LambdaDelta-2/aprem/props.ma: LambdaDelta-2/aprem/props.mma LambdaDelta-2/aprem/fwd.ma LambdaDelta-2/leq/defs.ma
+LambdaDelta-2/ex0/defs.ma: LambdaDelta-2/ex0/defs.mma LambdaDelta-2/A/defs.ma LambdaDelta-2/G/defs.ma
+LambdaDelta-2/ex0/props.ma: LambdaDelta-2/ex0/props.mma LambdaDelta-2/ex0/defs.ma LambdaDelta-2/leq/defs.ma LambdaDelta-2/aplus/props.ma
+LambdaDelta-2/arity/defs.ma: LambdaDelta-2/arity/defs.mma LambdaDelta-2/leq/defs.ma LambdaDelta-2/getl/defs.ma
+LambdaDelta-2/arity/fwd.ma: LambdaDelta-2/arity/fwd.mma LambdaDelta-2/arity/defs.ma LambdaDelta-2/leq/asucc.ma LambdaDelta-2/getl/drop.ma
+LambdaDelta-2/arity/props.ma: LambdaDelta-2/arity/props.mma LambdaDelta-2/arity/fwd.ma
+LambdaDelta-2/arity/subst0.ma: LambdaDelta-2/arity/subst0.mma LambdaDelta-2/arity/props.ma LambdaDelta-2/fsubst0/fwd.ma LambdaDelta-2/csubst0/getl.ma LambdaDelta-2/subst0/dec.ma LambdaDelta-2/subst0/fwd.ma LambdaDelta-2/getl/getl.ma
+LambdaDelta-2/arity/lift1.ma: LambdaDelta-2/arity/lift1.mma LambdaDelta-2/arity/props.ma LambdaDelta-2/drop1/fwd.ma
+LambdaDelta-2/arity/cimp.ma: LambdaDelta-2/arity/cimp.mma LambdaDelta-2/arity/defs.ma LambdaDelta-2/cimp/props.ma
+LambdaDelta-2/arity/aprem.ma: LambdaDelta-2/arity/aprem.mma LambdaDelta-2/arity/props.ma LambdaDelta-2/arity/cimp.ma LambdaDelta-2/aprem/props.ma
+LambdaDelta-2/pr0/defs.ma: LambdaDelta-2/pr0/defs.mma LambdaDelta-2/subst0/defs.ma
+LambdaDelta-2/pr0/fwd.ma: LambdaDelta-2/pr0/fwd.mma LambdaDelta-2/pr0/props.ma
+LambdaDelta-2/pr0/props.ma: LambdaDelta-2/pr0/props.mma LambdaDelta-2/pr0/defs.ma LambdaDelta-2/subst0/subst0.ma
+LambdaDelta-2/pr0/pr0.ma: LambdaDelta-2/pr0/pr0.mma LambdaDelta-2/pr0/fwd.ma LambdaDelta-2/lift/tlt.ma
+LambdaDelta-2/pr0/subst1.ma: LambdaDelta-2/pr0/subst1.mma LambdaDelta-2/pr0/props.ma LambdaDelta-2/subst1/defs.ma
+LambdaDelta-2/pr0/dec.ma: LambdaDelta-2/pr0/dec.mma LambdaDelta-2/pr0/fwd.ma LambdaDelta-2/subst0/dec.ma LambdaDelta-2/T/dec.ma LambdaDelta-2/T/props.ma
+LambdaDelta-2/pr1/defs.ma: LambdaDelta-2/pr1/defs.mma LambdaDelta-2/pr0/defs.ma
+LambdaDelta-2/pr1/props.ma: LambdaDelta-2/pr1/props.mma LambdaDelta-2/pr1/defs.ma LambdaDelta-2/pr0/subst1.ma LambdaDelta-2/subst1/props.ma LambdaDelta-2/T/props.ma
+LambdaDelta-2/pr1/pr1.ma: LambdaDelta-2/pr1/pr1.mma LambdaDelta-2/pr1/props.ma LambdaDelta-2/pr0/pr0.ma
+LambdaDelta-2/wcpr0/defs.ma: LambdaDelta-2/wcpr0/defs.mma LambdaDelta-2/pr0/defs.ma LambdaDelta-2/C/defs.ma
+LambdaDelta-2/wcpr0/fwd.ma: LambdaDelta-2/wcpr0/fwd.mma LambdaDelta-2/wcpr0/defs.ma
+LambdaDelta-2/wcpr0/getl.ma: LambdaDelta-2/wcpr0/getl.mma LambdaDelta-2/wcpr0/defs.ma LambdaDelta-2/getl/props.ma
+LambdaDelta-2/pr2/defs.ma: LambdaDelta-2/pr2/defs.mma LambdaDelta-2/pr0/defs.ma LambdaDelta-2/getl/defs.ma
+LambdaDelta-2/pr2/fwd.ma: LambdaDelta-2/pr2/fwd.mma LambdaDelta-2/pr2/defs.ma LambdaDelta-2/pr0/fwd.ma LambdaDelta-2/getl/drop.ma LambdaDelta-2/getl/clear.ma
+LambdaDelta-2/pr2/props.ma: LambdaDelta-2/pr2/props.mma LambdaDelta-2/pr2/defs.ma LambdaDelta-2/pr0/props.ma LambdaDelta-2/getl/drop.ma LambdaDelta-2/getl/clear.ma
+LambdaDelta-2/pr2/clen.ma: LambdaDelta-2/pr2/clen.mma LambdaDelta-2/pr2/props.ma LambdaDelta-2/clen/getl.ma
+LambdaDelta-2/pr2/pr2.ma: LambdaDelta-2/pr2/pr2.mma LambdaDelta-2/pr2/defs.ma LambdaDelta-2/pr0/pr0.ma LambdaDelta-2/getl/props.ma
+LambdaDelta-2/pr2/subst1.ma: LambdaDelta-2/pr2/subst1.mma LambdaDelta-2/pr2/defs.ma LambdaDelta-2/pr0/subst1.ma LambdaDelta-2/pr0/fwd.ma LambdaDelta-2/csubst1/getl.ma LambdaDelta-2/csubst1/fwd.ma LambdaDelta-2/subst1/subst1.ma LambdaDelta-2/getl/drop.ma
+LambdaDelta-2/pr3/defs.ma: LambdaDelta-2/pr3/defs.mma LambdaDelta-2/pr2/defs.ma
+LambdaDelta-2/pr3/pr1.ma: LambdaDelta-2/pr3/pr1.mma LambdaDelta-2/pr3/defs.ma LambdaDelta-2/pr1/defs.ma
+LambdaDelta-2/pr3/props.ma: LambdaDelta-2/pr3/props.mma LambdaDelta-2/pr3/pr1.ma LambdaDelta-2/pr2/props.ma LambdaDelta-2/pr1/props.ma
+LambdaDelta-2/pr3/fwd.ma: LambdaDelta-2/pr3/fwd.mma LambdaDelta-2/pr3/props.ma LambdaDelta-2/pr2/fwd.ma
+LambdaDelta-2/pr3/wcpr0.ma: LambdaDelta-2/pr3/wcpr0.mma LambdaDelta-2/pr3/props.ma LambdaDelta-2/wcpr0/getl.ma
+LambdaDelta-2/pr3/pr3.ma: LambdaDelta-2/pr3/pr3.mma LambdaDelta-2/pr3/props.ma LambdaDelta-2/pr2/pr2.ma
+LambdaDelta-2/pr3/subst1.ma: LambdaDelta-2/pr3/subst1.mma LambdaDelta-2/pr3/defs.ma LambdaDelta-2/pr2/subst1.ma
+LambdaDelta-2/pr3/iso.ma: LambdaDelta-2/pr3/iso.mma LambdaDelta-2/pr3/fwd.ma LambdaDelta-2/iso/props.ma LambdaDelta-2/tlist/props.ma
+LambdaDelta-2/csuba/defs.ma: LambdaDelta-2/csuba/defs.mma LambdaDelta-2/arity/defs.ma
+LambdaDelta-2/csuba/fwd.ma: LambdaDelta-2/csuba/fwd.mma LambdaDelta-2/csuba/defs.ma
+LambdaDelta-2/csuba/props.ma: LambdaDelta-2/csuba/props.mma LambdaDelta-2/csuba/defs.ma
+LambdaDelta-2/csuba/clear.ma: LambdaDelta-2/csuba/clear.mma LambdaDelta-2/csuba/defs.ma LambdaDelta-2/clear/fwd.ma
+LambdaDelta-2/csuba/drop.ma: LambdaDelta-2/csuba/drop.mma LambdaDelta-2/csuba/fwd.ma LambdaDelta-2/drop/fwd.ma
+LambdaDelta-2/csuba/getl.ma: LambdaDelta-2/csuba/getl.mma LambdaDelta-2/csuba/drop.ma LambdaDelta-2/csuba/clear.ma LambdaDelta-2/getl/clear.ma
+LambdaDelta-2/csuba/arity.ma: LambdaDelta-2/csuba/arity.mma LambdaDelta-2/csuba/getl.ma LambdaDelta-2/csuba/props.ma LambdaDelta-2/arity/props.ma LambdaDelta-2/csubv/getl.ma
+LambdaDelta-2/arity/pr3.ma: LambdaDelta-2/arity/pr3.mma LambdaDelta-2/csuba/arity.ma LambdaDelta-2/pr3/defs.ma LambdaDelta-2/pr1/defs.ma LambdaDelta-2/wcpr0/getl.ma LambdaDelta-2/pr0/fwd.ma LambdaDelta-2/arity/subst0.ma
+LambdaDelta-2/nf2/defs.ma: LambdaDelta-2/nf2/defs.mma LambdaDelta-2/pr2/defs.ma
+LambdaDelta-2/nf2/fwd.ma: LambdaDelta-2/nf2/fwd.mma LambdaDelta-2/nf2/defs.ma LambdaDelta-2/pr2/clen.ma LambdaDelta-2/subst0/dec.ma LambdaDelta-2/T/props.ma
+LambdaDelta-2/nf2/props.ma: LambdaDelta-2/nf2/props.mma LambdaDelta-2/nf2/defs.ma LambdaDelta-2/pr2/fwd.ma
+LambdaDelta-2/nf2/arity.ma: LambdaDelta-2/nf2/arity.mma LambdaDelta-2/nf2/fwd.ma LambdaDelta-2/arity/subst0.ma
+LambdaDelta-2/nf2/pr3.ma: LambdaDelta-2/nf2/pr3.mma LambdaDelta-2/nf2/defs.ma LambdaDelta-2/pr3/pr3.ma
+LambdaDelta-2/nf2/lift1.ma: LambdaDelta-2/nf2/lift1.mma LambdaDelta-2/nf2/props.ma LambdaDelta-2/drop1/fwd.ma
+LambdaDelta-2/nf2/iso.ma: LambdaDelta-2/nf2/iso.mma LambdaDelta-2/nf2/pr3.ma LambdaDelta-2/pr3/fwd.ma LambdaDelta-2/iso/props.ma
+LambdaDelta-2/ex2/defs.ma: LambdaDelta-2/ex2/defs.mma LambdaDelta-2/C/defs.ma
+LambdaDelta-2/ex2/props.ma: LambdaDelta-2/ex2/props.mma LambdaDelta-2/ex2/defs.ma LambdaDelta-2/nf2/defs.ma LambdaDelta-2/pr2/fwd.ma LambdaDelta-2/arity/fwd.ma
+LambdaDelta-2/nf2/dec.ma: LambdaDelta-2/nf2/dec.mma LambdaDelta-2/nf2/defs.ma LambdaDelta-2/pr2/clen.ma LambdaDelta-2/pr2/fwd.ma LambdaDelta-2/pr0/dec.ma LambdaDelta-2/C/props.ma
+LambdaDelta-2/sn3/defs.ma: LambdaDelta-2/sn3/defs.mma LambdaDelta-2/pr3/defs.ma
+LambdaDelta-2/sn3/fwd.ma: LambdaDelta-2/sn3/fwd.mma LambdaDelta-2/sn3/defs.ma LambdaDelta-2/pr3/props.ma
+LambdaDelta-2/sn3/nf2.ma: LambdaDelta-2/sn3/nf2.mma LambdaDelta-2/sn3/defs.ma LambdaDelta-2/nf2/dec.ma LambdaDelta-2/nf2/pr3.ma
+LambdaDelta-2/sn3/props.ma: LambdaDelta-2/sn3/props.mma LambdaDelta-2/sn3/nf2.ma LambdaDelta-2/sn3/fwd.ma LambdaDelta-2/nf2/iso.ma LambdaDelta-2/pr3/iso.ma
+LambdaDelta-2/sn3/lift1.ma: LambdaDelta-2/sn3/lift1.mma LambdaDelta-2/sn3/props.ma LambdaDelta-2/drop1/fwd.ma LambdaDelta-2/lift1/fwd.ma
+LambdaDelta-2/sc3/defs.ma: LambdaDelta-2/sc3/defs.mma LambdaDelta-2/sn3/defs.ma LambdaDelta-2/arity/defs.ma LambdaDelta-2/drop1/defs.ma
+LambdaDelta-2/sc3/props.ma: LambdaDelta-2/sc3/props.mma LambdaDelta-2/sc3/defs.ma LambdaDelta-2/sn3/lift1.ma LambdaDelta-2/nf2/lift1.ma LambdaDelta-2/csuba/arity.ma LambdaDelta-2/arity/lift1.ma LambdaDelta-2/arity/aprem.ma LambdaDelta-2/llt/props.ma LambdaDelta-2/drop1/getl.ma LambdaDelta-2/drop1/props.ma LambdaDelta-2/lift1/props.ma
+LambdaDelta-2/csubc/defs.ma: LambdaDelta-2/csubc/defs.mma LambdaDelta-2/sc3/defs.ma
+LambdaDelta-2/csubc/fwd.ma: LambdaDelta-2/csubc/fwd.mma LambdaDelta-2/csubc/defs.ma
+LambdaDelta-2/csubc/props.ma: LambdaDelta-2/csubc/props.mma LambdaDelta-2/csubc/defs.ma LambdaDelta-2/sc3/props.ma
+LambdaDelta-2/csubc/csuba.ma: LambdaDelta-2/csubc/csuba.mma LambdaDelta-2/csubc/defs.ma LambdaDelta-2/sc3/props.ma
+LambdaDelta-2/csubc/drop.ma: LambdaDelta-2/csubc/drop.mma LambdaDelta-2/csubc/fwd.ma LambdaDelta-2/sc3/props.ma
+LambdaDelta-2/csubc/drop1.ma: LambdaDelta-2/csubc/drop1.mma LambdaDelta-2/csubc/drop.ma
+LambdaDelta-2/csubc/clear.ma: LambdaDelta-2/csubc/clear.mma LambdaDelta-2/csubc/fwd.ma
+LambdaDelta-2/csubc/getl.ma: LambdaDelta-2/csubc/getl.mma LambdaDelta-2/csubc/drop.ma LambdaDelta-2/csubc/clear.ma
+LambdaDelta-2/csubc/arity.ma: LambdaDelta-2/csubc/arity.mma LambdaDelta-2/csubc/csuba.ma
+LambdaDelta-2/sc3/arity.ma: LambdaDelta-2/sc3/arity.mma LambdaDelta-2/csubc/arity.ma LambdaDelta-2/csubc/getl.ma LambdaDelta-2/csubc/drop1.ma LambdaDelta-2/csubc/props.ma
+LambdaDelta-2/pc1/defs.ma: LambdaDelta-2/pc1/defs.mma LambdaDelta-2/pr1/defs.ma
+LambdaDelta-2/pc1/props.ma: LambdaDelta-2/pc1/props.mma LambdaDelta-2/pc1/defs.ma LambdaDelta-2/pr1/pr1.ma
+LambdaDelta-2/pc3/defs.ma: LambdaDelta-2/pc3/defs.mma LambdaDelta-2/pr3/defs.ma
+LambdaDelta-2/pc3/props.ma: LambdaDelta-2/pc3/props.mma LambdaDelta-2/pc3/defs.ma LambdaDelta-2/pr3/pr3.ma
+LambdaDelta-2/pc3/pc1.ma: LambdaDelta-2/pc3/pc1.mma LambdaDelta-2/pc3/defs.ma LambdaDelta-2/pc1/defs.ma LambdaDelta-2/pr3/pr1.ma
+LambdaDelta-2/pc3/nf2.ma: LambdaDelta-2/pc3/nf2.mma LambdaDelta-2/pc3/defs.ma LambdaDelta-2/nf2/pr3.ma
+LambdaDelta-2/pc3/wcpr0.ma: LambdaDelta-2/pc3/wcpr0.mma LambdaDelta-2/pc3/props.ma LambdaDelta-2/wcpr0/getl.ma
+LambdaDelta-2/pc3/left.ma: LambdaDelta-2/pc3/left.mma LambdaDelta-2/pc3/props.ma
+LambdaDelta-2/pc3/fwd.ma: LambdaDelta-2/pc3/fwd.mma LambdaDelta-2/pc3/props.ma LambdaDelta-2/pr3/fwd.ma
+LambdaDelta-2/pc3/fsubst0.ma: LambdaDelta-2/pc3/fsubst0.mma LambdaDelta-2/pc3/left.ma LambdaDelta-2/fsubst0/defs.ma LambdaDelta-2/csubst0/getl.ma
+LambdaDelta-2/pc3/subst1.ma: LambdaDelta-2/pc3/subst1.mma LambdaDelta-2/pc3/props.ma LambdaDelta-2/pr3/subst1.ma
+LambdaDelta-2/ty3/defs.ma: LambdaDelta-2/ty3/defs.mma LambdaDelta-2/G/defs.ma LambdaDelta-2/pc3/defs.ma
+LambdaDelta-2/ty3/fwd.ma: LambdaDelta-2/ty3/fwd.mma LambdaDelta-2/ty3/defs.ma LambdaDelta-2/pc3/props.ma
+LambdaDelta-2/ex1/defs.ma: LambdaDelta-2/ex1/defs.mma LambdaDelta-2/C/defs.ma
+LambdaDelta-2/ex1/props.ma: LambdaDelta-2/ex1/props.mma LambdaDelta-2/ex1/defs.ma LambdaDelta-2/ty3/fwd.ma LambdaDelta-2/pc3/fwd.ma LambdaDelta-2/nf2/pr3.ma LambdaDelta-2/nf2/props.ma LambdaDelta-2/arity/defs.ma LambdaDelta-2/leq/props.ma
+LambdaDelta-2/ty3/props.ma: LambdaDelta-2/ty3/props.mma LambdaDelta-2/ty3/fwd.ma LambdaDelta-2/pc3/fwd.ma
+LambdaDelta-2/ty3/fsubst0.ma: LambdaDelta-2/ty3/fsubst0.mma LambdaDelta-2/ty3/props.ma LambdaDelta-2/pc3/fsubst0.ma LambdaDelta-2/getl/getl.ma
+LambdaDelta-2/ty3/subst1.ma: LambdaDelta-2/ty3/subst1.mma LambdaDelta-2/ty3/props.ma LambdaDelta-2/pc3/subst1.ma LambdaDelta-2/getl/getl.ma
+LambdaDelta-2/csubt/defs.ma: LambdaDelta-2/csubt/defs.mma LambdaDelta-2/ty3/defs.ma
+LambdaDelta-2/csubt/fwd.ma: LambdaDelta-2/csubt/fwd.mma LambdaDelta-2/csubt/defs.ma
+LambdaDelta-2/csubt/props.ma: LambdaDelta-2/csubt/props.mma LambdaDelta-2/csubt/defs.ma
+LambdaDelta-2/csubt/clear.ma: LambdaDelta-2/csubt/clear.mma LambdaDelta-2/csubt/defs.ma LambdaDelta-2/clear/fwd.ma
+LambdaDelta-2/csubt/drop.ma: LambdaDelta-2/csubt/drop.mma LambdaDelta-2/csubt/fwd.ma LambdaDelta-2/drop/fwd.ma
+LambdaDelta-2/csubt/getl.ma: LambdaDelta-2/csubt/getl.mma LambdaDelta-2/csubt/clear.ma LambdaDelta-2/csubt/drop.ma LambdaDelta-2/getl/clear.ma
+LambdaDelta-2/csubt/pc3.ma: LambdaDelta-2/csubt/pc3.mma LambdaDelta-2/csubt/getl.ma LambdaDelta-2/pc3/left.ma
+LambdaDelta-2/csubt/ty3.ma: LambdaDelta-2/csubt/ty3.mma LambdaDelta-2/csubt/pc3.ma LambdaDelta-2/csubt/props.ma
+LambdaDelta-2/ty3/pr3.ma: LambdaDelta-2/ty3/pr3.mma LambdaDelta-2/csubt/ty3.ma LambdaDelta-2/ty3/subst1.ma LambdaDelta-2/ty3/fsubst0.ma LambdaDelta-2/pc3/pc1.ma LambdaDelta-2/pc3/wcpr0.ma LambdaDelta-2/pc1/props.ma
+LambdaDelta-2/ty3/pr3_props.ma: LambdaDelta-2/ty3/pr3_props.mma LambdaDelta-2/ty3/pr3.ma
+LambdaDelta-2/ty3/sty0.ma: LambdaDelta-2/ty3/sty0.mma LambdaDelta-2/ty3/pr3_props.ma LambdaDelta-2/sty0/fwd.ma
+LambdaDelta-2/ty3/arity.ma: LambdaDelta-2/ty3/arity.mma LambdaDelta-2/ty3/pr3_props.ma LambdaDelta-2/arity/pr3.ma LambdaDelta-2/asucc/fwd.ma
+LambdaDelta-2/ty3/arity_props.ma: LambdaDelta-2/ty3/arity_props.mma LambdaDelta-2/ty3/arity.ma LambdaDelta-2/sc3/arity.ma
+LambdaDelta-2/csubt/csuba.ma: LambdaDelta-2/csubt/csuba.mma LambdaDelta-2/ty3/arity.ma
+LambdaDelta-2/ty3/fwd_nf2.ma: LambdaDelta-2/ty3/fwd_nf2.mma LambdaDelta-2/ty3/arity_props.ma LambdaDelta-2/pc3/nf2.ma LambdaDelta-2/nf2/fwd.ma
+LambdaDelta-2/ty3/nf2.ma: LambdaDelta-2/ty3/nf2.mma LambdaDelta-2/ty3/arity.ma LambdaDelta-2/pc3/nf2.ma LambdaDelta-2/nf2/arity.ma
+LambdaDelta-2/pc3/dec.ma: LambdaDelta-2/pc3/dec.mma LambdaDelta-2/ty3/arity_props.ma LambdaDelta-2/nf2/fwd.ma
+LambdaDelta-2/ty3/dec.ma: LambdaDelta-2/ty3/dec.mma LambdaDelta-2/pc3/dec.ma LambdaDelta-2/getl/flt.ma LambdaDelta-2/getl/dec.ma
+LambdaDelta-2/wf3/defs.ma: LambdaDelta-2/wf3/defs.mma LambdaDelta-2/ty3/defs.ma
+LambdaDelta-2/wf3/fwd.ma: LambdaDelta-2/wf3/fwd.mma LambdaDelta-2/wf3/defs.ma
+LambdaDelta-2/wf3/clear.ma: LambdaDelta-2/wf3/clear.mma LambdaDelta-2/wf3/fwd.ma
+LambdaDelta-2/wf3/getl.ma: LambdaDelta-2/wf3/getl.mma LambdaDelta-2/wf3/clear.ma LambdaDelta-2/ty3/dec.ma
+LambdaDelta-2/wf3/ty3.ma: LambdaDelta-2/wf3/ty3.mma LambdaDelta-2/wf3/getl.ma
+LambdaDelta-2/wf3/props.ma: LambdaDelta-2/wf3/props.mma LambdaDelta-2/wf3/ty3.ma LambdaDelta-2/app/defs.ma
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/preamble.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/T/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/C/defs.ma".
+
+include "LambdaDelta-2/T/props.ma".
+
+inline procedural "LambdaDelta-1/C/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/preamble.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/T/defs.ma".
+
+inline procedural "LambdaDelta-1/T/dec.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/preamble.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/T/defs.ma".
+
+inline procedural "LambdaDelta-1/T/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/asucc/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/aplus/defs.ma".
+
+include "LambdaDelta-2/next_plus/props.ma".
+
+inline procedural "LambdaDelta-1/aplus/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/C/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/A/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/aprem/defs.ma".
+
+inline procedural "LambdaDelta-1/aprem/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/aprem/fwd.ma".
+
+include "LambdaDelta-2/leq/defs.ma".
+
+inline procedural "LambdaDelta-1/aprem/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/arity/props.ma".
+
+include "LambdaDelta-2/arity/cimp.ma".
+
+include "LambdaDelta-2/aprem/props.ma".
+
+inline procedural "LambdaDelta-1/arity/aprem.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/arity/defs.ma".
+
+include "LambdaDelta-2/cimp/props.ma".
+
+inline procedural "LambdaDelta-1/arity/cimp.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/leq/defs.ma".
+
+include "LambdaDelta-2/getl/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/arity/defs.ma".
+
+include "LambdaDelta-2/leq/asucc.ma".
+
+include "LambdaDelta-2/getl/drop.ma".
+
+inline procedural "LambdaDelta-1/arity/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/arity/props.ma".
+
+include "LambdaDelta-2/drop1/fwd.ma".
+
+inline procedural "LambdaDelta-1/arity/lift1.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csuba/arity.ma".
+
+include "LambdaDelta-2/pr3/defs.ma".
+
+include "LambdaDelta-2/pr1/defs.ma".
+
+include "LambdaDelta-2/wcpr0/getl.ma".
+
+include "LambdaDelta-2/pr0/fwd.ma".
+
+include "LambdaDelta-2/arity/subst0.ma".
+
+inline procedural "LambdaDelta-1/arity/pr3.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/arity/fwd.ma".
+
+inline procedural "LambdaDelta-1/arity/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/arity/props.ma".
+
+include "LambdaDelta-2/fsubst0/fwd.ma".
+
+include "LambdaDelta-2/csubst0/getl.ma".
+
+include "LambdaDelta-2/subst0/dec.ma".
+
+include "LambdaDelta-2/subst0/fwd.ma".
+
+include "LambdaDelta-2/getl/getl.ma".
+
+inline procedural "LambdaDelta-1/arity/subst0.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/A/defs.ma".
+
+include "LambdaDelta-2/G/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/asucc/defs.ma".
+
+inline procedural "LambdaDelta-1/asucc/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/getl/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/cimp/defs.ma".
+
+include "LambdaDelta-2/getl/getl.ma".
+
+inline procedural "LambdaDelta-1/cimp/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/C/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/clear/fwd.ma".
+
+include "LambdaDelta-2/drop/fwd.ma".
+
+inline procedural "LambdaDelta-1/clear/drop.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/clear/defs.ma".
+
+inline procedural "LambdaDelta-1/clear/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/clear/fwd.ma".
+
+inline procedural "LambdaDelta-1/clear/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/C/defs.ma".
+
+include "LambdaDelta-2/s/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/clen/defs.ma".
+
+include "LambdaDelta-2/getl/props.ma".
+
+inline procedural "LambdaDelta-1/clen/getl.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/T/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/cnt/defs.ma".
+
+include "LambdaDelta-2/lift/fwd.ma".
+
+inline procedural "LambdaDelta-1/cnt/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csuba/getl.ma".
+
+include "LambdaDelta-2/csuba/props.ma".
+
+include "LambdaDelta-2/arity/props.ma".
+
+include "LambdaDelta-2/csubv/getl.ma".
+
+inline procedural "LambdaDelta-1/csuba/arity.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csuba/defs.ma".
+
+include "LambdaDelta-2/clear/fwd.ma".
+
+inline procedural "LambdaDelta-1/csuba/clear.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/arity/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csuba/fwd.ma".
+
+include "LambdaDelta-2/drop/fwd.ma".
+
+inline procedural "LambdaDelta-1/csuba/drop.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csuba/defs.ma".
+
+inline procedural "LambdaDelta-1/csuba/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csuba/drop.ma".
+
+include "LambdaDelta-2/csuba/clear.ma".
+
+include "LambdaDelta-2/getl/clear.ma".
+
+inline procedural "LambdaDelta-1/csuba/getl.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csuba/defs.ma".
+
+inline procedural "LambdaDelta-1/csuba/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubc/csuba.ma".
+
+inline procedural "LambdaDelta-1/csubc/arity.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubc/fwd.ma".
+
+inline procedural "LambdaDelta-1/csubc/clear.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubc/defs.ma".
+
+include "LambdaDelta-2/sc3/props.ma".
+
+inline procedural "LambdaDelta-1/csubc/csuba.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/sc3/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubc/fwd.ma".
+
+include "LambdaDelta-2/sc3/props.ma".
+
+inline procedural "LambdaDelta-1/csubc/drop.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubc/drop.ma".
+
+inline procedural "LambdaDelta-1/csubc/drop1.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubc/defs.ma".
+
+inline procedural "LambdaDelta-1/csubc/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubc/drop.ma".
+
+include "LambdaDelta-2/csubc/clear.ma".
+
+inline procedural "LambdaDelta-1/csubc/getl.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubc/defs.ma".
+
+include "LambdaDelta-2/sc3/props.ma".
+
+inline procedural "LambdaDelta-1/csubc/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubst0/props.ma".
+
+include "LambdaDelta-2/csubst0/fwd.ma".
+
+include "LambdaDelta-2/clear/fwd.ma".
+
+inline procedural "LambdaDelta-1/csubst0/clear.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/subst0/defs.ma".
+
+include "LambdaDelta-2/C/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubst0/fwd.ma".
+
+include "LambdaDelta-2/drop/fwd.ma".
+
+include "LambdaDelta-2/s/props.ma".
+
+inline procedural "LambdaDelta-1/csubst0/drop.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubst0/defs.ma".
+
+inline procedural "LambdaDelta-1/csubst0/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubst0/clear.ma".
+
+include "LambdaDelta-2/csubst0/drop.ma".
+
+include "LambdaDelta-2/getl/fwd.ma".
+
+inline procedural "LambdaDelta-1/csubst0/getl.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubst0/defs.ma".
+
+inline procedural "LambdaDelta-1/csubst0/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubst0/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubst1/defs.ma".
+
+include "LambdaDelta-2/csubst0/fwd.ma".
+
+include "LambdaDelta-2/subst1/props.ma".
+
+inline procedural "LambdaDelta-1/csubst1/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubst1/props.ma".
+
+include "LambdaDelta-2/csubst0/getl.ma".
+
+include "LambdaDelta-2/subst1/props.ma".
+
+include "LambdaDelta-2/drop/props.ma".
+
+inline procedural "LambdaDelta-1/csubst1/getl.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubst1/defs.ma".
+
+include "LambdaDelta-2/subst1/defs.ma".
+
+inline procedural "LambdaDelta-1/csubst1/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubt/defs.ma".
+
+include "LambdaDelta-2/clear/fwd.ma".
+
+inline procedural "LambdaDelta-1/csubt/clear.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/ty3/arity.ma".
+
+inline procedural "LambdaDelta-1/csubt/csuba.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/ty3/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubt/fwd.ma".
+
+include "LambdaDelta-2/drop/fwd.ma".
+
+inline procedural "LambdaDelta-1/csubt/drop.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubt/defs.ma".
+
+inline procedural "LambdaDelta-1/csubt/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubt/clear.ma".
+
+include "LambdaDelta-2/csubt/drop.ma".
+
+include "LambdaDelta-2/getl/clear.ma".
+
+inline procedural "LambdaDelta-1/csubt/getl.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubt/getl.ma".
+
+include "LambdaDelta-2/pc3/left.ma".
+
+inline procedural "LambdaDelta-1/csubt/pc3.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubt/defs.ma".
+
+inline procedural "LambdaDelta-1/csubt/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubt/pc3.ma".
+
+include "LambdaDelta-2/csubt/props.ma".
+
+inline procedural "LambdaDelta-1/csubt/ty3.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubv/defs.ma".
+
+include "LambdaDelta-2/clear/fwd.ma".
+
+inline procedural "LambdaDelta-1/csubv/clear.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/C/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubv/props.ma".
+
+include "LambdaDelta-2/drop/fwd.ma".
+
+inline procedural "LambdaDelta-1/csubv/drop.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubv/clear.ma".
+
+include "LambdaDelta-2/csubv/drop.ma".
+
+include "LambdaDelta-2/getl/fwd.ma".
+
+inline procedural "LambdaDelta-1/csubv/getl.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubv/defs.ma".
+
+include "LambdaDelta-2/T/props.ma".
+
+inline procedural "LambdaDelta-1/csubv/props.ma".
+
--- /dev/null
+LambdaDelta-2/T/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/T/defs.ma
+LambdaDelta-2/T/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/T/props.ma
+LambdaDelta-2/T/dec.mma LambdaDelta-2/preamble.ma LambdaDelta-1/T/dec.ma
+LambdaDelta-2/s/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/s/defs.ma
+LambdaDelta-2/s/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/s/props.ma
+LambdaDelta-2/tlist/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/tlist/defs.ma
+LambdaDelta-2/tlist/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/tlist/props.ma
+LambdaDelta-2/tlt/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/tlt/defs.ma
+LambdaDelta-2/tlt/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/tlt/props.ma
+LambdaDelta-2/iso/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/iso/defs.ma
+LambdaDelta-2/iso/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/iso/fwd.ma
+LambdaDelta-2/iso/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/iso/props.ma
+LambdaDelta-2/C/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/C/defs.ma
+LambdaDelta-2/C/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/C/props.ma
+LambdaDelta-2/r/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/r/defs.ma
+LambdaDelta-2/r/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/r/props.ma
+LambdaDelta-2/clen/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/clen/defs.ma
+LambdaDelta-2/clen/getl.mma LambdaDelta-2/preamble.ma LambdaDelta-1/clen/getl.ma
+LambdaDelta-2/flt/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/flt/defs.ma
+LambdaDelta-2/flt/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/flt/props.ma
+LambdaDelta-2/app/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/app/defs.ma
+LambdaDelta-2/lift/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/lift/defs.ma
+LambdaDelta-2/lift/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/lift/fwd.ma
+LambdaDelta-2/lift/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/lift/props.ma
+LambdaDelta-2/lift/tlt.mma LambdaDelta-2/preamble.ma LambdaDelta-1/lift/tlt.ma
+LambdaDelta-2/lift1/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/lift1/defs.ma
+LambdaDelta-2/lift1/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/lift1/fwd.ma
+LambdaDelta-2/lift1/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/lift1/props.ma
+LambdaDelta-2/cnt/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/cnt/defs.ma
+LambdaDelta-2/cnt/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/cnt/props.ma
+LambdaDelta-2/drop/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/drop/defs.ma
+LambdaDelta-2/drop/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/drop/fwd.ma
+LambdaDelta-2/drop/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/drop/props.ma
+LambdaDelta-2/drop1/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/drop1/defs.ma
+LambdaDelta-2/drop1/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/drop1/fwd.ma
+LambdaDelta-2/drop1/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/drop1/props.ma
+LambdaDelta-2/drop1/getl.mma LambdaDelta-2/preamble.ma LambdaDelta-1/drop1/getl.ma
+LambdaDelta-2/clear/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/clear/defs.ma
+LambdaDelta-2/clear/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/clear/fwd.ma
+LambdaDelta-2/clear/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/clear/props.ma
+LambdaDelta-2/clear/drop.mma LambdaDelta-2/preamble.ma LambdaDelta-1/clear/drop.ma
+LambdaDelta-2/getl/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/getl/defs.ma
+LambdaDelta-2/getl/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/getl/fwd.ma
+LambdaDelta-2/getl/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/getl/props.ma
+LambdaDelta-2/getl/clear.mma LambdaDelta-2/preamble.ma LambdaDelta-1/getl/clear.ma
+LambdaDelta-2/getl/drop.mma LambdaDelta-2/preamble.ma LambdaDelta-1/getl/drop.ma
+LambdaDelta-2/getl/getl.mma LambdaDelta-2/preamble.ma LambdaDelta-1/getl/getl.ma
+LambdaDelta-2/getl/dec.mma LambdaDelta-2/preamble.ma LambdaDelta-1/getl/dec.ma
+LambdaDelta-2/getl/flt.mma LambdaDelta-2/preamble.ma LambdaDelta-1/getl/flt.ma
+LambdaDelta-2/cimp/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/cimp/defs.ma
+LambdaDelta-2/cimp/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/cimp/props.ma
+LambdaDelta-2/csubv/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubv/defs.ma
+LambdaDelta-2/csubv/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubv/props.ma
+LambdaDelta-2/csubv/drop.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubv/drop.ma
+LambdaDelta-2/csubv/clear.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubv/clear.ma
+LambdaDelta-2/csubv/getl.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubv/getl.ma
+LambdaDelta-2/subst0/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/subst0/defs.ma
+LambdaDelta-2/subst0/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/subst0/fwd.ma
+LambdaDelta-2/subst0/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/subst0/props.ma
+LambdaDelta-2/subst0/subst0.mma LambdaDelta-2/preamble.ma LambdaDelta-1/subst0/subst0.ma
+LambdaDelta-2/subst0/tlt.mma LambdaDelta-2/preamble.ma LambdaDelta-1/subst0/tlt.ma
+LambdaDelta-2/subst0/dec.mma LambdaDelta-2/preamble.ma LambdaDelta-1/subst0/dec.ma
+LambdaDelta-2/subst/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/subst/defs.ma
+LambdaDelta-2/subst/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/subst/fwd.ma
+LambdaDelta-2/subst/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/subst/props.ma
+LambdaDelta-2/subst1/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/subst1/defs.ma
+LambdaDelta-2/subst1/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/subst1/fwd.ma
+LambdaDelta-2/subst1/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/subst1/props.ma
+LambdaDelta-2/subst1/subst1.mma LambdaDelta-2/preamble.ma LambdaDelta-1/subst1/subst1.ma
+LambdaDelta-2/csubst0/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubst0/defs.ma
+LambdaDelta-2/csubst0/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubst0/fwd.ma
+LambdaDelta-2/csubst0/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubst0/props.ma
+LambdaDelta-2/csubst0/drop.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubst0/drop.ma
+LambdaDelta-2/csubst0/clear.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubst0/clear.ma
+LambdaDelta-2/csubst0/getl.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubst0/getl.ma
+LambdaDelta-2/csubst1/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubst1/defs.ma
+LambdaDelta-2/csubst1/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubst1/fwd.ma
+LambdaDelta-2/csubst1/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubst1/props.ma
+LambdaDelta-2/csubst1/getl.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubst1/getl.ma
+LambdaDelta-2/fsubst0/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/fsubst0/defs.ma
+LambdaDelta-2/fsubst0/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/fsubst0/fwd.ma
+LambdaDelta-2/G/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/G/defs.ma
+LambdaDelta-2/next_plus/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/next_plus/defs.ma
+LambdaDelta-2/next_plus/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/next_plus/props.ma
+LambdaDelta-2/sty0/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sty0/defs.ma
+LambdaDelta-2/sty0/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sty0/fwd.ma
+LambdaDelta-2/sty0/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sty0/props.ma
+LambdaDelta-2/sty1/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sty1/defs.ma
+LambdaDelta-2/sty1/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sty1/props.ma
+LambdaDelta-2/sty1/cnt.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sty1/cnt.ma
+LambdaDelta-2/A/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/A/defs.ma
+LambdaDelta-2/asucc/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/asucc/defs.ma
+LambdaDelta-2/asucc/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/asucc/fwd.ma
+LambdaDelta-2/aplus/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/aplus/defs.ma
+LambdaDelta-2/aplus/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/aplus/props.ma
+LambdaDelta-2/leq/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/leq/defs.ma
+LambdaDelta-2/leq/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/leq/fwd.ma
+LambdaDelta-2/leq/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/leq/props.ma
+LambdaDelta-2/leq/asucc.mma LambdaDelta-2/preamble.ma LambdaDelta-1/leq/asucc.ma
+LambdaDelta-2/llt/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/llt/defs.ma
+LambdaDelta-2/llt/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/llt/props.ma
+LambdaDelta-2/aprem/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/aprem/defs.ma
+LambdaDelta-2/aprem/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/aprem/fwd.ma
+LambdaDelta-2/aprem/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/aprem/props.ma
+LambdaDelta-2/ex0/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ex0/defs.ma
+LambdaDelta-2/ex0/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ex0/props.ma
+LambdaDelta-2/arity/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/arity/defs.ma
+LambdaDelta-2/arity/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/arity/fwd.ma
+LambdaDelta-2/arity/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/arity/props.ma
+LambdaDelta-2/arity/subst0.mma LambdaDelta-2/preamble.ma LambdaDelta-1/arity/subst0.ma
+LambdaDelta-2/arity/lift1.mma LambdaDelta-2/preamble.ma LambdaDelta-1/arity/lift1.ma
+LambdaDelta-2/arity/cimp.mma LambdaDelta-2/preamble.ma LambdaDelta-1/arity/cimp.ma
+LambdaDelta-2/arity/aprem.mma LambdaDelta-2/preamble.ma LambdaDelta-1/arity/aprem.ma
+LambdaDelta-2/pr0/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr0/defs.ma
+LambdaDelta-2/pr0/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr0/fwd.ma
+LambdaDelta-2/pr0/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr0/props.ma
+LambdaDelta-2/pr0/pr0.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr0/pr0.ma
+LambdaDelta-2/pr0/subst1.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr0/subst1.ma
+LambdaDelta-2/pr0/dec.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr0/dec.ma
+LambdaDelta-2/pr1/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr1/defs.ma
+LambdaDelta-2/pr1/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr1/props.ma
+LambdaDelta-2/pr1/pr1.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr1/pr1.ma
+LambdaDelta-2/wcpr0/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/wcpr0/defs.ma
+LambdaDelta-2/wcpr0/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/wcpr0/fwd.ma
+LambdaDelta-2/wcpr0/getl.mma LambdaDelta-2/preamble.ma LambdaDelta-1/wcpr0/getl.ma
+LambdaDelta-2/pr2/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr2/defs.ma
+LambdaDelta-2/pr2/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr2/fwd.ma
+LambdaDelta-2/pr2/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr2/props.ma
+LambdaDelta-2/pr2/clen.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr2/clen.ma
+LambdaDelta-2/pr2/pr2.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr2/pr2.ma
+LambdaDelta-2/pr2/subst1.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr2/subst1.ma
+LambdaDelta-2/pr3/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr3/defs.ma
+LambdaDelta-2/pr3/pr1.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr3/pr1.ma
+LambdaDelta-2/pr3/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr3/props.ma
+LambdaDelta-2/pr3/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr3/fwd.ma
+LambdaDelta-2/pr3/wcpr0.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr3/wcpr0.ma
+LambdaDelta-2/pr3/pr3.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr3/pr3.ma
+LambdaDelta-2/pr3/subst1.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr3/subst1.ma
+LambdaDelta-2/pr3/iso.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pr3/iso.ma
+LambdaDelta-2/csuba/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csuba/defs.ma
+LambdaDelta-2/csuba/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csuba/fwd.ma
+LambdaDelta-2/csuba/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csuba/props.ma
+LambdaDelta-2/csuba/clear.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csuba/clear.ma
+LambdaDelta-2/csuba/drop.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csuba/drop.ma
+LambdaDelta-2/csuba/getl.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csuba/getl.ma
+LambdaDelta-2/csuba/arity.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csuba/arity.ma
+LambdaDelta-2/arity/pr3.mma LambdaDelta-2/preamble.ma LambdaDelta-1/arity/pr3.ma
+LambdaDelta-2/nf2/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/nf2/defs.ma
+LambdaDelta-2/nf2/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/nf2/fwd.ma
+LambdaDelta-2/nf2/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/nf2/props.ma
+LambdaDelta-2/nf2/arity.mma LambdaDelta-2/preamble.ma LambdaDelta-1/nf2/arity.ma
+LambdaDelta-2/nf2/pr3.mma LambdaDelta-2/preamble.ma LambdaDelta-1/nf2/pr3.ma
+LambdaDelta-2/nf2/lift1.mma LambdaDelta-2/preamble.ma LambdaDelta-1/nf2/lift1.ma
+LambdaDelta-2/nf2/iso.mma LambdaDelta-2/preamble.ma LambdaDelta-1/nf2/iso.ma
+LambdaDelta-2/ex2/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ex2/defs.ma
+LambdaDelta-2/ex2/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ex2/props.ma
+LambdaDelta-2/nf2/dec.mma LambdaDelta-2/preamble.ma LambdaDelta-1/nf2/dec.ma
+LambdaDelta-2/sn3/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sn3/defs.ma
+LambdaDelta-2/sn3/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sn3/fwd.ma
+LambdaDelta-2/sn3/nf2.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sn3/nf2.ma
+LambdaDelta-2/sn3/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sn3/props.ma
+LambdaDelta-2/sn3/lift1.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sn3/lift1.ma
+LambdaDelta-2/sc3/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sc3/defs.ma
+LambdaDelta-2/sc3/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sc3/props.ma
+LambdaDelta-2/csubc/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubc/defs.ma
+LambdaDelta-2/csubc/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubc/fwd.ma
+LambdaDelta-2/csubc/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubc/props.ma
+LambdaDelta-2/csubc/csuba.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubc/csuba.ma
+LambdaDelta-2/csubc/drop.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubc/drop.ma
+LambdaDelta-2/csubc/drop1.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubc/drop1.ma
+LambdaDelta-2/csubc/clear.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubc/clear.ma
+LambdaDelta-2/csubc/getl.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubc/getl.ma
+LambdaDelta-2/csubc/arity.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubc/arity.ma
+LambdaDelta-2/sc3/arity.mma LambdaDelta-2/preamble.ma LambdaDelta-1/sc3/arity.ma
+LambdaDelta-2/pc1/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pc1/defs.ma
+LambdaDelta-2/pc1/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pc1/props.ma
+LambdaDelta-2/pc3/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pc3/defs.ma
+LambdaDelta-2/pc3/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pc3/props.ma
+LambdaDelta-2/pc3/pc1.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pc3/pc1.ma
+LambdaDelta-2/pc3/nf2.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pc3/nf2.ma
+LambdaDelta-2/pc3/wcpr0.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pc3/wcpr0.ma
+LambdaDelta-2/pc3/left.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pc3/left.ma
+LambdaDelta-2/pc3/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pc3/fwd.ma
+LambdaDelta-2/pc3/fsubst0.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pc3/fsubst0.ma
+LambdaDelta-2/pc3/subst1.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pc3/subst1.ma
+LambdaDelta-2/ty3/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ty3/defs.ma
+LambdaDelta-2/ty3/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ty3/fwd.ma
+LambdaDelta-2/ex1/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ex1/defs.ma
+LambdaDelta-2/ex1/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ex1/props.ma
+LambdaDelta-2/ty3/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ty3/props.ma
+LambdaDelta-2/ty3/fsubst0.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ty3/fsubst0.ma
+LambdaDelta-2/ty3/subst1.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ty3/subst1.ma
+LambdaDelta-2/csubt/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubt/defs.ma
+LambdaDelta-2/csubt/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubt/fwd.ma
+LambdaDelta-2/csubt/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubt/props.ma
+LambdaDelta-2/csubt/clear.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubt/clear.ma
+LambdaDelta-2/csubt/drop.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubt/drop.ma
+LambdaDelta-2/csubt/getl.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubt/getl.ma
+LambdaDelta-2/csubt/pc3.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubt/pc3.ma
+LambdaDelta-2/csubt/ty3.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubt/ty3.ma
+LambdaDelta-2/ty3/pr3.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ty3/pr3.ma
+LambdaDelta-2/ty3/pr3_props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ty3/pr3_props.ma
+LambdaDelta-2/ty3/sty0.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ty3/sty0.ma
+LambdaDelta-2/ty3/arity.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ty3/arity.ma
+LambdaDelta-2/ty3/arity_props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ty3/arity_props.ma
+LambdaDelta-2/csubt/csuba.mma LambdaDelta-2/preamble.ma LambdaDelta-1/csubt/csuba.ma
+LambdaDelta-2/ty3/fwd_nf2.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ty3/fwd_nf2.ma
+LambdaDelta-2/ty3/nf2.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ty3/nf2.ma
+LambdaDelta-2/pc3/dec.mma LambdaDelta-2/preamble.ma LambdaDelta-1/pc3/dec.ma
+LambdaDelta-2/ty3/dec.mma LambdaDelta-2/preamble.ma LambdaDelta-1/ty3/dec.ma
+LambdaDelta-2/wf3/defs.mma LambdaDelta-2/preamble.ma LambdaDelta-1/wf3/defs.ma
+LambdaDelta-2/wf3/fwd.mma LambdaDelta-2/preamble.ma LambdaDelta-1/wf3/fwd.ma
+LambdaDelta-2/wf3/clear.mma LambdaDelta-2/preamble.ma LambdaDelta-1/wf3/clear.ma
+LambdaDelta-2/wf3/getl.mma LambdaDelta-2/preamble.ma LambdaDelta-1/wf3/getl.ma
+LambdaDelta-2/wf3/ty3.mma LambdaDelta-2/preamble.ma LambdaDelta-1/wf3/ty3.ma
+LambdaDelta-2/wf3/props.mma LambdaDelta-2/preamble.ma LambdaDelta-1/wf3/props.ma
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/C/defs.ma".
+
+include "LambdaDelta-2/lift/defs.ma".
+
+include "LambdaDelta-2/r/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/drop/defs.ma".
+
+inline procedural "LambdaDelta-1/drop/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/drop/fwd.ma".
+
+include "LambdaDelta-2/lift/props.ma".
+
+include "LambdaDelta-2/r/props.ma".
+
+inline procedural "LambdaDelta-1/drop/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/drop/defs.ma".
+
+include "LambdaDelta-2/lift1/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/drop1/defs.ma".
+
+inline procedural "LambdaDelta-1/drop1/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/drop1/fwd.ma".
+
+include "LambdaDelta-2/getl/drop.ma".
+
+inline procedural "LambdaDelta-1/drop1/getl.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/drop1/fwd.ma".
+
+include "LambdaDelta-2/drop/props.ma".
+
+include "LambdaDelta-2/getl/defs.ma".
+
+inline procedural "LambdaDelta-1/drop1/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/A/defs.ma".
+
+include "LambdaDelta-2/G/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/ex0/defs.ma".
+
+include "LambdaDelta-2/leq/defs.ma".
+
+include "LambdaDelta-2/aplus/props.ma".
+
+inline procedural "LambdaDelta-1/ex0/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/C/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/ex1/defs.ma".
+
+include "LambdaDelta-2/ty3/fwd.ma".
+
+include "LambdaDelta-2/pc3/fwd.ma".
+
+include "LambdaDelta-2/nf2/pr3.ma".
+
+include "LambdaDelta-2/nf2/props.ma".
+
+include "LambdaDelta-2/arity/defs.ma".
+
+include "LambdaDelta-2/leq/props.ma".
+
+inline procedural "LambdaDelta-1/ex1/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/C/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/ex2/defs.ma".
+
+include "LambdaDelta-2/nf2/defs.ma".
+
+include "LambdaDelta-2/pr2/fwd.ma".
+
+include "LambdaDelta-2/arity/fwd.ma".
+
+inline procedural "LambdaDelta-1/ex2/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/C/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/flt/defs.ma".
+
+include "LambdaDelta-2/C/props.ma".
+
+inline procedural "LambdaDelta-1/flt/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubst0/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/fsubst0/defs.ma".
+
+inline procedural "LambdaDelta-1/fsubst0/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/getl/props.ma".
+
+include "LambdaDelta-2/clear/drop.ma".
+
+inline procedural "LambdaDelta-1/getl/clear.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/getl/props.ma".
+
+inline procedural "LambdaDelta-1/getl/dec.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/drop/defs.ma".
+
+include "LambdaDelta-2/clear/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/getl/props.ma".
+
+include "LambdaDelta-2/clear/drop.ma".
+
+inline procedural "LambdaDelta-1/getl/drop.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/getl/fwd.ma".
+
+include "LambdaDelta-2/clear/props.ma".
+
+include "LambdaDelta-2/flt/props.ma".
+
+inline procedural "LambdaDelta-1/getl/flt.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/getl/defs.ma".
+
+include "LambdaDelta-2/drop/fwd.ma".
+
+include "LambdaDelta-2/clear/fwd.ma".
+
+inline procedural "LambdaDelta-1/getl/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/getl/drop.ma".
+
+include "LambdaDelta-2/getl/clear.ma".
+
+inline procedural "LambdaDelta-1/getl/getl.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/getl/fwd.ma".
+
+include "LambdaDelta-2/drop/props.ma".
+
+include "LambdaDelta-2/clear/props.ma".
+
+inline procedural "LambdaDelta-1/getl/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/T/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/iso/defs.ma".
+
+include "LambdaDelta-2/tlist/defs.ma".
+
+inline procedural "LambdaDelta-1/iso/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/iso/fwd.ma".
+
+inline procedural "LambdaDelta-1/iso/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/leq/props.ma".
+
+inline procedural "LambdaDelta-1/leq/asucc.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/aplus/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/leq/defs.ma".
+
+inline procedural "LambdaDelta-1/leq/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/leq/fwd.ma".
+
+include "LambdaDelta-2/aplus/props.ma".
+
+inline procedural "LambdaDelta-1/leq/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/tlist/defs.ma".
+
+include "LambdaDelta-2/s/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/lift/defs.ma".
+
+inline procedural "LambdaDelta-1/lift/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/lift/fwd.ma".
+
+include "LambdaDelta-2/s/props.ma".
+
+inline procedural "LambdaDelta-1/lift/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/lift/fwd.ma".
+
+include "LambdaDelta-2/tlt/props.ma".
+
+inline procedural "LambdaDelta-1/lift/tlt.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/lift/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/lift1/defs.ma".
+
+include "LambdaDelta-2/lift/fwd.ma".
+
+inline procedural "LambdaDelta-1/lift1/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/lift/props.ma".
+
+include "LambdaDelta-2/drop1/defs.ma".
+
+inline procedural "LambdaDelta-1/lift1/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/A/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/llt/defs.ma".
+
+include "LambdaDelta-2/leq/defs.ma".
+
+inline procedural "LambdaDelta-1/llt/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/G/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/next_plus/defs.ma".
+
+inline procedural "LambdaDelta-1/next_plus/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/nf2/fwd.ma".
+
+include "LambdaDelta-2/arity/subst0.ma".
+
+inline procedural "LambdaDelta-1/nf2/arity.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/nf2/defs.ma".
+
+include "LambdaDelta-2/pr2/clen.ma".
+
+include "LambdaDelta-2/pr2/fwd.ma".
+
+include "LambdaDelta-2/pr0/dec.ma".
+
+include "LambdaDelta-2/C/props.ma".
+
+inline procedural "LambdaDelta-1/nf2/dec.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr2/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/nf2/defs.ma".
+
+include "LambdaDelta-2/pr2/clen.ma".
+
+include "LambdaDelta-2/subst0/dec.ma".
+
+include "LambdaDelta-2/T/props.ma".
+
+inline procedural "LambdaDelta-1/nf2/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/nf2/pr3.ma".
+
+include "LambdaDelta-2/pr3/fwd.ma".
+
+include "LambdaDelta-2/iso/props.ma".
+
+inline procedural "LambdaDelta-1/nf2/iso.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/nf2/props.ma".
+
+include "LambdaDelta-2/drop1/fwd.ma".
+
+inline procedural "LambdaDelta-1/nf2/lift1.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/nf2/defs.ma".
+
+include "LambdaDelta-2/pr3/pr3.ma".
+
+inline procedural "LambdaDelta-1/nf2/pr3.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/nf2/defs.ma".
+
+include "LambdaDelta-2/pr2/fwd.ma".
+
+inline procedural "LambdaDelta-1/nf2/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr1/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pc1/defs.ma".
+
+include "LambdaDelta-2/pr1/pr1.ma".
+
+inline procedural "LambdaDelta-1/pc1/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/ty3/arity_props.ma".
+
+include "LambdaDelta-2/nf2/fwd.ma".
+
+inline procedural "LambdaDelta-1/pc3/dec.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr3/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pc3/left.ma".
+
+include "LambdaDelta-2/fsubst0/defs.ma".
+
+include "LambdaDelta-2/csubst0/getl.ma".
+
+inline procedural "LambdaDelta-1/pc3/fsubst0.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pc3/props.ma".
+
+include "LambdaDelta-2/pr3/fwd.ma".
+
+inline procedural "LambdaDelta-1/pc3/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pc3/props.ma".
+
+inline procedural "LambdaDelta-1/pc3/left.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pc3/defs.ma".
+
+include "LambdaDelta-2/nf2/pr3.ma".
+
+inline procedural "LambdaDelta-1/pc3/nf2.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pc3/defs.ma".
+
+include "LambdaDelta-2/pc1/defs.ma".
+
+include "LambdaDelta-2/pr3/pr1.ma".
+
+inline procedural "LambdaDelta-1/pc3/pc1.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pc3/defs.ma".
+
+include "LambdaDelta-2/pr3/pr3.ma".
+
+inline procedural "LambdaDelta-1/pc3/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pc3/props.ma".
+
+include "LambdaDelta-2/pr3/subst1.ma".
+
+inline procedural "LambdaDelta-1/pc3/subst1.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pc3/props.ma".
+
+include "LambdaDelta-2/wcpr0/getl.ma".
+
+inline procedural "LambdaDelta-1/pc3/wcpr0.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr0/fwd.ma".
+
+include "LambdaDelta-2/subst0/dec.ma".
+
+include "LambdaDelta-2/T/dec.ma".
+
+include "LambdaDelta-2/T/props.ma".
+
+inline procedural "LambdaDelta-1/pr0/dec.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/subst0/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr0/props.ma".
+
+inline procedural "LambdaDelta-1/pr0/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr0/fwd.ma".
+
+include "LambdaDelta-2/lift/tlt.ma".
+
+inline procedural "LambdaDelta-1/pr0/pr0.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr0/defs.ma".
+
+include "LambdaDelta-2/subst0/subst0.ma".
+
+inline procedural "LambdaDelta-1/pr0/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr0/props.ma".
+
+include "LambdaDelta-2/subst1/defs.ma".
+
+inline procedural "LambdaDelta-1/pr0/subst1.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr0/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr1/props.ma".
+
+include "LambdaDelta-2/pr0/pr0.ma".
+
+inline procedural "LambdaDelta-1/pr1/pr1.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr1/defs.ma".
+
+include "LambdaDelta-2/pr0/subst1.ma".
+
+include "LambdaDelta-2/subst1/props.ma".
+
+include "LambdaDelta-2/T/props.ma".
+
+inline procedural "LambdaDelta-1/pr1/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr2/props.ma".
+
+include "LambdaDelta-2/clen/getl.ma".
+
+inline procedural "LambdaDelta-1/pr2/clen.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr0/defs.ma".
+
+include "LambdaDelta-2/getl/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr2/defs.ma".
+
+include "LambdaDelta-2/pr0/fwd.ma".
+
+include "LambdaDelta-2/getl/drop.ma".
+
+include "LambdaDelta-2/getl/clear.ma".
+
+inline procedural "LambdaDelta-1/pr2/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr2/defs.ma".
+
+include "LambdaDelta-2/pr0/pr0.ma".
+
+include "LambdaDelta-2/getl/props.ma".
+
+inline procedural "LambdaDelta-1/pr2/pr2.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr2/defs.ma".
+
+include "LambdaDelta-2/pr0/props.ma".
+
+include "LambdaDelta-2/getl/drop.ma".
+
+include "LambdaDelta-2/getl/clear.ma".
+
+inline procedural "LambdaDelta-1/pr2/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr2/defs.ma".
+
+include "LambdaDelta-2/pr0/subst1.ma".
+
+include "LambdaDelta-2/pr0/fwd.ma".
+
+include "LambdaDelta-2/csubst1/getl.ma".
+
+include "LambdaDelta-2/csubst1/fwd.ma".
+
+include "LambdaDelta-2/subst1/subst1.ma".
+
+include "LambdaDelta-2/getl/drop.ma".
+
+inline procedural "LambdaDelta-1/pr2/subst1.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr2/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr3/props.ma".
+
+include "LambdaDelta-2/pr2/fwd.ma".
+
+inline procedural "LambdaDelta-1/pr3/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr3/fwd.ma".
+
+include "LambdaDelta-2/iso/props.ma".
+
+include "LambdaDelta-2/tlist/props.ma".
+
+inline procedural "LambdaDelta-1/pr3/iso.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr3/defs.ma".
+
+include "LambdaDelta-2/pr1/defs.ma".
+
+inline procedural "LambdaDelta-1/pr3/pr1.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr3/props.ma".
+
+include "LambdaDelta-2/pr2/pr2.ma".
+
+inline procedural "LambdaDelta-1/pr3/pr3.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr3/pr1.ma".
+
+include "LambdaDelta-2/pr2/props.ma".
+
+include "LambdaDelta-2/pr1/props.ma".
+
+inline procedural "LambdaDelta-1/pr3/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr3/defs.ma".
+
+include "LambdaDelta-2/pr2/subst1.ma".
+
+inline procedural "LambdaDelta-1/pr3/subst1.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr3/props.ma".
+
+include "LambdaDelta-2/wcpr0/getl.ma".
+
+inline procedural "LambdaDelta-1/pr3/wcpr0.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "Base-2/theory.ma".
+include "LambdaDelta-1/definitions.ma".
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/T/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/r/defs.ma".
+
+include "LambdaDelta-2/s/defs.ma".
+
+inline procedural "LambdaDelta-1/r/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/T/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/s/defs.ma".
+
+inline procedural "LambdaDelta-1/s/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubc/arity.ma".
+
+include "LambdaDelta-2/csubc/getl.ma".
+
+include "LambdaDelta-2/csubc/drop1.ma".
+
+include "LambdaDelta-2/csubc/props.ma".
+
+inline procedural "LambdaDelta-1/sc3/arity.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/sn3/defs.ma".
+
+include "LambdaDelta-2/arity/defs.ma".
+
+include "LambdaDelta-2/drop1/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/sc3/defs.ma".
+
+include "LambdaDelta-2/sn3/lift1.ma".
+
+include "LambdaDelta-2/nf2/lift1.ma".
+
+include "LambdaDelta-2/csuba/arity.ma".
+
+include "LambdaDelta-2/arity/lift1.ma".
+
+include "LambdaDelta-2/arity/aprem.ma".
+
+include "LambdaDelta-2/llt/props.ma".
+
+include "LambdaDelta-2/drop1/getl.ma".
+
+include "LambdaDelta-2/drop1/props.ma".
+
+include "LambdaDelta-2/lift1/props.ma".
+
+inline procedural "LambdaDelta-1/sc3/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr3/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/sn3/defs.ma".
+
+include "LambdaDelta-2/pr3/props.ma".
+
+inline procedural "LambdaDelta-1/sn3/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/sn3/props.ma".
+
+include "LambdaDelta-2/drop1/fwd.ma".
+
+include "LambdaDelta-2/lift1/fwd.ma".
+
+inline procedural "LambdaDelta-1/sn3/lift1.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/sn3/defs.ma".
+
+include "LambdaDelta-2/nf2/dec.ma".
+
+include "LambdaDelta-2/nf2/pr3.ma".
+
+inline procedural "LambdaDelta-1/sn3/nf2.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/sn3/nf2.ma".
+
+include "LambdaDelta-2/sn3/fwd.ma".
+
+include "LambdaDelta-2/nf2/iso.ma".
+
+include "LambdaDelta-2/pr3/iso.ma".
+
+inline procedural "LambdaDelta-1/sn3/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/G/defs.ma".
+
+include "LambdaDelta-2/getl/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/sty0/defs.ma".
+
+inline procedural "LambdaDelta-1/sty0/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/sty0/defs.ma".
+
+include "LambdaDelta-2/getl/drop.ma".
+
+inline procedural "LambdaDelta-1/sty0/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/sty1/props.ma".
+
+include "LambdaDelta-2/cnt/props.ma".
+
+inline procedural "LambdaDelta-1/sty1/cnt.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/sty0/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/sty1/defs.ma".
+
+include "LambdaDelta-2/sty0/props.ma".
+
+inline procedural "LambdaDelta-1/sty1/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/lift/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/subst/defs.ma".
+
+inline procedural "LambdaDelta-1/subst/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/subst/fwd.ma".
+
+include "LambdaDelta-2/subst0/defs.ma".
+
+include "LambdaDelta-2/lift/props.ma".
+
+inline procedural "LambdaDelta-1/subst/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/subst0/defs.ma".
+
+include "LambdaDelta-2/lift/props.ma".
+
+inline procedural "LambdaDelta-1/subst0/dec.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/lift/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/subst0/defs.ma".
+
+include "LambdaDelta-2/lift/props.ma".
+
+inline procedural "LambdaDelta-1/subst0/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/subst0/fwd.ma".
+
+inline procedural "LambdaDelta-1/subst0/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/subst0/props.ma".
+
+inline procedural "LambdaDelta-1/subst0/subst0.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/subst0/defs.ma".
+
+include "LambdaDelta-2/lift/props.ma".
+
+include "LambdaDelta-2/lift/tlt.ma".
+
+inline procedural "LambdaDelta-1/subst0/tlt.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/subst0/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/subst1/defs.ma".
+
+include "LambdaDelta-2/subst0/props.ma".
+
+inline procedural "LambdaDelta-1/subst1/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/subst1/defs.ma".
+
+include "LambdaDelta-2/subst0/props.ma".
+
+inline procedural "LambdaDelta-1/subst1/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/subst1/fwd.ma".
+
+include "LambdaDelta-2/subst0/subst0.ma".
+
+inline procedural "LambdaDelta-1/subst1/subst1.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/subst0/tlt.ma".
+
+include "LambdaDelta-2/subst/props.ma".
+
+include "LambdaDelta-2/sty1/cnt.ma".
+
+include "LambdaDelta-2/ex0/props.ma".
+
+include "LambdaDelta-2/wcpr0/fwd.ma".
+
+include "LambdaDelta-2/pr3/wcpr0.ma".
+
+include "LambdaDelta-2/ex2/props.ma".
+
+include "LambdaDelta-2/ex1/props.ma".
+
+include "LambdaDelta-2/ty3/sty0.ma".
+
+include "LambdaDelta-2/csubt/csuba.ma".
+
+include "LambdaDelta-2/ty3/fwd_nf2.ma".
+
+include "LambdaDelta-2/ty3/nf2.ma".
+
+include "LambdaDelta-2/wf3/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/T/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/tlist/defs.ma".
+
+inline procedural "LambdaDelta-1/tlist/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/T/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/tlt/defs.ma".
+
+inline procedural "LambdaDelta-1/tlt/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/ty3/pr3_props.ma".
+
+include "LambdaDelta-2/arity/pr3.ma".
+
+include "LambdaDelta-2/asucc/fwd.ma".
+
+inline procedural "LambdaDelta-1/ty3/arity.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/ty3/arity.ma".
+
+include "LambdaDelta-2/sc3/arity.ma".
+
+inline procedural "LambdaDelta-1/ty3/arity_props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pc3/dec.ma".
+
+include "LambdaDelta-2/getl/flt.ma".
+
+include "LambdaDelta-2/getl/dec.ma".
+
+inline procedural "LambdaDelta-1/ty3/dec.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/G/defs.ma".
+
+include "LambdaDelta-2/pc3/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/ty3/props.ma".
+
+include "LambdaDelta-2/pc3/fsubst0.ma".
+
+include "LambdaDelta-2/getl/getl.ma".
+
+inline procedural "LambdaDelta-1/ty3/fsubst0.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/ty3/defs.ma".
+
+include "LambdaDelta-2/pc3/props.ma".
+
+inline procedural "LambdaDelta-1/ty3/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/ty3/arity_props.ma".
+
+include "LambdaDelta-2/pc3/nf2.ma".
+
+include "LambdaDelta-2/nf2/fwd.ma".
+
+inline procedural "LambdaDelta-1/ty3/fwd_nf2.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/ty3/arity.ma".
+
+include "LambdaDelta-2/pc3/nf2.ma".
+
+include "LambdaDelta-2/nf2/arity.ma".
+
+inline procedural "LambdaDelta-1/ty3/nf2.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/csubt/ty3.ma".
+
+include "LambdaDelta-2/ty3/subst1.ma".
+
+include "LambdaDelta-2/ty3/fsubst0.ma".
+
+include "LambdaDelta-2/pc3/pc1.ma".
+
+include "LambdaDelta-2/pc3/wcpr0.ma".
+
+include "LambdaDelta-2/pc1/props.ma".
+
+inline procedural "LambdaDelta-1/ty3/pr3.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/ty3/pr3.ma".
+
+inline procedural "LambdaDelta-1/ty3/pr3_props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/ty3/fwd.ma".
+
+include "LambdaDelta-2/pc3/fwd.ma".
+
+inline procedural "LambdaDelta-1/ty3/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/ty3/pr3_props.ma".
+
+include "LambdaDelta-2/sty0/fwd.ma".
+
+inline procedural "LambdaDelta-1/ty3/sty0.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/ty3/props.ma".
+
+include "LambdaDelta-2/pc3/subst1.ma".
+
+include "LambdaDelta-2/getl/getl.ma".
+
+inline procedural "LambdaDelta-1/ty3/subst1.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/pr0/defs.ma".
+
+include "LambdaDelta-2/C/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/wcpr0/defs.ma".
+
+inline procedural "LambdaDelta-1/wcpr0/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/wcpr0/defs.ma".
+
+include "LambdaDelta-2/getl/props.ma".
+
+inline procedural "LambdaDelta-1/wcpr0/getl.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/wf3/fwd.ma".
+
+inline procedural "LambdaDelta-1/wf3/clear.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/ty3/defs.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/wf3/defs.ma".
+
+inline procedural "LambdaDelta-1/wf3/fwd.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/wf3/clear.ma".
+
+include "LambdaDelta-2/ty3/dec.ma".
+
+inline procedural "LambdaDelta-1/wf3/getl.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/wf3/ty3.ma".
+
+include "LambdaDelta-2/app/defs.ma".
+
+inline procedural "LambdaDelta-1/wf3/props.ma".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "LambdaDelta-2/wf3/getl.ma".
+
+inline procedural "LambdaDelta-1/wf3/ty3.ma".
+
LOG = log.txt
-DIRS = Legacy-2 Base-2
+DIRS = Legacy-2 Base-2 LambdaDelta-2
SILENTMAKE = $(H)$(MAKE) H=$(H) -s --no-print-directory
$(H)$(BIN)matitaclean.opt $(MATITAOPTIONS) $(MAS)
$(H)$(RM) $(MAS) depends
+
+clean.mma:
+# $(H)for FILE in */*.mma ; do if [ -e ../LambdaDelta-1/$${FILE/.mma/.ma} ] ; then true ; else rm $$FILE ; fi done
+
depend:
@echo matitadep
- $(H)$(BIN)matitadep $(foreach DIR, $(DIRS), -exclude $(DIR)/theory.ma) -exclude LambdaDelta-2/theory.ma
+ $(H)$(BIN)matitadep $(foreach DIR, $(DIRS), -exclude $(DIR)/theory.ma)
$(H)cat $(DIRS:%=%/depends) >> depends
depend.opt:
@echo matitadep.opt
- $(H)$(BIN)matitadep.opt $(foreach DIR, $(DIRS), -exclude $(DIR)/theory.ma) -exclude LambdaDelta-2/theory.ma
+ $(H)$(BIN)matitadep.opt $(foreach DIR, $(DIRS), -exclude $(DIR)/theory.ma)
$(H)cat $(DIRS:%=%/depends) >> depends
depends: depend.opt
$(H)$(BIN)matitac.opt $(MATITAOPTIONS) -dump $@ $< 2>> $(LOG)
$(H)echo $@ `$(BIN)matitadep.opt -stdout $@` >> depends
-include Legacy-2/.depend
-include Base-2/.depend
+$(foreach DIR, $(DIRS), $(eval include $(DIR)/.depend))