From e8998d29ab83e7b6aa495a079193705b2f6743d3 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 25 Dec 2012 21:48:14 +0000 Subject: [PATCH] - lambda_delta: programmed renaming to lambdadelta - nat: general weight-based eliminator added for lambdadelta --- .../contribs/{lambda_delta => lambdadelta}/Makefile | 0 .../apps_2/functional/dsubst.ma | 0 .../apps_2/functional/lift.ma | 0 .../apps_2/functional/notation.ma | 0 .../apps_2/functional/rtm.ma | 0 .../apps_2/functional/rtm_step.ma | 0 .../basic_2/basic_1.orig | 0 .../basic_2/basic_1.txt | 0 .../basic_2/computation/acp.ma | 0 .../basic_2/computation/acp_aaa.ma | 0 .../basic_2/computation/acp_cr.ma | 0 .../basic_2/computation/cpe.ma | 0 .../basic_2/computation/cpe_cpe.ma | 0 .../basic_2/computation/cprs.ma | 0 .../basic_2/computation/cprs_aaa.ma | 0 .../basic_2/computation/cprs_cprs.ma | 0 .../basic_2/computation/cprs_delift.ma | 0 .../basic_2/computation/cprs_lfpr.ma | 0 .../basic_2/computation/cprs_lfprs.ma | 0 .../basic_2/computation/cprs_lift.ma | 0 .../basic_2/computation/cprs_ltpr.ma | 0 .../basic_2/computation/cprs_tstc.ma | 0 .../basic_2/computation/cprs_tstc_vector.ma | 0 .../basic_2/computation/csn.ma | 0 .../basic_2/computation/csn_aaa.ma | 0 .../basic_2/computation/csn_alt.ma | 0 .../basic_2/computation/csn_cpr.ma | 0 .../basic_2/computation/csn_cpr_vector.ma | 0 .../basic_2/computation/csn_lfpr.ma | 0 .../basic_2/computation/csn_lift.ma | 0 .../basic_2/computation/csn_tstc_vector.ma | 0 .../basic_2/computation/csn_vector.ma | 0 .../basic_2/computation/fprs.ma | 0 .../basic_2/computation/fprs_aaa.ma | 0 .../basic_2/computation/fprs_cprs.ma | 0 .../basic_2/computation/fprs_fprs.ma | 0 .../basic_2/computation/lfprs.ma | 0 .../basic_2/computation/lfprs_aaa.ma | 0 .../basic_2/computation/lfprs_cprs.ma | 0 .../basic_2/computation/lfprs_lfprs.ma | 0 .../basic_2/computation/lsubc.ma | 0 .../basic_2/computation/lsubc_ldrop.ma | 0 .../basic_2/computation/lsubc_ldrops.ma | 0 .../basic_2/computation/lsubc_lsuba.ma | 0 .../basic_2/computation/ltprs.ma | 0 .../basic_2/computation/ltprs_alt.ma | 0 .../basic_2/computation/ltprs_ldrop.ma | 0 .../basic_2/computation/ltprs_ltprs.ma | 0 .../basic_2/computation/tprs.ma | 0 .../basic_2/computation/tprs_lift.ma | 0 .../basic_2/computation/tprs_tprs.ma | 0 .../basic_2/computation/xprs.ma | 0 .../basic_2/computation/xprs_aaa.ma | 0 .../basic_2/computation/xprs_cprs.ma | 0 .../basic_2/computation/xprs_lift.ma | 0 .../basic_2/computation/xprs_lsubss.ma | 0 .../basic_2/computation/xprs_xprs.ma | 0 .../basic_2/conversion/cpc.ma | 0 .../basic_2/conversion/cpc_cpc.ma | 0 .../basic_2/conversion/fpc.ma | 0 .../basic_2/conversion/fpc_fpc.ma | 0 .../basic_2/conversion/lfpc.ma | 0 .../basic_2/conversion/lfpc_lfpc.ma | 0 .../basic_2/dynamic/snv.ma | 0 .../basic_2/dynamic/snv_aaa.ma | 0 .../basic_2/dynamic/snv_lift.ma | 0 .../basic_2/dynamic/snv_ssta.ma | 0 .../basic_2/equivalence/cpcs.ma | 0 .../basic_2/equivalence/cpcs_aaa.ma | 0 .../basic_2/equivalence/cpcs_cpcs.ma | 0 .../basic_2/equivalence/cpcs_cprs.ma | 0 .../basic_2/equivalence/cpcs_delift.ma | 0 .../basic_2/equivalence/cpcs_ltpr.ma | 0 .../basic_2/equivalence/cpcs_ltpss.ma | 0 .../basic_2/equivalence/fpcs.ma | 0 .../basic_2/equivalence/fpcs_aaa.ma | 0 .../basic_2/equivalence/fpcs_cpcs.ma | 0 .../basic_2/equivalence/fpcs_fpcs.ma | 0 .../basic_2/equivalence/fpcs_fprs.ma | 0 .../basic_2/equivalence/lfpcs.ma | 0 .../basic_2/equivalence/lfpcs_aaa.ma | 0 .../basic_2/equivalence/lfpcs_lfpcs.ma | 0 .../basic_2/equivalence/lfpcs_lfprs.ma | 0 .../basic_2/equivalence/lsubse.ma | 0 .../basic_2/equivalence/lsubse_cpcs.ma | 0 .../basic_2/equivalence/lsubse_ldrop.ma | 0 .../basic_2/equivalence/lsubse_ssta.ma | 0 .../basic_2/etc/csup/csup.etc | 0 .../basic_2/etc/csup/csup_csup.etc | 0 .../basic_2/etc/csup/csupp.etc | 0 .../basic_2/etc/csup/csupp_csupp.etc | 0 .../basic_2/etc/csup/csups.etc | 0 .../basic_2/etc/csup/csups_csups.etc | 0 .../basic_2/etc/csup/ypr.etc | 0 .../basic_2/etc/csup/yprs.etc | 0 .../basic_2/etc/csup/yprs_csups.etc | 0 .../basic_2/etc/csup/yprs_xprs.etc | 0 .../basic_2/etc/csup/yprs_yprs.etc | 0 .../basic_2/etc/csup/ysteps.etc | 0 .../basic_2/etc/csup/ysteps_csups.etc | 0 .../basic_2/etc/hod/ntas.etc | 0 .../basic_2/etc/hod/ntas_lift.etc | 0 .../basic_2/etc/lenv_px/lcpcs.etc | 0 .../basic_2/etc/lenv_px/lcpcs_ltpr.etc | 0 .../basic_2/etc/lenv_px/lenv_px_sn.etc | 0 .../basic_2/etc/lsubn/lsubn_lsubn.etc | 0 .../basic_2/etc/lsubsv/lsubsv.etc | 0 .../basic_2/etc/lsubsv/lsubsv_cpcs.etc | 0 .../basic_2/etc/lsubsv/lsubsv_ldrop.etc | 0 .../basic_2/etc/lsubsv/lsubsv_snv.etc | 0 .../basic_2/etc/lsubsv/lsubsv_ssta.etc | 0 .../basic_2/etc/nta/lsubn.etc | 0 .../basic_2/etc/nta/lsubn_cpcs.etc | 0 .../basic_2/etc/nta/lsubn_ldrop.etc | 0 .../basic_2/etc/nta/lsubn_nta.etc | 0 .../basic_2/etc/nta/nta.etc | 0 .../basic_2/etc/nta/nta_aaa.etc | 0 .../basic_2/etc/nta/nta_alt.etc | 0 .../basic_2/etc/nta/nta_lift.etc | 0 .../basic_2/etc/nta/nta_ltpr.etc | 0 .../basic_2/etc/nta/nta_ltpss.etc | 0 .../basic_2/etc/nta/nta_nta.etc | 0 .../basic_2/etc/nta/nta_sta.etc | 0 .../basic_2/etc/nta/nta_thin.etc | 0 .../basic_2/etc/snta/lsubsn.etc | 0 .../basic_2/etc/snta/lsubsn_cpcs.etc | 0 .../basic_2/etc/snta/lsubsn_ldrop.etc | 0 .../basic_2/etc/snta/lsubsn_snta.etc | 0 .../basic_2/etc/snta/snta.etc | 0 .../basic_2/etc/snta/snta_lift.etc | 0 .../basic_2/etc/snta/snta_ltpr.etc | 0 .../basic_2/etc/snta/snta_ltpss.etc | 0 .../basic_2/etc/snta/snta_snta.etc | 0 .../basic_2/etc/snta/snta_thin.etc | 0 .../basic_2/etc/sstas/sstas.etc | 0 .../basic_2/etc/sstas/sstas_lift.etc | 0 .../basic_2/etc/sstas/sstas_ltpss.etc | 0 .../basic_2/etc/sstas/sstas_sstas.etc | 0 .../basic_2/etc/sta/sta.etc | 0 .../basic_2/etc/sta/sta_lift.etc | 0 .../basic_2/etc/sta/sta_ltpss.etc | 0 .../basic_2/etc/sta/sta_sta.etc | 0 .../basic_2/etc/top/lenv_top.etc | 0 .../basic_2/grammar/aarity.ma | 0 .../basic_2/grammar/cl_shift.ma | 0 .../basic_2/grammar/cl_weight.ma | 0 .../basic_2/grammar/genv.ma | 0 .../basic_2/grammar/item.ma | 0 .../basic_2/grammar/lenv.ma | 0 .../basic_2/grammar/lenv_append.ma | 0 .../basic_2/grammar/lenv_length.ma | 0 .../basic_2/grammar/lenv_px.ma | 0 .../basic_2/grammar/lenv_px_bi.ma | 0 .../basic_2/grammar/lenv_weight.ma | 0 .../basic_2/grammar/term.ma | 0 .../basic_2/grammar/term_simple.ma | 0 .../basic_2/grammar/term_vector.ma | 0 .../basic_2/grammar/term_weight.ma | 0 .../basic_2/grammar/tshf.ma | 0 .../basic_2/grammar/tstc.ma | 0 .../basic_2/grammar/tstc_tstc.ma | 0 .../basic_2/grammar/tstc_vector.ma | 0 .../{lambda_delta => lambdadelta}/basic_2/names.txt | 0 .../basic_2/notation.ma | 0 .../basic_2/reducibility/cfpr.ma | 0 .../basic_2/reducibility/cfpr_aaa.ma | 0 .../basic_2/reducibility/cfpr_cfpr.ma | 0 .../basic_2/reducibility/cfpr_cpr.ma | 0 .../basic_2/reducibility/cfpr_ltpss.ma | 0 .../basic_2/reducibility/cif.ma | 0 .../basic_2/reducibility/cif_append.ma | 0 .../basic_2/reducibility/cnf.ma | 0 .../basic_2/reducibility/cnf_cif.ma | 0 .../basic_2/reducibility/cnf_lift.ma | 0 .../basic_2/reducibility/cpr.ma | 0 .../basic_2/reducibility/cpr_aaa.ma | 0 .../basic_2/reducibility/cpr_cpr.ma | 0 .../basic_2/reducibility/cpr_delift.ma | 0 .../basic_2/reducibility/cpr_lift.ma | 0 .../basic_2/reducibility/cpr_ltpr.ma | 0 .../basic_2/reducibility/cpr_ltpss.ma | 0 .../basic_2/reducibility/cpr_tpss.ma | 0 .../basic_2/reducibility/crf.ma | 0 .../basic_2/reducibility/crf_append.ma | 0 .../basic_2/reducibility/fpr.ma | 0 .../basic_2/reducibility/fpr_cpr.ma | 0 .../basic_2/reducibility/fpr_fpr.ma | 0 .../basic_2/reducibility/lfpr.ma | 0 .../basic_2/reducibility/lfpr_aaa.ma | 0 .../basic_2/reducibility/lfpr_alt.ma | 0 .../basic_2/reducibility/lfpr_cpr.ma | 0 .../basic_2/reducibility/lfpr_fpr.ma | 0 .../basic_2/reducibility/lfpr_lfpr.ma | 0 .../basic_2/reducibility/ltpr.ma | 0 .../basic_2/reducibility/ltpr_aaa.ma | 0 .../basic_2/reducibility/ltpr_ldrop.ma | 0 .../basic_2/reducibility/ltpr_ltpr.ma | 0 .../basic_2/reducibility/ltpr_ltpss_dx.ma | 0 .../basic_2/reducibility/ltpr_ltpss_sn.ma | 0 .../basic_2/reducibility/ltpr_tps.ma | 0 .../basic_2/reducibility/thnf.ma | 0 .../basic_2/reducibility/tpr.ma | 0 .../basic_2/reducibility/tpr_delift.ma | 0 .../basic_2/reducibility/tpr_lift.ma | 0 .../basic_2/reducibility/tpr_tpr.ma | 0 .../basic_2/reducibility/tpr_tps.ma | 0 .../basic_2/reducibility/tpr_tpss.ma | 0 .../basic_2/reducibility/xpr.ma | 0 .../basic_2/reducibility/xpr_aaa.ma | 0 .../basic_2/reducibility/xpr_lift.ma | 0 .../basic_2/reducibility/xpr_lsubss.ma | 0 .../basic_2/static/aaa.ma | 0 .../basic_2/static/aaa_aaa.ma | 0 .../basic_2/static/aaa_lift.ma | 0 .../basic_2/static/aaa_lifts.ma | 0 .../basic_2/static/aaa_ltpss_dx.ma | 0 .../basic_2/static/aaa_ltpss_sn.ma | 0 .../basic_2/static/lsuba.ma | 0 .../basic_2/static/lsuba_aaa.ma | 0 .../basic_2/static/lsuba_ldrop.ma | 0 .../basic_2/static/lsuba_lsuba.ma | 0 .../basic_2/static/lsubss.ma | 0 .../basic_2/static/lsubss_ldrop.ma | 0 .../basic_2/static/lsubss_lsubss.ma | 0 .../basic_2/static/lsubss_ssta.ma | 0 .../basic_2/static/sd.ma | 0 .../basic_2/static/sh.ma | 0 .../basic_2/static/ssta.ma | 0 .../basic_2/static/ssta_aaa.ma | 0 .../basic_2/static/ssta_lift.ma | 0 .../basic_2/static/ssta_ltpss_dx.ma | 0 .../basic_2/static/ssta_ltpss_sn.ma | 0 .../basic_2/static/ssta_ssta.ma | 0 .../basic_2/substitution/frsup.ma | 0 .../basic_2/substitution/gdrop.ma | 0 .../basic_2/substitution/gdrop_gdrop.ma | 0 .../basic_2/substitution/ldrop.ma | 0 .../basic_2/substitution/ldrop_append.ma | 0 .../basic_2/substitution/ldrop_ldrop.ma | 0 .../basic_2/substitution/ldrop_lpx.ma | 0 .../basic_2/substitution/ldrop_sfr.ma | 0 .../basic_2/substitution/lift.ma | 0 .../basic_2/substitution/lift_lift.ma | 0 .../basic_2/substitution/lift_lift_vector.ma | 0 .../basic_2/substitution/lift_vector.ma | 0 .../basic_2/substitution/lsubs.ma | 0 .../basic_2/substitution/lsubs_sfr.ma | 0 .../basic_2/substitution/tps.ma | 0 .../basic_2/substitution/tps_lift.ma | 0 .../basic_2/substitution/tps_tps.ma | 0 .../basic_2/unfold/delift.ma | 0 .../basic_2/unfold/delift_alt.ma | 0 .../basic_2/unfold/delift_delift.ma | 0 .../basic_2/unfold/delift_lift.ma | 0 .../basic_2/unfold/delift_ltpss.ma | 0 .../basic_2/unfold/delift_tpss.ma | 0 .../basic_2/unfold/frsupp.ma | 0 .../basic_2/unfold/frsupp_frsupp.ma | 0 .../basic_2/unfold/frsups.ma | 0 .../basic_2/unfold/frsups_frsups.ma | 0 .../basic_2/unfold/gr2.ma | 0 .../basic_2/unfold/gr2_gr2.ma | 0 .../basic_2/unfold/gr2_minus.ma | 0 .../basic_2/unfold/gr2_plus.ma | 0 .../basic_2/unfold/ldrops.ma | 0 .../basic_2/unfold/ldrops_ldrop.ma | 0 .../basic_2/unfold/ldrops_ldrops.ma | 0 .../basic_2/unfold/lifts.ma | 0 .../basic_2/unfold/lifts_lift.ma | 0 .../basic_2/unfold/lifts_lift_vector.ma | 0 .../basic_2/unfold/lifts_lifts.ma | 0 .../basic_2/unfold/lifts_vector.ma | 0 .../basic_2/unfold/ltpss_dx.ma | 0 .../basic_2/unfold/ltpss_dx_ldrop.ma | 0 .../basic_2/unfold/ltpss_dx_ltpss_dx.ma | 0 .../basic_2/unfold/ltpss_dx_tps.ma | 0 .../basic_2/unfold/ltpss_dx_tpss.ma | 0 .../basic_2/unfold/ltpss_sn.ma | 0 .../basic_2/unfold/ltpss_sn_alt.ma | 0 .../basic_2/unfold/ltpss_sn_ldrop.ma | 0 .../basic_2/unfold/ltpss_sn_ltpss_sn.ma | 0 .../basic_2/unfold/ltpss_sn_tps.ma | 0 .../basic_2/unfold/ltpss_sn_tpss.ma | 0 .../basic_2/unfold/thin.ma | 0 .../basic_2/unfold/thin_delift.ma | 0 .../basic_2/unfold/thin_ldrop.ma | 0 .../basic_2/unfold/tpss.ma | 0 .../basic_2/unfold/tpss_alt.ma | 0 .../basic_2/unfold/tpss_lift.ma | 0 .../basic_2/unfold/tpss_tpss.ma | 0 .../{lambda_delta => lambdadelta}/ground_2/arith.ma | 0 .../{lambda_delta => lambdadelta}/ground_2/list.ma | 0 .../ground_2/notation.ma | 0 .../{lambda_delta => lambdadelta}/ground_2/star.ma | 0 .../ground_2/xoa.conf.xml | 0 .../{lambda_delta => lambdadelta}/ground_2/xoa.ma | 0 .../ground_2/xoa_notation.ma | 0 .../ground_2/xoa_props.ma | 0 .../{lambda_delta => lambdadelta}/ma2etc.sh | 0 .../contribs/{lambda_delta => lambdadelta}/orig.sh | 0 .../{lambda_delta => lambdadelta}/replace.sh | 0 .../contribs/{lambda_delta => lambdadelta}/root | 0 matita/matita/lib/arithmetics/nat.ma | 13 +++++++++++++ 303 files changed, 13 insertions(+) rename matita/matita/contribs/{lambda_delta => lambdadelta}/Makefile (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/apps_2/functional/dsubst.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/apps_2/functional/lift.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/apps_2/functional/notation.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/apps_2/functional/rtm.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/apps_2/functional/rtm_step.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/basic_1.orig (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/basic_1.txt (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/acp.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/acp_aaa.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/acp_cr.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/cpe.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/cpe_cpe.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/cprs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/cprs_aaa.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/cprs_cprs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/cprs_delift.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/cprs_lfpr.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/cprs_lfprs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/cprs_lift.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/cprs_ltpr.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/cprs_tstc.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/cprs_tstc_vector.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/csn.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/csn_aaa.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/csn_alt.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/csn_cpr.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/csn_cpr_vector.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/csn_lfpr.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/csn_lift.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/csn_tstc_vector.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/csn_vector.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/fprs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/fprs_aaa.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/fprs_cprs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/fprs_fprs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/lfprs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/lfprs_aaa.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/lfprs_cprs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/lfprs_lfprs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/lsubc.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/lsubc_ldrop.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/lsubc_ldrops.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/lsubc_lsuba.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/ltprs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/ltprs_alt.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/ltprs_ldrop.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/ltprs_ltprs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/tprs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/tprs_lift.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/tprs_tprs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/xprs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/xprs_aaa.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/xprs_cprs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/xprs_lift.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/xprs_lsubss.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/computation/xprs_xprs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/conversion/cpc.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/conversion/cpc_cpc.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/conversion/fpc.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/conversion/fpc_fpc.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/conversion/lfpc.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/conversion/lfpc_lfpc.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/dynamic/snv.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/dynamic/snv_aaa.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/dynamic/snv_lift.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/dynamic/snv_ssta.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/equivalence/cpcs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/equivalence/cpcs_aaa.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/equivalence/cpcs_cpcs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/equivalence/cpcs_cprs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/equivalence/cpcs_delift.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/equivalence/cpcs_ltpr.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/equivalence/cpcs_ltpss.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/equivalence/fpcs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/equivalence/fpcs_aaa.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/equivalence/fpcs_cpcs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/equivalence/fpcs_fpcs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/equivalence/fpcs_fprs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/equivalence/lfpcs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/equivalence/lfpcs_aaa.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/equivalence/lfpcs_lfpcs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/equivalence/lfpcs_lfprs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/equivalence/lsubse.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/equivalence/lsubse_cpcs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/equivalence/lsubse_ldrop.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/equivalence/lsubse_ssta.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/csup/csup.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/csup/csup_csup.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/csup/csupp.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/csup/csupp_csupp.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/csup/csups.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/csup/csups_csups.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/csup/ypr.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/csup/yprs.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/csup/yprs_csups.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/csup/yprs_xprs.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/csup/yprs_yprs.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/csup/ysteps.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/csup/ysteps_csups.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/hod/ntas.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/hod/ntas_lift.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/lenv_px/lcpcs.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/lenv_px/lcpcs_ltpr.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/lenv_px/lenv_px_sn.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/lsubn/lsubn_lsubn.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/lsubsv/lsubsv.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/lsubsv/lsubsv_cpcs.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/lsubsv/lsubsv_ldrop.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/lsubsv/lsubsv_snv.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/lsubsv/lsubsv_ssta.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/nta/lsubn.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/nta/lsubn_cpcs.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/nta/lsubn_ldrop.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/nta/lsubn_nta.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/nta/nta.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/nta/nta_aaa.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/nta/nta_alt.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/nta/nta_lift.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/nta/nta_ltpr.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/nta/nta_ltpss.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/nta/nta_nta.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/nta/nta_sta.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/nta/nta_thin.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/snta/lsubsn.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/snta/lsubsn_cpcs.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/snta/lsubsn_ldrop.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/snta/lsubsn_snta.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/snta/snta.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/snta/snta_lift.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/snta/snta_ltpr.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/snta/snta_ltpss.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/snta/snta_snta.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/snta/snta_thin.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/sstas/sstas.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/sstas/sstas_lift.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/sstas/sstas_ltpss.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/sstas/sstas_sstas.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/sta/sta.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/sta/sta_lift.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/sta/sta_ltpss.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/sta/sta_sta.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/etc/top/lenv_top.etc (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/grammar/aarity.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/grammar/cl_shift.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/grammar/cl_weight.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/grammar/genv.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/grammar/item.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/grammar/lenv.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/grammar/lenv_append.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/grammar/lenv_length.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/grammar/lenv_px.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/grammar/lenv_px_bi.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/grammar/lenv_weight.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/grammar/term.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/grammar/term_simple.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/grammar/term_vector.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/grammar/term_weight.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/grammar/tshf.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/grammar/tstc.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/grammar/tstc_tstc.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/grammar/tstc_vector.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/names.txt (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/notation.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/cfpr.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/cfpr_aaa.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/cfpr_cfpr.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/cfpr_cpr.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/cfpr_ltpss.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/cif.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/cif_append.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/cnf.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/cnf_cif.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/cnf_lift.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/cpr.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/cpr_aaa.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/cpr_cpr.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/cpr_delift.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/cpr_lift.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/cpr_ltpr.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/cpr_ltpss.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/cpr_tpss.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/crf.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/crf_append.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/fpr.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/fpr_cpr.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/fpr_fpr.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/lfpr.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/lfpr_aaa.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/lfpr_alt.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/lfpr_cpr.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/lfpr_fpr.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/lfpr_lfpr.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/ltpr.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/ltpr_aaa.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/ltpr_ldrop.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/ltpr_ltpr.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/ltpr_ltpss_dx.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/ltpr_ltpss_sn.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/ltpr_tps.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/thnf.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/tpr.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/tpr_delift.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/tpr_lift.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/tpr_tpr.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/tpr_tps.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/tpr_tpss.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/xpr.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/xpr_aaa.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/xpr_lift.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/reducibility/xpr_lsubss.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/static/aaa.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/static/aaa_aaa.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/static/aaa_lift.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/static/aaa_lifts.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/static/aaa_ltpss_dx.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/static/aaa_ltpss_sn.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/static/lsuba.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/static/lsuba_aaa.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/static/lsuba_ldrop.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/static/lsuba_lsuba.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/static/lsubss.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/static/lsubss_ldrop.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/static/lsubss_lsubss.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/static/lsubss_ssta.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/static/sd.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/static/sh.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/static/ssta.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/static/ssta_aaa.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/static/ssta_lift.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/static/ssta_ltpss_dx.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/static/ssta_ltpss_sn.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/static/ssta_ssta.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/substitution/frsup.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/substitution/gdrop.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/substitution/gdrop_gdrop.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/substitution/ldrop.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/substitution/ldrop_append.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/substitution/ldrop_ldrop.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/substitution/ldrop_lpx.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/substitution/ldrop_sfr.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/substitution/lift.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/substitution/lift_lift.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/substitution/lift_lift_vector.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/substitution/lift_vector.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/substitution/lsubs.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/substitution/lsubs_sfr.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/substitution/tps.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/substitution/tps_lift.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/substitution/tps_tps.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/delift.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/delift_alt.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/delift_delift.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/delift_lift.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/delift_ltpss.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/delift_tpss.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/frsupp.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/frsupp_frsupp.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/frsups.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/frsups_frsups.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/gr2.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/gr2_gr2.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/gr2_minus.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/gr2_plus.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/ldrops.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/ldrops_ldrop.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/ldrops_ldrops.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/lifts.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/lifts_lift.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/lifts_lift_vector.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/lifts_lifts.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/lifts_vector.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/ltpss_dx.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/ltpss_dx_ldrop.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/ltpss_dx_ltpss_dx.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/ltpss_dx_tps.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/ltpss_dx_tpss.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/ltpss_sn.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/ltpss_sn_alt.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/ltpss_sn_ldrop.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/ltpss_sn_ltpss_sn.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/ltpss_sn_tps.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/ltpss_sn_tpss.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/thin.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/thin_delift.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/thin_ldrop.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/tpss.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/tpss_alt.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/tpss_lift.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/basic_2/unfold/tpss_tpss.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/ground_2/arith.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/ground_2/list.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/ground_2/notation.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/ground_2/star.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/ground_2/xoa.conf.xml (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/ground_2/xoa.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/ground_2/xoa_notation.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/ground_2/xoa_props.ma (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/ma2etc.sh (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/orig.sh (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/replace.sh (100%) rename matita/matita/contribs/{lambda_delta => lambdadelta}/root (100%) diff --git a/matita/matita/contribs/lambda_delta/Makefile b/matita/matita/contribs/lambdadelta/Makefile similarity index 100% rename from matita/matita/contribs/lambda_delta/Makefile rename to matita/matita/contribs/lambdadelta/Makefile diff --git a/matita/matita/contribs/lambda_delta/apps_2/functional/dsubst.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/dsubst.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/apps_2/functional/dsubst.ma rename to matita/matita/contribs/lambdadelta/apps_2/functional/dsubst.ma diff --git a/matita/matita/contribs/lambda_delta/apps_2/functional/lift.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/apps_2/functional/lift.ma rename to matita/matita/contribs/lambdadelta/apps_2/functional/lift.ma diff --git a/matita/matita/contribs/lambda_delta/apps_2/functional/notation.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/apps_2/functional/notation.ma rename to matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma diff --git a/matita/matita/contribs/lambda_delta/apps_2/functional/rtm.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/apps_2/functional/rtm.ma rename to matita/matita/contribs/lambdadelta/apps_2/functional/rtm.ma diff --git a/matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma rename to matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/basic_1.orig b/matita/matita/contribs/lambdadelta/basic_2/basic_1.orig similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/basic_1.orig rename to matita/matita/contribs/lambdadelta/basic_2/basic_1.orig diff --git a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt b/matita/matita/contribs/lambdadelta/basic_2/basic_1.txt similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/basic_1.txt rename to matita/matita/contribs/lambdadelta/basic_2/basic_1.txt diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/acp.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/acp.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpe.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/cpe.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cpe_cpe.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpe_cpe.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/cpe_cpe.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/cpe_cpe.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_aaa.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/cprs_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/cprs_aaa.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_delift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/cprs_delift.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lfpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lfpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lfpr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lfprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lfprs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lfprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lfprs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_ltpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/cprs_ltpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/cprs_ltpr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc_vector.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc_vector.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc_vector.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/csn_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/csn_alt.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_cpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/csn_cpr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_cpr_vector.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr_vector.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/csn_cpr_vector.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lfpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/csn_lfpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/csn_lfpr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_tstc_vector.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/csn_tstc_vector.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_vector.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/csn_vector.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/fprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fprs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/fprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/fprs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/fprs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_aaa.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/fprs_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/fprs_aaa.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/fprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_cprs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/fprs_cprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/fprs_cprs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/fprs_fprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_fprs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/fprs_fprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/fprs_fprs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/lfprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/lfprs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_aaa.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_aaa.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_cprs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_cprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_cprs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_lfprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_lfprs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_lfprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_lfprs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/lsubc.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrop.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrop.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrop.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrops.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrops.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrops.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrops.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_lsuba.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/ltprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/ltprs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_alt.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_alt.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_alt.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ldrop.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_ldrop.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ldrop.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_ltprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_ltprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/tprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/tprs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/tprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/tprs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/tprs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/tprs_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/tprs_lift.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/tprs_tprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_tprs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/tprs_tprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/tprs_tprs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/xprs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/xprs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/xprs_aaa.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/xprs_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/xprs_aaa.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/xprs_cprs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/xprs_cprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/xprs_cprs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/xprs_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/xprs_lift.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/xprs_lsubss.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lsubss.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/xprs_lsubss.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_xprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/xprs_xprs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/computation/xprs_xprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/xprs_xprs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/conversion/cpc.ma b/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/conversion/cpc.ma rename to matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/conversion/cpc_cpc.ma b/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc_cpc.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/conversion/cpc_cpc.ma rename to matita/matita/contribs/lambdadelta/basic_2/conversion/cpc_cpc.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/conversion/fpc.ma b/matita/matita/contribs/lambdadelta/basic_2/conversion/fpc.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/conversion/fpc.ma rename to matita/matita/contribs/lambdadelta/basic_2/conversion/fpc.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/conversion/fpc_fpc.ma b/matita/matita/contribs/lambdadelta/basic_2/conversion/fpc_fpc.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/conversion/fpc_fpc.ma rename to matita/matita/contribs/lambdadelta/basic_2/conversion/fpc_fpc.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/conversion/lfpc.ma b/matita/matita/contribs/lambdadelta/basic_2/conversion/lfpc.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/conversion/lfpc.ma rename to matita/matita/contribs/lambdadelta/basic_2/conversion/lfpc.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/conversion/lfpc_lfpc.ma b/matita/matita/contribs/lambdadelta/basic_2/conversion/lfpc_lfpc.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/conversion/lfpc_lfpc.ma rename to matita/matita/contribs/lambdadelta/basic_2/conversion/lfpc_lfpc.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma rename to matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_ssta.ma rename to matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs.ma rename to matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_aaa.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_aaa.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma rename to matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cprs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cprs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_delift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma rename to matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_delift.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_ltpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_ltpr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpss.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_ltpss.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpss.ma rename to matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_ltpss.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs.ma rename to matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_aaa.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_aaa.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_cpcs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs_cpcs.ma rename to matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_cpcs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs_fpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_fpcs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs_fpcs.ma rename to matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_fpcs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs_fprs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_fprs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs_fprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_fprs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs.ma rename to matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_aaa.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_aaa.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_lfpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_lfpcs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_lfpcs.ma rename to matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_lfpcs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_lfprs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_lfprs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_lfprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_lfprs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lsubse.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubse.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/equivalence/lsubse.ma rename to matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubse.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lsubse_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubse_cpcs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/equivalence/lsubse_cpcs.ma rename to matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubse_cpcs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lsubse_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubse_ldrop.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/equivalence/lsubse_ldrop.ma rename to matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubse_ldrop.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lsubse_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubse_ssta.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/equivalence/lsubse_ssta.ma rename to matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubse_ssta.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csup.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csup.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/csup/csup.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/csup/csup.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csup_csup.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csup_csup.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/csup/csup_csup.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/csup/csup_csup.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csupp.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csupp.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/csup/csupp.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/csup/csupp.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csupp_csupp.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csupp_csupp.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/csup/csupp_csupp.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/csup/csupp_csupp.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csups.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csups.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/csup/csups.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/csup/csups.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csups_csups.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csups_csups.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/csup/csups_csups.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/csup/csups_csups.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/ypr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/ypr.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/csup/ypr.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/csup/ypr.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/yprs.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/csup/yprs.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_csups.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/yprs_csups.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_csups.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/csup/yprs_csups.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_xprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/yprs_xprs.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_xprs.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/csup/yprs_xprs.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_yprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/yprs_yprs.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_yprs.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/csup/yprs_yprs.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/ysteps.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/ysteps.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/csup/ysteps.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/csup/ysteps.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/ysteps_csups.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/ysteps_csups.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/csup/ysteps_csups.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/csup/ysteps_csups.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/hod/ntas.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/hod/ntas.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/hod/ntas.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/hod/ntas.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/hod/ntas_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/hod/ntas_lift.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/hod/ntas_lift.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/hod/ntas_lift.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/lenv_px/lcpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lenv_px/lcpcs.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/lenv_px/lcpcs.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lenv_px/lcpcs.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/lenv_px/lcpcs_ltpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lenv_px/lcpcs_ltpr.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/lenv_px/lcpcs_ltpr.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lenv_px/lcpcs_ltpr.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/lenv_px/lenv_px_sn.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lenv_px/lenv_px_sn.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/lenv_px/lenv_px_sn.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lenv_px/lenv_px_sn.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/lsubn/lsubn_lsubn.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubn/lsubn_lsubn.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/lsubn/lsubn_lsubn.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubn/lsubn_lsubn.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv_cpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_cpcs.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv_cpcs.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_cpcs.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv_ldrop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_ldrop.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv_ldrop.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_ldrop.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv_snv.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_snv.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv_snv.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_snv.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv_ssta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_ssta.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv_ssta.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_ssta.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/nta/lsubn.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/lsubn.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/nta/lsubn.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/nta/lsubn.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/nta/lsubn_cpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/lsubn_cpcs.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/nta/lsubn_cpcs.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/nta/lsubn_cpcs.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/nta/lsubn_ldrop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/lsubn_ldrop.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/nta/lsubn_ldrop.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/nta/lsubn_ldrop.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/nta/lsubn_nta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/lsubn_nta.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/nta/lsubn_nta.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/nta/lsubn_nta.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_aaa.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_aaa.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_aaa.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_alt.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_alt.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_alt.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_lift.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_lift.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_lift.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_ltpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_ltpr.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_ltpr.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_ltpr.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_ltpss.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_ltpss.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_ltpss.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_ltpss.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_nta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_nta.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_nta.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_nta.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_sta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_sta.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_sta.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_sta.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_thin.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_thin.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_thin.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_thin.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/snta/lsubsn.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/snta/lsubsn.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn_cpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/snta/lsubsn_cpcs.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn_cpcs.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/snta/lsubsn_cpcs.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn_ldrop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/snta/lsubsn_ldrop.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn_ldrop.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/snta/lsubsn_ldrop.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn_snta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/snta/lsubsn_snta.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn_snta.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/snta/lsubsn_snta.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/snta/snta.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/snta/snta.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/snta/snta_lift.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_lift.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/snta/snta_lift.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_ltpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/snta/snta_ltpr.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_ltpr.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/snta/snta_ltpr.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_ltpss.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/snta/snta_ltpss.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_ltpss.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/snta/snta_ltpss.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_snta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/snta/snta_snta.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_snta.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/snta/snta_snta.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_thin.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/snta/snta_thin.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_thin.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/snta/snta_thin.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/sstas/sstas.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/sstas/sstas.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/sstas/sstas_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas_lift.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/sstas/sstas_lift.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas_lift.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/sstas/sstas_ltpss.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas_ltpss.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/sstas/sstas_ltpss.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas_ltpss.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/sstas/sstas_sstas.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas_sstas.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/sstas/sstas_sstas.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas_sstas.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/sta/sta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/sta/sta.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/sta/sta_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_lift.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/sta/sta_lift.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_lift.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/sta/sta_ltpss.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_ltpss.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/sta/sta_ltpss.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_ltpss.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/sta/sta_sta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_sta.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/sta/sta_sta.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_sta.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/top/lenv_top.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/top/lenv_top.etc similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/etc/top/lenv_top.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/top/lenv_top.etc diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma rename to matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_shift.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_shift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/grammar/cl_shift.ma rename to matita/matita/contribs/lambdadelta/basic_2/grammar/cl_shift.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma rename to matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/genv.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/grammar/genv.ma rename to matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/item.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/grammar/item.ma rename to matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma rename to matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma rename to matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_length.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_length.ma rename to matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma rename to matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px_bi.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px_bi.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px_bi.ma rename to matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px_bi.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma rename to matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/term.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/grammar/term.ma rename to matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_simple.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/grammar/term_simple.ma rename to matita/matita/contribs/lambdadelta/basic_2/grammar/term_simple.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/grammar/term_vector.ma rename to matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_weight.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma rename to matita/matita/contribs/lambdadelta/basic_2/grammar/term_weight.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/tshf.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/tshf.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/grammar/tshf.ma rename to matita/matita/contribs/lambdadelta/basic_2/grammar/tshf.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/grammar/tstc.ma rename to matita/matita/contribs/lambdadelta/basic_2/grammar/tstc.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc_tstc.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_tstc.ma rename to matita/matita/contribs/lambdadelta/basic_2/grammar/tstc_tstc.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc_vector.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_vector.ma rename to matita/matita/contribs/lambdadelta/basic_2/grammar/tstc_vector.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/names.txt rename to matita/matita/contribs/lambdadelta/basic_2/names.txt diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/notation.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_aaa.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_aaa.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_cfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_cfpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_cfpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_cfpr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_cpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_cpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_cpr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_ltpss.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_ltpss.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_ltpss.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_ltpss.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cif.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cif.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/cif.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/cif.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cif_append.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cif_append.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/cif_append.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/cif_append.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_cif.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_cif.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_cif.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_cif.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_lift.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_aaa.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_aaa.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_cpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_cpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_cpr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_delift.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_delift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_delift.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_delift.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_ltpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_ltpr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpss.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_ltpss.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpss.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_ltpss.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_tpss.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_tpss.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_tpss.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/crf.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/crf.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/crf.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/crf.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/crf_append.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/crf_append.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/crf_append.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/crf_append.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr_cpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr_fpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_fpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr_fpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_fpr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_aaa.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_aaa.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_alt.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_alt.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_alt.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_cpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_cpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_cpr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_fpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_fpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_fpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_fpr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_lfpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_lfpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_lfpr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_aaa.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_aaa.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ldrop.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ldrop.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ldrop.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpss_dx.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpss_dx.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpss_dx.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpss_sn.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpss_sn.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpss_sn.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_tps.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_tps.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_tps.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_tps.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/thnf.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/thnf.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/thnf.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/thnf.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_delift.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_delift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_delift.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_delift.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_lift.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tps.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tps.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tps.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tps.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpss.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpss.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_aaa.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_aaa.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_lift.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_lsubss.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_lsubss.ma rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_lsubss.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/static/aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_aaa.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/static/aaa_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/aaa_aaa.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/static/aaa_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/aaa_lift.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lifts.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/static/aaa_lifts.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/aaa_lifts.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_ltpss_dx.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss_dx.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/aaa_ltpss_dx.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_ltpss_sn.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss_sn.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/aaa_ltpss_sn.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/static/lsuba.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_aaa.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/static/lsuba_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/lsuba_aaa.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_ldrop.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/static/lsuba_ldrop.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/lsuba_ldrop.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/static/lsuba_lsuba.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubss.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/static/lsubss.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/lsubss.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/lsubss_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubss_ldrop.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/static/lsubss_ldrop.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/lsubss_ldrop.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/lsubss_lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubss_lsubss.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/static/lsubss_lsubss.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/lsubss_lsubss.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/lsubss_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubss_ssta.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/static/lsubss_ssta.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/lsubss_ssta.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/sd.ma b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/static/sd.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/sd.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/sh.ma b/matita/matita/contribs/lambdadelta/basic_2/static/sh.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/static/sh.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/sh.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/static/ssta.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/ssta_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/static/ssta_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/ssta_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/static/ssta_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/ssta_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_dx.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/static/ssta_ltpss_dx.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_dx.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/ssta_ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_sn.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/static/ssta_ltpss_sn.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_sn.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/ssta_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ssta.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/static/ssta_ssta.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/ssta_ssta.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/frsup.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/frsup.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/substitution/frsup.ma rename to matita/matita/contribs/lambdadelta/basic_2/substitution/frsup.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/gdrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/gdrop.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/substitution/gdrop.ma rename to matita/matita/contribs/lambdadelta/basic_2/substitution/gdrop.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/gdrop_gdrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/gdrop_gdrop.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/substitution/gdrop_gdrop.ma rename to matita/matita/contribs/lambdadelta/basic_2/substitution/gdrop_gdrop.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma rename to matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_append.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_append.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_append.ma rename to matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_append.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_ldrop.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_ldrop.ma rename to matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_ldrop.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_lpx.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_lpx.ma rename to matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_lpx.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_sfr.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_sfr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_sfr.ma rename to matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_sfr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift_vector.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift_vector.ma rename to matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift_vector.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_vector.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/substitution/lift_vector.ma rename to matita/matita/contribs/lambdadelta/basic_2/substitution/lift_vector.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs.ma rename to matita/matita/contribs/lambdadelta/basic_2/substitution/lsubs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs_sfr.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubs_sfr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs_sfr.ma rename to matita/matita/contribs/lambdadelta/basic_2/substitution/lsubs_sfr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma rename to matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/substitution/tps_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/substitution/tps_lift.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_tps.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_tps.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/substitution/tps_tps.ma rename to matita/matita/contribs/lambdadelta/basic_2/substitution/tps_tps.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_delift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/delift_delift.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/delift_lift.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_ltpss.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/delift_ltpss.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_tpss.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/delift_tpss.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/delift_tpss.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/frsupp.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/frsupp.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/frsupp.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/frsupp.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/frsupp_frsupp.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/frsupp_frsupp.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/frsupp_frsupp.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/frsupp_frsupp.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/frsups.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/frsups.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/frsups.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/frsups.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/frsups_frsups.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/frsups_frsups.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/frsups_frsups.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/frsups_frsups.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/gr2.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/gr2.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/gr2.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_gr2.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/gr2_gr2.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_gr2.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/gr2_gr2.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_minus.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/gr2_minus.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_minus.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/gr2_minus.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_plus.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/gr2_plus.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_plus.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/gr2_plus.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ldrops.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/ldrops.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ldrops_ldrop.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops_ldrop.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/ldrops_ldrop.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops_ldrops.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ldrops_ldrops.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops_ldrops.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/ldrops_ldrops.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lifts.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/lifts.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_lift.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lift_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_lift_vector.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lift_vector.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_lift_vector.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_lifts.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lifts.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_lifts.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_vector.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_vector.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_vector.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ldrop.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx_ldrop.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ldrop.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ltpss_dx.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx_ltpss_dx.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ltpss_dx.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx_tps.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_tps.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx_tps.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_tps.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_tpss.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx_tpss.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_tpss.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_alt.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_alt.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_alt.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ldrop.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_ldrop.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ldrop.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ltpss_sn.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_ltpss_sn.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ltpss_sn.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_tps.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_tps.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_tps.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_tps.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_tpss.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_tpss.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_tpss.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/thin.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/thin.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/thin_delift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/thin_delift.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/thin_ldrop.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/thin_ldrop.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/thin_ldrop.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_alt.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_lift.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_tpss.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_tpss.ma rename to matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_tpss.ma diff --git a/matita/matita/contribs/lambda_delta/ground_2/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/arith.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/ground_2/arith.ma rename to matita/matita/contribs/lambdadelta/ground_2/arith.ma diff --git a/matita/matita/contribs/lambda_delta/ground_2/list.ma b/matita/matita/contribs/lambdadelta/ground_2/list.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/ground_2/list.ma rename to matita/matita/contribs/lambdadelta/ground_2/list.ma diff --git a/matita/matita/contribs/lambda_delta/ground_2/notation.ma b/matita/matita/contribs/lambdadelta/ground_2/notation.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/ground_2/notation.ma rename to matita/matita/contribs/lambdadelta/ground_2/notation.ma diff --git a/matita/matita/contribs/lambda_delta/ground_2/star.ma b/matita/matita/contribs/lambdadelta/ground_2/star.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/ground_2/star.ma rename to matita/matita/contribs/lambdadelta/ground_2/star.ma diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml b/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml similarity index 100% rename from matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml rename to matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/ground_2/xoa.ma rename to matita/matita/contribs/lambdadelta/ground_2/xoa.ma diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa_notation.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma rename to matita/matita/contribs/lambdadelta/ground_2/xoa_notation.ma diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa_props.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa_props.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/ground_2/xoa_props.ma rename to matita/matita/contribs/lambdadelta/ground_2/xoa_props.ma diff --git a/matita/matita/contribs/lambda_delta/ma2etc.sh b/matita/matita/contribs/lambdadelta/ma2etc.sh similarity index 100% rename from matita/matita/contribs/lambda_delta/ma2etc.sh rename to matita/matita/contribs/lambdadelta/ma2etc.sh diff --git a/matita/matita/contribs/lambda_delta/orig.sh b/matita/matita/contribs/lambdadelta/orig.sh similarity index 100% rename from matita/matita/contribs/lambda_delta/orig.sh rename to matita/matita/contribs/lambdadelta/orig.sh diff --git a/matita/matita/contribs/lambda_delta/replace.sh b/matita/matita/contribs/lambdadelta/replace.sh similarity index 100% rename from matita/matita/contribs/lambda_delta/replace.sh rename to matita/matita/contribs/lambdadelta/replace.sh diff --git a/matita/matita/contribs/lambda_delta/root b/matita/matita/contribs/lambdadelta/root similarity index 100% rename from matita/matita/contribs/lambda_delta/root rename to matita/matita/contribs/lambdadelta/root diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma index 5b430d7c6..e80380217 100644 --- a/matita/matita/lib/arithmetics/nat.ma +++ b/matita/matita/lib/arithmetics/nat.ma @@ -505,6 +505,19 @@ lemma f_ind: ∀A. ∀f:A→ℕ. ∀P:predicate A. (∀n. (∀a. f a < n → P a) → ∀a. f a = n → P a) → ∀a. P a. #A #f #P #H #a @(f_ind_aux … H) -H [2: // | skip ] +qed-. + +fact f2_ind_aux: ∀A1,A2. ∀f:A1→A2→ℕ. ∀P:relation2 A1 A2. + (∀n. (∀a1,a2. f a1 a2 < n → P a1 a2) → ∀a1,a2. f a1 a2 = n → P a1 a2) → + ∀n,a1,a2. f a1 a2 = n → P a1 a2. +#A1 #A2 #f #P #H #n @(nat_elim1 … n) -n #n /3 width=3/ (**) (* auto slow (34s) without #n *) +qed-. + +lemma f2_ind: ∀A1,A2. ∀f:A1→A2→ℕ. ∀P:relation2 A1 A2. + (∀n. (∀a1,a2. f a1 a2 < n → P a1 a2) → ∀a1,a2. f a1 a2 = n → P a1 a2) → + ∀a1,a2. P a1 a2. +#A1 #A2 #f #P #H #a1 #a2 +@(f2_ind_aux … H) -H [2: // | skip ] qed-. (* More negated equalities **************************************************) -- 2.39.2