+Require Export base_tactics.
+Require Export base_hints.
+Require Export base_types.
+Require Export base_blt.
+Require Export base_rewrite.
+Require Export Base.
Require Export terms_defs.
Require Export tlt_defs.
Require Export contexts_defs.
Require Export lift_gen.
Require Export lift_props.
Require Export lift_tlt.
+Require Export drop_defs.
+Require Export drop_props.
Require Export subst0_defs.
Require Export subst0_gen.
Require Export subst0_lift.
Require Export subst1_lift.
Require Export subst1_subst1.
Require Export subst1_confluence.
-Require Export drop_defs.
-Require Export drop_props.
Require Export csubst0_defs.
Require Export csubst1_defs.
+Require Export fsubst0_defs.
Require Export pr0_defs.
Require Export pr0_lift.
Require Export pr0_gen.
Require Export pr0_subst1.
Require Export pr1_defs.
Require Export pr1_confluence.
+Require Export cpr0_defs.
Require Export pr2_defs.
Require Export pr2_lift.
Require Export pr2_gen.
Require Export pr3_confluence.
Require Export pr3_subst1.
Require Export pr3_gen_context.
-Require Export cpr0_defs.
-Require Export cpr0_props.
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 ty0_defs.
+Require Export ty0_gen.
Require Export ty0_lift.
Require Export ty0_props.
Require Export ty0_subst0.
Require Export ty0_gen_context.
Require Export csub0_defs.
+Require Export csub0_props.
Require Export ty0_sred.
Require Export ty0_sred_props.