]>
matita.cs.unibo.it Git - helm.git/blobdiff - helm/coq-contribs/LAMBDA-TYPES/Make
lift_gen.v
lift_props.v
lift_tlt.v
lift_gen.v
lift_props.v
lift_tlt.v
+drop_defs.v
+drop_props.v
subst0_defs.v
subst0_gen.v
subst0_lift.v
subst0_defs.v
subst0_gen.v
subst0_lift.v
subst1_lift.v
subst1_subst1.v
subst1_confluence.v
subst1_lift.v
subst1_subst1.v
subst1_confluence.v
-drop_defs.v
-drop_props.v
csubst0_defs.v
csubst1_defs.v
csubst0_defs.v
csubst1_defs.v
pr0_defs.v
pr0_lift.v
pr0_gen.v
pr0_defs.v
pr0_lift.v
pr0_gen.v
pr0_subst1.v
pr1_defs.v
pr1_confluence.v
pr0_subst1.v
pr1_defs.v
pr1_confluence.v
pr2_defs.v
pr2_lift.v
pr2_gen.v
pr2_defs.v
pr2_lift.v
pr2_gen.v
pr3_confluence.v
pr3_subst1.v
pr3_gen_context.v
pr3_confluence.v
pr3_subst1.v
pr3_gen_context.v
-cpr0_defs.v
-cpr0_props.v
pc3_defs.v
pc3_props.v
pc3_gen.v
pc3_subst0.v
pc3_gen_context.v
ty0_defs.v
pc3_defs.v
pc3_props.v
pc3_gen.v
pc3_subst0.v
pc3_gen_context.v
ty0_defs.v
ty0_lift.v
ty0_props.v
ty0_subst0.v
ty0_gen_context.v
csub0_defs.v
ty0_lift.v
ty0_props.v
ty0_subst0.v
ty0_gen_context.v
csub0_defs.v
ty0_sred.v
ty0_sred_props.v
LambdaDelta.v
ty0_sred.v
ty0_sred_props.v
LambdaDelta.v