(****************************************************************************)
(*                                                                          *)
(*                The formal system \lambda\delta                           *)
(*                                                                          *)
(*                Author: Ferruccio Guidi                                   *)
(*                                                                          *)
(*                This file is distributed under the terms of the           *)
(*                GNU General Public License Version 2                      *)
(*                                                                          *)
(****************************************************************************)

Require Export terms_defs.
Require Export tlist_defs.
Require Export tlt_defs.
Require Export iso_defs.
Require Export contexts_defs.
Require Export clt_defs.
Require Export ctail_defs.
Require Export flt_defs.
Require Export app_defs.
Require Export lift_defs.
Require Export lift_gen.
Require Export lift_props.
Require Export lift_tlt.
Require Export lift1_defs.
Require Export lift1_props.
Require Export cnt_defs.
Require Export drop_defs.
Require Export drop_props.
Require Export drop1_defs.
Require Export drop1_props.
Require Export getl_defs.
Require Export getl_props.
Require Export csubv_defs.
Require Export subst0_defs.
Require Export subst0_gen.
Require Export subst0_lift.
Require Export subst0_subst0.
Require Export subst0_confluence.
Require Export subst0_tlt.
Require Export dnf_dec.
Require Export subst1_defs.
Require Export subst1_gen.
Require Export subst1_lift.
Require Export subst1_subst1.
Require Export subst1_confluence.
Require Export subst_defs.
Require Export subst_props.
Require Export csubst0_defs.
Require Export csubst1_defs.
Require Export csubst1_props.
Require Export fsubst0_defs.
Require Export parameter_defs.
Require Export sty0_defs.
Require Export sty0_props.
Require Export sty1_defs.
Require Export sty1_props.
Require Export levels_defs.
Require Export llt_defs.
Require Export aprem_defs.
Require Export levels_ex0.
Require Export arity_defs.
Require Export arity_gen.
Require Export arity_props.
Require Export arity_subst0.
Require Export pr0_defs.
Require Export pr0_lift.
Require Export pr0_gen.
Require Export pr0_subst0.
Require Export pr0_confluence.
Require Export pr0_subst1.
Require Export nf0_dec.
Require Export pr1_defs.
Require Export pr1_props.
Require Export pr1_confluence.
Require Export wcpr0_defs.
Require Export pr2_defs.
Require Export pr2_lift.
Require Export pr2_gen.
Require Export pr2_confluence.
Require Export pr2_subst1.
Require Export pr2_gen_context.
Require Export pr3_defs.
Require Export pr3_props.
Require Export pr3_gen.
Require Export pr3_confluence.
Require Export pr3_subst1.
Require Export pr3_gen_context.
Require Export pr3_iso.
Require Export csuba_defs.
Require Export csuba_props.
Require Export arity_sred.
Require Export nf2_defs.
Require Export nf2_ex2.
Require Export nf2_gen.
Require Export nf2_props.
Require Export nf2_dec.
Require Export sn3_defs.
Require Export sn3_gen.
Require Export sn3_props.
Require Export sc3_defs.
Require Export sc3_props.
Require Export csubc_defs.
Require Export csubc_props.
Require Export sc3_arity.
Require Export pc1_defs.
Require Export pc1_props.
Require Export pc3_defs.
Require Export pc3_props.
Require Export pc3_gen.
Require Export pc3_subst0.
Require Export pc3_gen_context.
Require Export ty3_defs.
Require Export ty3_gen.
Require Export ty3_ex1.
Require Export ty3_lift.
Require Export ty3_props.
Require Export ty3_subst0.
Require Export ty3_gen_context.
Require Export csubt_defs.
Require Export csubt_props.
Require Export ty3_sred.
Require Export ty3_sred_props.
Require Export ty3_arity_props.
Require Export csubt_arity_props.
Require Export ty3_gen_nf2.
Require Export ty3_nf2_gen.
Require Export ty3_dec.
Require Export wf3_defs.
Require Export wf3_props.