Reverting to the previous version some files which weren't intended to be

changed.

diff --git a/helm/software/components/ng_kernel/alluris.txt b/helm/software/components/ng_kernel/alluris.txt
index bfd76a2af1dd1434a035a2948e289a6670c6d97d..0d49a6a7425a76edabbad17f91dfb6a623516729 100644 (file)
--- a/helm/software/components/ng_kernel/alluris.txt
+++ b/helm/software/components/ng_kernel/alluris.txt
@@ -1,2400 +1,573 @@
-cic:/BellLabs/lazyPCF/OpSem/environments/cfgenv.con
-cic:/BellLabs/lazyPCF/OpSem/environments/cfgexp.con
-cic:/BellLabs/lazyPCF/OpSem/environments/config.ind
-cic:/BellLabs/lazyPCF/OpSem/environments/config_ind.con
-cic:/BellLabs/lazyPCF/OpSem/environments/config_rec.con
-cic:/BellLabs/lazyPCF/OpSem/environments/config_rect.con
-cic:/BellLabs/lazyPCF/OpSem/environments/mapsto.con
-cic:/BellLabs/lazyPCF/OpSem/environments/member.con
-cic:/BellLabs/lazyPCF/OpSem/environments/OS_Dom.con
-cic:/BellLabs/lazyPCF/OpSem/environments/OS_Dom_ty.con
-cic:/BellLabs/lazyPCF/OpSem/environments/OS_env.con
-cic:/BellLabs/lazyPCF/OpSem/environments/TE_Dom.con
-cic:/BellLabs/lazyPCF/OpSem/environments/ty_env.con
-cic:/BellLabs/lazyPCF/OpSem/environments/VT.con
-cic:/BellLabs/lazyPCF/OpSem/environments/VTT.con
-cic:/BellLabs/lazyPCF/OpSem/freevars/fv.con
-cic:/BellLabs/lazyPCF/OpSem/freevars/FV_fv.con
-cic:/BellLabs/lazyPCF/OpSem/freevars/FV.ind
-cic:/BellLabs/lazyPCF/OpSem/freevars/FV_ind.con
-cic:/BellLabs/lazyPCF/OpSem/freevars/inv_FV_abs.con
-cic:/BellLabs/lazyPCF/OpSem/freevars/inv_FV_appl.con
-cic:/BellLabs/lazyPCF/OpSem/freevars/inv_FV_clos.con
-cic:/BellLabs/lazyPCF/OpSem/freevars/inv_FV_cond.con
-cic:/BellLabs/lazyPCF/OpSem/freevars/inv_FV_fff.con
-cic:/BellLabs/lazyPCF/OpSem/freevars/inv_FV_fix.con
-cic:/BellLabs/lazyPCF/OpSem/freevars/inv_FV_is_o.con
-cic:/BellLabs/lazyPCF/OpSem/freevars/inv_FV_o.con
-cic:/BellLabs/lazyPCF/OpSem/freevars/inv_FV_prd.con
-cic:/BellLabs/lazyPCF/OpSem/freevars/inv_FV_succ.con
-cic:/BellLabs/lazyPCF/OpSem/freevars/inv_FV_ttt.con
-cic:/BellLabs/lazyPCF/OpSem/freevars/inv_FV_var.con
-cic:/BellLabs/lazyPCF/OpSem/freevars/notFV_abs.con
-cic:/BellLabs/lazyPCF/OpSem/freevars/notFV_appl.con
-cic:/BellLabs/lazyPCF/OpSem/freevars/notFV_clos.con
-cic:/BellLabs/lazyPCF/OpSem/freevars/notFV_cond.con
-cic:/BellLabs/lazyPCF/OpSem/freevars/notFV_fix.con
-cic:/BellLabs/lazyPCF/OpSem/freevars/notFV_is_o.con
-cic:/BellLabs/lazyPCF/OpSem/freevars/notFV_prd.con
-cic:/BellLabs/lazyPCF/OpSem/freevars/notFV_succ.con
-cic:/BellLabs/lazyPCF/OpSem/freevars/notFV_var.con
-cic:/BellLabs/lazyPCF/OpSem/OSrules/Ap.ind
-cic:/BellLabs/lazyPCF/OpSem/OSrules/Ap_ind.con
-cic:/BellLabs/lazyPCF/OpSem/OSrules/ApNewVar.con
-cic:/BellLabs/lazyPCF/OpSem/OSrules/OScons.con
-cic:/BellLabs/lazyPCF/OpSem/OSrules/OSred.ind
-cic:/BellLabs/lazyPCF/OpSem/OSrules/OSred_ind.con
-cic:/BellLabs/lazyPCF/OpSem/rename/rename.ind
-cic:/BellLabs/lazyPCF/OpSem/rename/rename_ind.con
-cic:/BellLabs/lazyPCF/OpSem/rename/RenNotFree.con
-cic:/BellLabs/lazyPCF/OpSem/syntax/tm.ind
-cic:/BellLabs/lazyPCF/OpSem/syntax/tm_ind.con
-cic:/BellLabs/lazyPCF/OpSem/syntax/tm_rec.con
-cic:/BellLabs/lazyPCF/OpSem/syntax/tm_rect.con
-cic:/BellLabs/lazyPCF/OpSem/syntax/ty.ind
-cic:/BellLabs/lazyPCF/OpSem/syntax/ty_ind.con
-cic:/BellLabs/lazyPCF/OpSem/syntax/ty_rec.con
-cic:/BellLabs/lazyPCF/OpSem/syntax/ty_rect.con
-cic:/BellLabs/lazyPCF/OpSem/syntax/vari.ind
-cic:/BellLabs/lazyPCF/OpSem/syntax/vari_ind.con
-cic:/BellLabs/lazyPCF/OpSem/syntax/vari_rec.con
-cic:/BellLabs/lazyPCF/OpSem/syntax/vari_rect.con
-cic:/BellLabs/lazyPCF/OpSem/typecheck/inv_TC_abs.con
-cic:/BellLabs/lazyPCF/OpSem/typecheck/inv_TC_appl.con
-cic:/BellLabs/lazyPCF/OpSem/typecheck/inv_TC_clos.con
-cic:/BellLabs/lazyPCF/OpSem/typecheck/inv_TC_cond.con
-cic:/BellLabs/lazyPCF/OpSem/typecheck/inv_TC_fff.con
-cic:/BellLabs/lazyPCF/OpSem/typecheck/inv_TC_fix.con
-cic:/BellLabs/lazyPCF/OpSem/typecheck/inv_TC_is_o.con
-cic:/BellLabs/lazyPCF/OpSem/typecheck/inv_TC_o.con
-cic:/BellLabs/lazyPCF/OpSem/typecheck/inv_TC_prd.con
-cic:/BellLabs/lazyPCF/OpSem/typecheck/inv_TC_succ.con
-cic:/BellLabs/lazyPCF/OpSem/typecheck/inv_TC_ttt.con
-cic:/BellLabs/lazyPCF/OpSem/typecheck/inv_TC_var.con
-cic:/BellLabs/lazyPCF/OpSem/typecheck/tc.con
-cic:/BellLabs/lazyPCF/OpSem/typecheck/TC.ind
-cic:/BellLabs/lazyPCF/OpSem/typecheck/TC_ind.con
-cic:/BellLabs/lazyPCF/OpSem/typecheck/TC_tc.con
-cic:/BellLabs/lazyPCF/OpSem/utils/AABC_ABC.con
-cic:/BellLabs/lazyPCF/OpSem/utils/bool_not_arr.con
-cic:/BellLabs/lazyPCF/OpSem/utils/F_If.con
-cic:/BellLabs/lazyPCF/OpSem/utils/IfA_IfAIfA.con
-cic:/BellLabs/lazyPCF/OpSem/utils/If_F.con
-cic:/BellLabs/lazyPCF/OpSem/utils/If_T.con
-cic:/BellLabs/lazyPCF/OpSem/utils/is_arr.con
-cic:/BellLabs/lazyPCF/OpSem/utils/is_bool.con
-cic:/BellLabs/lazyPCF/OpSem/utils/is_nat.con
-cic:/BellLabs/lazyPCF/OpSem/utils/nat_not_arr.con
-cic:/BellLabs/lazyPCF/OpSem/utils/nat_not_bool.con
-cic:/BellLabs/lazyPCF/OpSem/utils/Rand_ty.con
-cic:/BellLabs/lazyPCF/OpSem/utils/Rator_ty.con
-cic:/BellLabs/lazyPCF/OpSem/utils/subty_eq.con
-cic:/BellLabs/lazyPCF/OpSem/utils/T_If.con
-cic:/BellLabs/lazyPCF/OpSem/utils/valu.con
-cic:/BellLabs/lazyPCF/OpSem/utils/vari_nat.con
-cic:/BellLabs/lazyPCF/OpSem/utils/Xmidnat.con
-cic:/BellLabs/lazyPCF/OpSem/utils/Xmidvar.con
-cic:/BellLabs/lazyPCF/SubjRed/ApTypes/ren_case1.con
-cic:/BellLabs/lazyPCF/SubjRed/ApTypes/ren_case2.con
-cic:/BellLabs/lazyPCF/SubjRed/ApTypes/ren_var1.con
-cic:/BellLabs/lazyPCF/SubjRed/ApTypes/ren_var2.con
-cic:/BellLabs/lazyPCF/SubjRed/ApTypes/TEp_Ap.con
-cic:/BellLabs/lazyPCF/SubjRed/ApTypes/TEp_RenExp.con
-cic:/BellLabs/lazyPCF/SubjRed/ApTypes/TEp_RenExpGen.con
-cic:/BellLabs/lazyPCF/SubjRed/envprops/dom_pres.con
-cic:/BellLabs/lazyPCF/SubjRed/envprops/TCHet_FVeinDomH.con
-cic:/BellLabs/lazyPCF/SubjRed/envprops/TEDomDomty_OSDom.con
-cic:/BellLabs/lazyPCF/SubjRed/envprops/vtinH_vinDomH.con
-cic:/BellLabs/lazyPCF/SubjRed/mapsto/Mp_eqExt.con
-cic:/BellLabs/lazyPCF/SubjRed/mapsto/Mp_inv_eqExt.con
-cic:/BellLabs/lazyPCF/SubjRed/mapsto/Mp_inv_nfvExt.con
-cic:/BellLabs/lazyPCF/SubjRed/mapsto/Mp_nfvExt.con
-cic:/BellLabs/lazyPCF/SubjRed/mapsto/Mp_swap.con
-cic:/BellLabs/lazyPCF/SubjRed/NF/F.ind
-cic:/BellLabs/lazyPCF/SubjRed/NF/F_ind.con
-cic:/BellLabs/lazyPCF/SubjRed/NF/inv_NF_Sno.con
-cic:/BellLabs/lazyPCF/SubjRed/NF/inv_Sno_s.con
-cic:/BellLabs/lazyPCF/SubjRed/NF/NF.ind
-cic:/BellLabs/lazyPCF/SubjRed/NF/NF_ind.con
-cic:/BellLabs/lazyPCF/SubjRed/NF/NFsucc.con
-cic:/BellLabs/lazyPCF/SubjRed/NFprops/Fe_not_bool.con
-cic:/BellLabs/lazyPCF/SubjRed/NFprops/Fe_not_nat.con
-cic:/BellLabs/lazyPCF/SubjRed/NFprops/NFebool_TF.con
-cic:/BellLabs/lazyPCF/SubjRed/NFprops/NFe_Fe.con
-cic:/BellLabs/lazyPCF/SubjRed/NFprops/NFenat_Snoe.con
-cic:/BellLabs/lazyPCF/SubjRed/NFprops/Snoe_notFVe.con
-cic:/BellLabs/lazyPCF/SubjRed/NF/Sno.ind
-cic:/BellLabs/lazyPCF/SubjRed/NF/Sno_ind.con
-cic:/BellLabs/lazyPCF/SubjRed/NF/SnoSucc.con
-cic:/BellLabs/lazyPCF/SubjRed/subjrnf/NormalForms.con
-cic:/BellLabs/lazyPCF/SubjRed/subjrnf/subjr_NF.con
-cic:/BellLabs/lazyPCF/SubjRed/subjrnf/subjr_red.con
-cic:/BellLabs/lazyPCF/SubjRed/TypeThms/TEp_eqExt.con
-cic:/BellLabs/lazyPCF/SubjRed/TypeThms/TEp_inv_eqExt.con
-cic:/BellLabs/lazyPCF/SubjRed/TypeThms/TEp_inv_nfvExt.con
-cic:/BellLabs/lazyPCF/SubjRed/TypeThms/TEp_nfvExt.con
-cic:/BellLabs/lazyPCF/SubjRed/TypeThms/TEp_swap.con
-cic:/BellLabs/lazyPCF/SubjRed/valid/inv_valid_cons.con
-cic:/BellLabs/lazyPCF/SubjRed/valid/valid_c.con
-cic:/BellLabs/lazyPCF/SubjRed/valid/valid_config.ind
-cic:/BellLabs/lazyPCF/SubjRed/valid/valid_config_ind.con
-cic:/BellLabs/lazyPCF/SubjRed/valid/valid_env.ind
-cic:/BellLabs/lazyPCF/SubjRed/valid/valid_env_ind.con
-cic:/Cachan/SMC/alloc/BDDalloc_BDD_OK.con
-cic:/Cachan/SMC/alloc/BDDalloc.con
-cic:/Cachan/SMC/alloc/BDDallocGet.con
-cic:/Cachan/SMC/alloc/BDDalloc_keeps_cnt_OK.con
-cic:/Cachan/SMC/alloc/BDDalloc_keeps_config_OK.con
-cic:/Cachan/SMC/alloc/BDDalloc_keeps_free_list_OK.con
-cic:/Cachan/SMC/alloc/BDDalloc_keeps_neg_memo_OK.con
-cic:/Cachan/SMC/alloc/BDDalloc_keeps_or_memo_OK.con
-cic:/Cachan/SMC/alloc/BDDalloc_keeps_sharing_OK.con
-cic:/Cachan/SMC/alloc/BDDalloc_keeps_state_OK.con
-cic:/Cachan/SMC/alloc/BDDalloc_keeps_univ_memo_OK.con
-cic:/Cachan/SMC/alloc/BDDalloc_lemma_1.con
-cic:/Cachan/SMC/alloc/BDDalloc_lemma_2.con
-cic:/Cachan/SMC/alloc/BDDalloc_lemma_3.con
-cic:/Cachan/SMC/alloc/BDDalloc_lemma_4.con
-cic:/Cachan/SMC/alloc/BDDalloc_lemma_5.con
-cic:/Cachan/SMC/alloc/BDDalloc_negm_same.con
-cic:/Cachan/SMC/alloc/BDDalloc_node_OK.con
-cic:/Cachan/SMC/alloc/BDDalloc_one.con
-cic:/Cachan/SMC/alloc/BDDalloc_orm_same.con
-cic:/Cachan/SMC/alloc/BDDalloc_preserves_nodes.con
-cic:/Cachan/SMC/alloc/BDDalloc_preserves_used_nodes.con
-cic:/Cachan/SMC/alloc/BDDalloc_um_same.con
-cic:/Cachan/SMC/alloc/BDDalloc_zero.con
-cic:/Cachan/SMC/alloc/BDD_OK_l.con
-cic:/Cachan/SMC/alloc/BDD_OK_r.con
-cic:/Cachan/SMC/alloc/BDDsharing_OK_1.con
-cic:/Cachan/SMC/alloc/new_cfg_nodes_preserved.con
-cic:/Cachan/SMC/alloc/new_cfg_OK.con
-cic:/Cachan/SMC/alloc/new_l_OK.con
-cic:/Cachan/SMC/alloc/new_r_OK.con
-cic:/Cachan/SMC/alloc/new_xl_lt_x.con
-cic:/Cachan/SMC/alloc/new_xr_lt_x.con
-cic:/Cachan/SMC/alloc/no_dup_new.con
-cic:/Cachan/SMC/bool_fun/augment.con
-cic:/Cachan/SMC/bool_fun/bool_expr.ind
-cic:/Cachan/SMC/bool_fun/bool_expr_ind.con
-cic:/Cachan/SMC/bool_fun/bool_expr_rec.con
-cic:/Cachan/SMC/bool_fun/bool_expr_rect.con
-cic:/Cachan/SMC/bool_fun/bool_fun_and_comm.con
-cic:/Cachan/SMC/bool_fun/bool_fun_and.con
-cic:/Cachan/SMC/bool_fun/bool_fun_and_idempotent.con
-cic:/Cachan/SMC/bool_fun/bool_fun_and_lemma.con
-cic:/Cachan/SMC/bool_fun/bool_fun_and_orthogonal.con
-cic:/Cachan/SMC/bool_fun/bool_fun_and_preserves_eq.con
-cic:/Cachan/SMC/bool_fun/bool_fun.con
-cic:/Cachan/SMC/bool_fun/bool_fun_eq.con
-cic:/Cachan/SMC/bool_fun/bool_fun_eq_independent.con
-cic:/Cachan/SMC/bool_fun/bool_fun_eq_neg_eq.con
-cic:/Cachan/SMC/bool_fun/bool_fun_eq_refl.con
-cic:/Cachan/SMC/bool_fun/bool_fun_eq_sym.con
-cic:/Cachan/SMC/bool_fun/bool_fun_eq_trans.con
-cic:/Cachan/SMC/bool_fun/bool_fun_ex.con
-cic:/Cachan/SMC/bool_fun/bool_fun_ex_lemma.con
-cic:/Cachan/SMC/bool_fun/bool_fun_ex_preserves_eq.con
-cic:/Cachan/SMC/bool_fun/bool_fun_ext.con
-cic:/Cachan/SMC/bool_fun/bool_fun_ext_if.con
-cic:/Cachan/SMC/bool_fun/bool_fun_ext_one.con
-cic:/Cachan/SMC/bool_fun/bool_fun_ext_zero.con
-cic:/Cachan/SMC/bool_fun/bool_fun_forall.con
-cic:/Cachan/SMC/bool_fun/bool_fun_forall_if_egal.con
-cic:/Cachan/SMC/bool_fun/bool_fun_forall_independent.con
-cic:/Cachan/SMC/bool_fun/bool_fun_forall_one.con
-cic:/Cachan/SMC/bool_fun/bool_fun_forall_orthogonal.con
-cic:/Cachan/SMC/bool_fun/bool_fun_forall_preserves_eq.con
-cic:/Cachan/SMC/bool_fun/bool_fun_forall_zero.con
-cic:/Cachan/SMC/bool_fun/bool_fun_if.con
-cic:/Cachan/SMC/bool_fun/bool_fun_if_eq_1.con
-cic:/Cachan/SMC/bool_fun/bool_fun_if_eq_2.con
-cic:/Cachan/SMC/bool_fun/bool_fun_iff.con
-cic:/Cachan/SMC/bool_fun/bool_fun_iff_lemma.con
-cic:/Cachan/SMC/bool_fun/bool_fun_iff_preserves_eq.con
-cic:/Cachan/SMC/bool_fun/bool_fun_if_preserves_eq.con
-cic:/Cachan/SMC/bool_fun/bool_fun_if_restrict.con
-cic:/Cachan/SMC/bool_fun/bool_fun_if_restrict_false.con
-cic:/Cachan/SMC/bool_fun/bool_fun_if_restrict_false_independent.con
-cic:/Cachan/SMC/bool_fun/bool_fun_if_restrict_true.con
-cic:/Cachan/SMC/bool_fun/bool_fun_if_restrict_true_independent.con
-cic:/Cachan/SMC/bool_fun/bool_fun_impl.con
-cic:/Cachan/SMC/bool_fun/bool_fun_impl_lemma.con
-cic:/Cachan/SMC/bool_fun/bool_fun_impl_preserves_eq.con
-cic:/Cachan/SMC/bool_fun/bool_fun_independent.con
-cic:/Cachan/SMC/bool_fun/bool_fun_independent_if.con
-cic:/Cachan/SMC/bool_fun/bool_fun_independent_one.con
-cic:/Cachan/SMC/bool_fun/bool_fun_independent_zero.con
-cic:/Cachan/SMC/bool_fun/bool_fun_neg.con
-cic:/Cachan/SMC/bool_fun/bool_fun_neg_one.con
-cic:/Cachan/SMC/bool_fun/bool_fun_neg_orthogonal.con
-cic:/Cachan/SMC/bool_fun/bool_fun_neg_preserves_eq.con
-cic:/Cachan/SMC/bool_fun/bool_fun_neg_zero.con
-cic:/Cachan/SMC/bool_fun/bool_fun_of_bool_expr.con
-cic:/Cachan/SMC/bool_fun/bool_fun_one.con
-cic:/Cachan/SMC/bool_fun/bool_fun_or_comm.con
-cic:/Cachan/SMC/bool_fun/bool_fun_or.con
-cic:/Cachan/SMC/bool_fun/bool_fun_or_one.con
-cic:/Cachan/SMC/bool_fun/bool_fun_or_orthogonal.con
-cic:/Cachan/SMC/bool_fun/bool_fun_or_orthogonal_left.con
-cic:/Cachan/SMC/bool_fun/bool_fun_or_orthogonal_right.con
-cic:/Cachan/SMC/bool_fun/bool_fun_or_preserves_eq.con
-cic:/Cachan/SMC/bool_fun/bool_fun_or_zero.con
-cic:/Cachan/SMC/bool_fun/bool_fun_restrict.con
-cic:/Cachan/SMC/bool_fun/bool_fun_restrict_one.con
-cic:/Cachan/SMC/bool_fun/bool_fun_restrict_preserves_eq.con
-cic:/Cachan/SMC/bool_fun/bool_fun_restrict_zero.con
-cic:/Cachan/SMC/bool_fun/bool_fun_var.con
-cic:/Cachan/SMC/bool_fun/bool_fun_var_lemma.con
-cic:/Cachan/SMC/bool_fun/bool_fun_zero.con
-cic:/Cachan/SMC/bool_fun/var_env.con
-cic:/Cachan/SMC/config/BDDbounded.ind
-cic:/Cachan/SMC/config/BDDbounded_ind.con
-cic:/Cachan/SMC/config/BDDbounded_lemma.con
-cic:/Cachan/SMC/config/BDDbounded_node_OK.con
-cic:/Cachan/SMC/config/BDDconfig.con
-cic:/Cachan/SMC/config/BDDconfig_OK.con
-cic:/Cachan/SMC/config/BDDfree_list.con
-cic:/Cachan/SMC/config/BDDfree_list_OK.con
-cic:/Cachan/SMC/config/BDDneg_memo.con
-cic:/Cachan/SMC/config/BDDneg_memo_OK.con
-cic:/Cachan/SMC/config/BDDneg_memo_put.con
-cic:/Cachan/SMC/config/BDDnegm_put_nodes_preserved.con
-cic:/Cachan/SMC/config/BDDnegm_put_OK.con
-cic:/Cachan/SMC/config/BDD_OK.con
-cic:/Cachan/SMC/config/BDD_OK_node_OK.con
-cic:/Cachan/SMC/config/BDDone.con
-cic:/Cachan/SMC/config/BDDone_preserved.con
-cic:/Cachan/SMC/config/BDDor_memo.con
-cic:/Cachan/SMC/config/BDDor_memo_OK.con
-cic:/Cachan/SMC/config/BDDor_memo_put.con
-cic:/Cachan/SMC/config/BDDorm_put_nodes_preserved.con
-cic:/Cachan/SMC/config/BDDorm_put_OK.con
-cic:/Cachan/SMC/config/BDDsharing_map.con
-cic:/Cachan/SMC/config/BDDsharing_OK.con
-cic:/Cachan/SMC/config/BDDstate.con
-cic:/Cachan/SMC/config/BDDstate_OK.con
-cic:/Cachan/SMC/config/BDDum_put_nodes_preserved.con
-cic:/Cachan/SMC/config/BDDum_put_OK.con
-cic:/Cachan/SMC/config/BDDunique_1.con
-cic:/Cachan/SMC/config/BDDunique.con
-cic:/Cachan/SMC/config/BDDuniv_memo.con
-cic:/Cachan/SMC/config/BDDuniv_memo_OK.con
-cic:/Cachan/SMC/config/BDDuniv_memo_put.con
-cic:/Cachan/SMC/config/BDDvar_independent_1.con
-cic:/Cachan/SMC/config/BDDvar_independent_bs.con
-cic:/Cachan/SMC/config/BDDvar_independent_high.con
-cic:/Cachan/SMC/config/BDDvar_independent_low.con
-cic:/Cachan/SMC/config/BDDzero.con
-cic:/Cachan/SMC/config/BDDzero_preserved.con
-cic:/Cachan/SMC/config/bool_fun_of_BDD_1_change_bound.con
-cic:/Cachan/SMC/config/bool_fun_of_BDD_1.con
-cic:/Cachan/SMC/config/bool_fun_of_BDD_1_ext.con
-cic:/Cachan/SMC/config/bool_fun_of_BDD_bs.con
-cic:/Cachan/SMC/config/bool_fun_of_BDD_bs_ext.con
-cic:/Cachan/SMC/config/bool_fun_of_BDD_bs_high.con
-cic:/Cachan/SMC/config/bool_fun_of_BDD_bs_int.con
-cic:/Cachan/SMC/config/bool_fun_of_BDD_bs_low.con
-cic:/Cachan/SMC/config/bool_fun_of_BDD_bs_one.con
-cic:/Cachan/SMC/config/bool_fun_of_BDD_bs_zero.con
-cic:/Cachan/SMC/config/bool_fun_of_BDD.con
-cic:/Cachan/SMC/config/bool_fun_of_BDD_int.con
-cic:/Cachan/SMC/config/bool_fun_of_BDD_one.con
-cic:/Cachan/SMC/config/bool_fun_of_BDD_zero.con
-cic:/Cachan/SMC/config/bs_node_height.con
-cic:/Cachan/SMC/config/bs_node_height_left.con
-cic:/Cachan/SMC/config/bs_node_height_left_le.con
-cic:/Cachan/SMC/config/bs_node_height_right.con
-cic:/Cachan/SMC/config/bs_node_height_right_le.con
-cic:/Cachan/SMC/config/bs_of_cfg.con
-cic:/Cachan/SMC/config/bs_of_cfg_OK.con
-cic:/Cachan/SMC/config/cfg_comp.con
-cic:/Cachan/SMC/config/cnt_of_cfg.con
-cic:/Cachan/SMC/config/cnt_of_cfg_OK.con
-cic:/Cachan/SMC/config/cnt_OK.con
-cic:/Cachan/SMC/config/config_node_OK.con
-cic:/Cachan/SMC/config/config_OK_one.con
-cic:/Cachan/SMC/config/config_OK_zero.con
-cic:/Cachan/SMC/config/cons_OK_list_OK.con
-cic:/Cachan/SMC/config/fl_of_cfg.con
-cic:/Cachan/SMC/config/fl_of_cfg_OK.con
-cic:/Cachan/SMC/config/gc_OK.con
-cic:/Cachan/SMC/config/high_bounded.con
-cic:/Cachan/SMC/config/high_OK.con
-cic:/Cachan/SMC/config/high_used_bs.con
-cic:/Cachan/SMC/config/high_used'_bs.con
-cic:/Cachan/SMC/config/high_used.con
-cic:/Cachan/SMC/config/high_used'.con
-cic:/Cachan/SMC/config/increase_bound.con
-cic:/Cachan/SMC/config/initBDDconfig.con
-cic:/Cachan/SMC/config/initBDDconfig_OK.con
-cic:/Cachan/SMC/config/initBDDfree_list.con
-cic:/Cachan/SMC/config/initBDDfree_list_OK.con
-cic:/Cachan/SMC/config/initBDDneg_memo.con
-cic:/Cachan/SMC/config/initBDDneg_memo_OK.con
-cic:/Cachan/SMC/config/initBDDor_memo.con
-cic:/Cachan/SMC/config/initBDDor_memo_OK.con
-cic:/Cachan/SMC/config/initBDDsharing_map.con
-cic:/Cachan/SMC/config/initBDDsharing_map_OK.con
-cic:/Cachan/SMC/config/initBDDstate.con
-cic:/Cachan/SMC/config/initBDDstate_OK.con
-cic:/Cachan/SMC/config/initBDDuniv_memo.con
-cic:/Cachan/SMC/config/initBDDuniv_memo_OK.con
-cic:/Cachan/SMC/config/internal_node_lemma.con
-cic:/Cachan/SMC/config/int_node_gt_1.con
-cic:/Cachan/SMC/config/int_node_lt_cnt.con
-cic:/Cachan/SMC/config/low_bounded.con
-cic:/Cachan/SMC/config/low_high_neq.con
-cic:/Cachan/SMC/config/low_OK.con
-cic:/Cachan/SMC/config/low_used_bs.con
-cic:/Cachan/SMC/config/low_used'_bs.con
-cic:/Cachan/SMC/config/low_used.con
-cic:/Cachan/SMC/config/low_used'.con
-cic:/Cachan/SMC/config/negm_of_cfg.con
-cic:/Cachan/SMC/config/negm_of_cfg_OK.con
-cic:/Cachan/SMC/config/node_height.con
-cic:/Cachan/SMC/config/node_height_one.con
-cic:/Cachan/SMC/config/node_height_zero.con
-cic:/Cachan/SMC/config/node_OK_BDD_OK.con
-cic:/Cachan/SMC/config/node_OK.con
-cic:/Cachan/SMC/config/node_OK_list_OK_bs.con
-cic:/Cachan/SMC/config/node_OK_list_OK.con
-cic:/Cachan/SMC/config/node_preserved_bs_bool_fun_1.con
-cic:/Cachan/SMC/config/node_preserved_bs_bool_fun.con
-cic:/Cachan/SMC/config/node_preserved_bs.con
-cic:/Cachan/SMC/config/node_preserved_bs_node_height_eq.con
-cic:/Cachan/SMC/config/node_preserved_bs_reachable_1.con
-cic:/Cachan/SMC/config/node_preserved_bs_reachable.con
-cic:/Cachan/SMC/config/node_preserved_bs_trans.con
-cic:/Cachan/SMC/config/node_preserved.con
-cic:/Cachan/SMC/config/node_preserved_node_height_eq.con
-cic:/Cachan/SMC/config/node_preserved_OK_bs.con
-cic:/Cachan/SMC/config/nodes_preserved_bool_fun.con
-cic:/Cachan/SMC/config/nodes_preserved_bounded.con
-cic:/Cachan/SMC/config/nodes_preserved_bs_bool_fun_1.con
-cic:/Cachan/SMC/config/nodes_preserved_bs_bool_fun.con
-cic:/Cachan/SMC/config/nodes_preserved_bs.con
-cic:/Cachan/SMC/config/nodes_preserved_bs_node_height_eq.con
-cic:/Cachan/SMC/config/nodes_preserved_bs_node_OK.con
-cic:/Cachan/SMC/config/nodes_preserved_bs_refl.con
-cic:/Cachan/SMC/config/nodes_preserved_bs_trans.con
-cic:/Cachan/SMC/config/nodes_preserved.con
-cic:/Cachan/SMC/config/nodes_preserved_config_node_OK.con
-cic:/Cachan/SMC/config/nodes_preserved_neg_memo_OK.con
-cic:/Cachan/SMC/config/nodes_preserved_node_height_eq.con
-cic:/Cachan/SMC/config/nodes_preserved_or_memo_OK.con
-cic:/Cachan/SMC/config/nodes_preserved_refl.con
-cic:/Cachan/SMC/config/nodes_preserved_trans.con
-cic:/Cachan/SMC/config/nodes_preserved_um_OK.con
-cic:/Cachan/SMC/config/nodes_preserved_used_nodes_preserved.con
-cic:/Cachan/SMC/config/nodes_reachableBDDone.con
-cic:/Cachan/SMC/config/nodes_reachableBDDzero.con
-cic:/Cachan/SMC/config/nodes_reachable.ind
-cic:/Cachan/SMC/config/nodes_reachable_ind.con
-cic:/Cachan/SMC/config/nodes_reachable_lemma_1.con
-cic:/Cachan/SMC/config/nodes_reachable_trans.con
-cic:/Cachan/SMC/config/no_duplicate_node.con
-cic:/Cachan/SMC/config/no_new_node_bs.con
-cic:/Cachan/SMC/config/no_new_node.con
-cic:/Cachan/SMC/config/not_zero_is_one.con
-cic:/Cachan/SMC/config/one_OK.con
-cic:/Cachan/SMC/config/orm_of_cfg.con
-cic:/Cachan/SMC/config/orm_of_cfg_OK.con
-cic:/Cachan/SMC/config/reachable_node_OK_1.con
-cic:/Cachan/SMC/config/reachable_node_OK.con
-cic:/Cachan/SMC/config/share_of_cfg.con
-cic:/Cachan/SMC/config/share_of_cfg_OK.con
-cic:/Cachan/SMC/config/um_of_cfg.con
-cic:/Cachan/SMC/config/um_of_cfg_OK.con
-cic:/Cachan/SMC/config/used_list_OK_bs.con
-cic:/Cachan/SMC/config/used_list_OK.con
-cic:/Cachan/SMC/config/used_node_bs.con
-cic:/Cachan/SMC/config/used_node'_bs.con
-cic:/Cachan/SMC/config/used_node.con
-cic:/Cachan/SMC/config/used_node'.con
-cic:/Cachan/SMC/config/used_node_cons_node_ul.con
-cic:/Cachan/SMC/config/used_node_cons_node'_ul.con
-cic:/Cachan/SMC/config/used_node'_cons_node_ul.con
-cic:/Cachan/SMC/config/used_node'_cons_node'_ul.con
-cic:/Cachan/SMC/config/used_node_OK_bs.con
-cic:/Cachan/SMC/config/used_node'_OK_bs.con
-cic:/Cachan/SMC/config/used_node_OK.con
-cic:/Cachan/SMC/config/used_node'_OK.con
-cic:/Cachan/SMC/config/used_nodes_preserved_bool_fun.con
-cic:/Cachan/SMC/config/used_nodes_preserved'_bool_fun.con
-cic:/Cachan/SMC/config/used_nodes_preserved_bs_bool_fun.con
-cic:/Cachan/SMC/config/used_nodes_preserved'_bs_bool_fun.con
-cic:/Cachan/SMC/config/used_nodes_preserved_bs.con
-cic:/Cachan/SMC/config/used_nodes_preserved_bs_cons.con
-cic:/Cachan/SMC/config/used_nodes_preserved.con
-cic:/Cachan/SMC/config/used_nodes_preserved_cons.con
-cic:/Cachan/SMC/config/used_nodes_preserved_list_OK_bs.con
-cic:/Cachan/SMC/config/used_nodes_preserved_list_OK.con
-cic:/Cachan/SMC/config/used_nodes_preserved_node_height_eq.con
-cic:/Cachan/SMC/config/used_nodes_preserved'_node_height_eq.con
-cic:/Cachan/SMC/config/used_nodes_preserved_node_OK.con
-cic:/Cachan/SMC/config/used_nodes_preserved_node_OK'.con
-cic:/Cachan/SMC/config/used_nodes_preserved_preserved_bs.con
-cic:/Cachan/SMC/config/used_nodes_preserved_preserved'_bs.con
-cic:/Cachan/SMC/config/used_nodes_preserved_refl.con
-cic:/Cachan/SMC/config/used_nodes_preserved_trans.con
-cic:/Cachan/SMC/config/used_nodes_preserved_used_node.con
-cic:/Cachan/SMC/config/used_nodes_preserved_used_node'.con
-cic:/Cachan/SMC/config/used_node'_used_node_bs.con
-cic:/Cachan/SMC/config/used'_one.con
-cic:/Cachan/SMC/config/used'_zero.con
-cic:/Cachan/SMC/config/zero_OK.con
-cic:/Cachan/SMC/gc/add_used_nodes_1.con
-cic:/Cachan/SMC/gc/add_used_nodes_1_lemma_1.con
-cic:/Cachan/SMC/gc/add_used_nodes_1_lemma_2.con
-cic:/Cachan/SMC/gc/add_used_nodes.con
-cic:/Cachan/SMC/gc/add_used_nodes_lemma_1.con
-cic:/Cachan/SMC/gc/add_used_nodes_lemma_2.con
-cic:/Cachan/SMC/gc/clean'1_1.con
-cic:/Cachan/SMC/gc/clean'1_1_lemma.con
-cic:/Cachan/SMC/gc/clean'1.con
-cic:/Cachan/SMC/gc/clean1.con
-cic:/Cachan/SMC/gc/clean'1_lemma.con
-cic:/Cachan/SMC/gc/clean1_lemma.con
-cic:/Cachan/SMC/gc/clean'2_1.con
-cic:/Cachan/SMC/gc/clean2_1.con
-cic:/Cachan/SMC/gc/clean'2_1_lemma.con
-cic:/Cachan/SMC/gc/clean2_1_lemma.con
-cic:/Cachan/SMC/gc/clean'2.con
-cic:/Cachan/SMC/gc/clean2.con
-cic:/Cachan/SMC/gc/clean'2_lemma.con
-cic:/Cachan/SMC/gc/clean2_lemma.con
-cic:/Cachan/SMC/gc/clean3_1.con
-cic:/Cachan/SMC/gc/clean3_1_lemma.con
-cic:/Cachan/SMC/gc/clean3.con
-cic:/Cachan/SMC/gc/clean3_lemma.con
-cic:/Cachan/SMC/gc/dummy_mark.ind
-cic:/Cachan/SMC/gc/dummy_mark_ind.con
-cic:/Cachan/SMC/gc/dummy_mark_rec.con
-cic:/Cachan/SMC/gc/dummy_mark_rect.con
-cic:/Cachan/SMC/gc/gc_0.con
-cic:/Cachan/SMC/gc/gc_0_OK.con
-cic:/Cachan/SMC/gc/gc_inf.con
-cic:/Cachan/SMC/gc/gc_inf_OK.con
-cic:/Cachan/SMC/gc/gc_x.con
-cic:/Cachan/SMC/gc/gc_x_OK.con
-cic:/Cachan/SMC/gc/gc_x_opt.con
-cic:/Cachan/SMC/gc/gc_x_opt_OK.con
-cic:/Cachan/SMC/gc/is_nil.con
-cic:/Cachan/SMC/gc/mark.con
-cic:/Cachan/SMC/gc/mark_lemma_1.con
-cic:/Cachan/SMC/gc/mark_lemma_2.con
-cic:/Cachan/SMC/gc/mark_lemma_3.con
-cic:/Cachan/SMC/gc/new_bsBDDbounded_1.con
-cic:/Cachan/SMC/gc/new_bs_BDDhigh.con
-cic:/Cachan/SMC/gc/new_bs_BDDlow.con
-cic:/Cachan/SMC/gc/new_bs.con
-cic:/Cachan/SMC/gc/new_bs_lemma_1.con
-cic:/Cachan/SMC/gc/new_bs_lemma_2.con
-cic:/Cachan/SMC/gc/new_bs_OK.con
-cic:/Cachan/SMC/gc/new_bs_one.con
-cic:/Cachan/SMC/gc/new_bs_used_nodes_preserved.con
-cic:/Cachan/SMC/gc/new_bs_zero.con
-cic:/Cachan/SMC/gc/new_cfg_OK.con
-cic:/Cachan/SMC/gc/new_cnt_OK.con
-cic:/Cachan/SMC/gc/new_fl.con
-cic:/Cachan/SMC/gc/new_fl_OK.con
-cic:/Cachan/SMC/gc/new_negm_OK.con
-cic:/Cachan/SMC/gc/new_orm_OK.con
-cic:/Cachan/SMC/gc/new_share_OK.con
-cic:/Cachan/SMC/gc/new_univm_OK.con
-cic:/Cachan/SMC/gc/no_new_node_new_bs.con
-cic:/Cachan/SMC/gc/set_closed.con
-cic:/Cachan/SMC/gc/used_node_bs_1.con
-cic:/Cachan/SMC/gc/used_node_bs_1_preserved.con
-cic:/Cachan/SMC/make/BDDmake_bool_fun.con
-cic:/Cachan/SMC/make/BDDmake.con
-cic:/Cachan/SMC/make/BDDmake_keeps_config_OK.con
-cic:/Cachan/SMC/make/BDDmake_node_height_eq_1.con
-cic:/Cachan/SMC/make/BDDmake_node_height_eq.con
-cic:/Cachan/SMC/make/BDDmake_node_height_le.con
-cic:/Cachan/SMC/make/BDDmake_node_OK.con
-cic:/Cachan/SMC/make/BDDmake_preserves_used_nodes.con
-cic:/Cachan/SMC/make/no_dup.con
-cic:/Cachan/SMC/misc/ad_gt_1_lemma.con
-cic:/Cachan/SMC/misc/ad_lt_lemma.con
-cic:/Cachan/SMC/misc/ad_S_compare.con
-cic:/Cachan/SMC/misc/ad_S.con
-cic:/Cachan/SMC/misc/ad_S_is_S.con
-cic:/Cachan/SMC/misc/ad_S_le_then_neq.con
-cic:/Cachan/SMC/misc/ad_S_neq_ad_z.con
-cic:/Cachan/SMC/misc/andb3_lemma_1.con
-cic:/Cachan/SMC/misc/andb3_lemma.con
-cic:/Cachan/SMC/misc/BDDcompare_1.con
-cic:/Cachan/SMC/misc/BDDcompare.con
-cic:/Cachan/SMC/misc/BDDcompare_inf_sup.con
-cic:/Cachan/SMC/misc/BDDcompare_lt.con
-cic:/Cachan/SMC/misc/BDDcompare_sup_inf.con
-cic:/Cachan/SMC/misc/BDDcompare_trans.con
-cic:/Cachan/SMC/misc/BDD_EGAL_complete.con
-cic:/Cachan/SMC/misc/BDD_EGAL_correct.con
-cic:/Cachan/SMC/misc/BDDlt_compare.con
-cic:/Cachan/SMC/misc/BDDvar.con
-cic:/Cachan/SMC/misc/BDDvar_le_max_1.con
-cic:/Cachan/SMC/misc/BDDvar_le_max_2.con
-cic:/Cachan/SMC/misc/BDDvar_max_comm.con
-cic:/Cachan/SMC/misc/BDDvar_max.con
-cic:/Cachan/SMC/misc/BDDvar_max_inf.con
-cic:/Cachan/SMC/misc/BDDvar_max_max.con
-cic:/Cachan/SMC/misc/eq_ad_S_eq.con
-cic:/Cachan/SMC/misc/list_sum.con
-cic:/Cachan/SMC/misc/lt_max_1_2.con
-cic:/Cachan/SMC/misc/lt_max_1.con
-cic:/Cachan/SMC/misc/lt_max_2.con
-cic:/Cachan/SMC/misc/lt_trans_1.con
-cic:/Cachan/SMC/misc/max.con
-cic:/Cachan/SMC/misc/max_x_x_eq_x.con
-cic:/Cachan/SMC/misc/nat_gt_1_lemma.con
-cic:/Cachan/SMC/misc/no_dup_cons_no_dup.con
-cic:/Cachan/SMC/misc/no_dup_cons_no_in.con
-cic:/Cachan/SMC/misc/no_dup_list.ind
-cic:/Cachan/SMC/misc/no_dup_list_ind.con
-cic:/Cachan/SMC/misc/no_dup_sum.con
-cic:/Cachan/SMC/misc/prod_sum.con
-cic:/Cachan/SMC/misc/relation_sum.con
-cic:/Cachan/SMC/mu/ad_to_be_eq1.con
-cic:/Cachan/SMC/mu/ad_to_be_eq.con
-cic:/Cachan/SMC/mu/ad_to_be_ok.con
-cic:/Cachan/SMC/mu/BDDiter2n.con
-cic:/Cachan/SMC/mu/BDDiter2n_lemma1.con
-cic:/Cachan/SMC/mu/BDDiter2n_lemma2.con
-cic:/Cachan/SMC/mu/BDDiter_as_iter.con
-cic:/Cachan/SMC/mu/BDDiter.con
-cic:/Cachan/SMC/mu/BDDmu_eval.con
-cic:/Cachan/SMC/mu/BDDmu_eval_ok.con
-cic:/Cachan/SMC/mu/be_iter1.con
-cic:/Cachan/SMC/mu/be_iter1eq2.con
-cic:/Cachan/SMC/mu/be_iter1_fix_ex.con
-cic:/Cachan/SMC/mu/be_iter1_inc.con
-cic:/Cachan/SMC/mu/be_iter1_le_preserved.con
-cic:/Cachan/SMC/mu/be_iter1_n_le.con
-cic:/Cachan/SMC/mu/be_iter1_ok.con
-cic:/Cachan/SMC/mu/be_iter1_plus1.con
-cic:/Cachan/SMC/mu/be_iter1_plus.con
-cic:/Cachan/SMC/mu/be_iter1_preserves_eq.con
-cic:/Cachan/SMC/mu/be_iter2.con
-cic:/Cachan/SMC/mu/be_iter2n_0.con
-cic:/Cachan/SMC/mu/be_iter2n_2n.con
-cic:/Cachan/SMC/mu/be_iter2n.con
-cic:/Cachan/SMC/mu/be_iter2n_eq_preserved_1.con
-cic:/Cachan/SMC/mu/be_iter2n_eq_preserved_2.con
-cic:/Cachan/SMC/mu/be_iter2n_eq_preserved.con
-cic:/Cachan/SMC/mu/be_iter2n_false.con
-cic:/Cachan/SMC/mu/be_iter2n_is_lfp_be.con
-cic:/Cachan/SMC/mu/be_iter2n_le_preserved.con
-cic:/Cachan/SMC/mu/be_iter2n_prop_preserved.con
-cic:/Cachan/SMC/mu/be_iter2n_true.con
-cic:/Cachan/SMC/mu/be_iter.con
-cic:/Cachan/SMC/mu/be_iter_eq_1.con
-cic:/Cachan/SMC/mu/be_iter_eq_preserved_1.con
-cic:/Cachan/SMC/mu/be_iter_eq_preserved.con
-cic:/Cachan/SMC/mu/be_iter_is_lfp_be.con
-cic:/Cachan/SMC/mu/be_iter_le_preserved.con
-cic:/Cachan/SMC/mu/be_iter_prop_preserved.con
-cic:/Cachan/SMC/mu/be_le1.con
-cic:/Cachan/SMC/mu/be_le1_le.con
-cic:/Cachan/SMC/mu/be_le_ens_inc.con
-cic:/Cachan/SMC/mu/be_le_le1.con
-cic:/Cachan/SMC/mu/be_le_zero.con
-cic:/Cachan/SMC/mu/beq_complete.con
-cic:/Cachan/SMC/mu/beq_correct.con
-cic:/Cachan/SMC/mu/beq_Eq_true.con
-cic:/Cachan/SMC/mu/be_to_be_inc.con
-cic:/Cachan/SMC/mu/bool_expr_to_var_env''_card.con
-cic:/Cachan/SMC/mu/bool_expr_to_var_env''.con
-cic:/Cachan/SMC/mu/bool_expr_to_var_env''_finite.con
-cic:/Cachan/SMC/mu/Brel_env.con
-cic:/Cachan/SMC/mu/Btrans_env.con
-cic:/Cachan/SMC/mu/card_Evar_env''LSU_lemma.con
-cic:/Cachan/SMC/mu/card_imagef1'lemma.con
-cic:/Cachan/SMC/mu/card_imagef1'orf2'lemma.con
-cic:/Cachan/SMC/mu/card_imagef2'lemma.con
-cic:/Cachan/SMC/mu/cardinal_Union.con
-cic:/Cachan/SMC/mu/cfgnode_eq.con
-cic:/Cachan/SMC/mu/cfg_re_bre_ok.con
-cic:/Cachan/SMC/mu/cfg_re_bre_ok_put.con
-cic:/Cachan/SMC/mu/cfg_te_bte_ok.con
-cic:/Cachan/SMC/mu/cfg_ul_bre_cons_ok.con
-cic:/Cachan/SMC/mu/cfg_ul_bre_ok.con
-cic:/Cachan/SMC/mu/cfg_ul_bre_ok_put.con
-cic:/Cachan/SMC/mu/cfg_ul_bte_cons_ok.con
-cic:/Cachan/SMC/mu/cfg_ul_bte_ok.con
-cic:/Cachan/SMC/mu/cfg_ul_re_bre_ok_preserved.con
-cic:/Cachan/SMC/mu/cfg_ul_te_bte_ok_preserved.con
-cic:/Cachan/SMC/mu/decreasing_be_seq_1.con
-cic:/Cachan/SMC/mu/decreasing_be_seq.con
-cic:/Cachan/SMC/mu/decreasing_ens_seq.con
-cic:/Cachan/SMC/mu/decreasing_seq.con
-cic:/Cachan/SMC/mu/Eenv''_var''card.con
-cic:/Cachan/SMC/mu/Eenv''_var''finite.con
-cic:/Cachan/SMC/mu/Eenv_var''LU_card.con
-cic:/Cachan/SMC/mu/Eenv_var''LU_finite.con
-cic:/Cachan/SMC/mu/empty_map_card.con
-cic:/Cachan/SMC/mu/eval_be_independent.con
-cic:/Cachan/SMC/mu/Evar_env'.con
-cic:/Cachan/SMC/mu/Evar_env''.con
-cic:/Cachan/SMC/mu/Evar_env''LSU.con
-cic:/Cachan/SMC/mu/Evar_env'LSU.con
-cic:/Cachan/SMC/mu/Evar_env''LSU_finite.con
-cic:/Cachan/SMC/mu/Evar_env''LSULU.con
-cic:/Cachan/SMC/mu/Evar_env''LU.con
-cic:/Cachan/SMC/mu/Evar_env'LU.con
-cic:/Cachan/SMC/mu/Evar_env''ntoSn.con
-cic:/Cachan/SMC/mu/Evar_env'ntoSn.con
-cic:/Cachan/SMC/mu/Evar_env''ntoSn_lemma.con
-cic:/Cachan/SMC/mu/Evar_env'ntoSn_lemma.con
-cic:/Cachan/SMC/mu/f1.con
-cic:/Cachan/SMC/mu/f1'.con
-cic:/Cachan/SMC/mu/f2.con
-cic:/Cachan/SMC/mu/f2'.con
-cic:/Cachan/SMC/mu/f_bre_ok.con
-cic:/Cachan/SMC/mu/f_bte_ok.con
-cic:/Cachan/SMC/mu/f_ok.ind
-cic:/Cachan/SMC/mu/f_ok_ind.con
-cic:/Cachan/SMC/mu/fp.con
-cic:/Cachan/SMC/mu/f_P_even.ind
-cic:/Cachan/SMC/mu/f_P_even_ind.con
-cic:/Cachan/SMC/mu/imagef1.con
-cic:/Cachan/SMC/mu/imagef1'.con
-cic:/Cachan/SMC/mu/imagef1'finite.con
-cic:/Cachan/SMC/mu/imagef1lemma'.con
-cic:/Cachan/SMC/mu/imagef1'orf2'.con
-cic:/Cachan/SMC/mu/imagef1orf2.con
-cic:/Cachan/SMC/mu/imagef1'orf2'finite.con
-cic:/Cachan/SMC/mu/imagef1'orf2'lemma.con
-cic:/Cachan/SMC/mu/imagef2.con
-cic:/Cachan/SMC/mu/imagef2'.con
-cic:/Cachan/SMC/mu/imagef2'finite.con
-cic:/Cachan/SMC/mu/imagef2lemma'.con
-cic:/Cachan/SMC/mu/incl_eq.con
-cic:/Cachan/SMC/mu/increasing_be_seq_1.con
-cic:/Cachan/SMC/mu/increasing_seq.con
-cic:/Cachan/SMC/mu/iter2n.con
-cic:/Cachan/SMC/mu/iter.con
-cic:/Cachan/SMC/mu/le_minus_le.con
-cic:/Cachan/SMC/mu/le_minus_minus.con
-cic:/Cachan/SMC/mu/lfp_be.con
-cic:/Cachan/SMC/mu/lfp_be_lfp.con
-cic:/Cachan/SMC/mu/lfp.con
-cic:/Cachan/SMC/mu/lt_mn_minus.con
-cic:/Cachan/SMC/mu/lx'N.con
-cic:/Cachan/SMC/mu/lxN.con
-cic:/Cachan/SMC/mu/M0inEvar_env''.con
-cic:/Cachan/SMC/mu/Map_eq_complete.con
-cic:/Cachan/SMC/mu/Map_eq.con
-cic:/Cachan/SMC/mu/Map_eq_correct.con
-cic:/Cachan/SMC/mu/Map_eq_dec.con
-cic:/Cachan/SMC/mu/mf_be_ok.con
-cic:/Cachan/SMC/mu/mf.con
-cic:/Cachan/SMC/mu/mf_fix_ex.con
-cic:/Cachan/SMC/mu/mf_inc.con
-cic:/Cachan/SMC/mu/mf_lfp.con
-cic:/Cachan/SMC/mu/mf_preserves_eq.con
-cic:/Cachan/SMC/mu/mfs.con
-cic:/Cachan/SMC/mu/minus_n_m_le_n.con
-cic:/Cachan/SMC/mu/minusUL0_var_lu.con
-cic:/Cachan/SMC/mu/mu_all_bre_ok.con
-cic:/Cachan/SMC/mu/mu_all_bte_ok.con
-cic:/Cachan/SMC/mu/mu_all_eval_lu.con
-cic:/Cachan/SMC/mu/mu_and_bre_ok.con
-cic:/Cachan/SMC/mu/mu_and_bte_ok.con
-cic:/Cachan/SMC/mu/mu_ap_ok_inv.con
-cic:/Cachan/SMC/mu/mu_eval.con
-cic:/Cachan/SMC/mu/mu_eval_lemma1.con
-cic:/Cachan/SMC/mu/mu_eval_lemma2.con
-cic:/Cachan/SMC/mu/mu_eval_mu_is_lfp.con
-cic:/Cachan/SMC/mu/mu_ex_bre_ok.con
-cic:/Cachan/SMC/mu/mu_ex_bte_ok.con
-cic:/Cachan/SMC/mu/mu_ex_eval_lu.con
-cic:/Cachan/SMC/mu/mu_form_ap_ok.ind
-cic:/Cachan/SMC/mu/mu_form_ap_ok_ind.con
-cic:/Cachan/SMC/mu/mu_form.ind
-cic:/Cachan/SMC/mu/mu_form_ind.con
-cic:/Cachan/SMC/mu/mu_form_rec.con
-cic:/Cachan/SMC/mu/mu_form_rect.con
-cic:/Cachan/SMC/mu/mu_iff_bre_ok.con
-cic:/Cachan/SMC/mu/mu_iff_bte_ok.con
-cic:/Cachan/SMC/mu/mu_impl_bre_ok.con
-cic:/Cachan/SMC/mu/mu_impl_bte_ok.con
-cic:/Cachan/SMC/mu/mu_mu_bre_ok.con
-cic:/Cachan/SMC/mu/mu_or_bre_ok.con
-cic:/Cachan/SMC/mu/mu_or_bte_ok.con
-cic:/Cachan/SMC/mu/mu_rel_free.con
-cic:/Cachan/SMC/mu/mu_t_free.con
-cic:/Cachan/SMC/mu/nat_lu.con
-cic:/Cachan/SMC/mu/nat_lu_var_lu.con
-cic:/Cachan/SMC/munew/be_dash.con
-cic:/Cachan/SMC/munew/bool_fun_of_be_ext1.con
-cic:/Cachan/SMC/munew/dash_be_ok.con
-cic:/Cachan/SMC/munew/dash_renf.con
-cic:/Cachan/SMC/munew/eval_dash_lemma1.con
-cic:/Cachan/SMC/munew/exl_semantics.con
-cic:/Cachan/SMC/munew/forall_lemma1.con
-cic:/Cachan/SMC/munew/mu_all_eval_semantics1.con
-cic:/Cachan/SMC/munew/mu_all_eval_semantics2.con
-cic:/Cachan/SMC/munew/mu_ex_eval_semantics1.con
-cic:/Cachan/SMC/munew/mu_ex_eval_semantics2.con
-cic:/Cachan/SMC/munew/no_dup_lx'_1.con
-cic:/Cachan/SMC/munew/renamef.con
-cic:/Cachan/SMC/munew/renamef_ext.con
-cic:/Cachan/SMC/munew/renamef_id.con
-cic:/Cachan/SMC/munew/renamefS.con
-cic:/Cachan/SMC/munew/renfnad.con
-cic:/Cachan/SMC/munew/renfnat.con
-cic:/Cachan/SMC/munew/replacel_lemma2.con
-cic:/Cachan/SMC/munew/replacel_lemma.con
-cic:/Cachan/SMC/munew/univl_semantics.con
-cic:/Cachan/SMC/munew/var_env'_dash.con
-cic:/Cachan/SMC/munew/var_env''_dash.con
-cic:/Cachan/SMC/munew/var_env_or.con
-cic:/Cachan/SMC/munew/var_env'_or.con
-cic:/Cachan/SMC/mu/rel_env.con
-cic:/Cachan/SMC/mu/re_put.con
-cic:/Cachan/SMC/mu/re_to_be_dec.con
-cic:/Cachan/SMC/mu/re_to_be_inc.con
-cic:/Cachan/SMC/mu/same_set_finite.con
-cic:/Cachan/SMC/mu/same_set_same_cardinal.con
-cic:/Cachan/SMC/mu/seq.con
-cic:/Cachan/SMC/mu/seq_eq.con
-cic:/Cachan/SMC/mu/seq_inj.con
-cic:/Cachan/SMC/mu/seq_surj.con
-cic:/Cachan/SMC/muset/env_to_be_lemma1.con
-cic:/Cachan/SMC/muset/env_to_be_lemma.con
-cic:/Cachan/SMC/muset/le_minus_le1.con
-cic:/Cachan/SMC/muset/muevaleqset.con
-cic:/Cachan/SMC/muset/mu_form2set.con
-cic:/Cachan/SMC/muset/new_t_to_rel.con
-cic:/Cachan/SMC/muset/rel_1.con
-cic:/Cachan/SMC/muset/relfreeeven.con
-cic:/Cachan/SMC/muset/re_sre_ok.con
-cic:/Cachan/SMC/muset/set_0.con
-cic:/Cachan/SMC/muset/set_1.con
-cic:/Cachan/SMC/muset/set_all.con
-cic:/Cachan/SMC/muset/set_and.con
-cic:/Cachan/SMC/muset/set_ap.con
-cic:/Cachan/SMC/muset/set_ap_state_set.con
-cic:/Cachan/SMC/muset/set_ex.ind
-cic:/Cachan/SMC/muset/set_ex_ind.con
-cic:/Cachan/SMC/muset/set_iff.con
-cic:/Cachan/SMC/muset/set_impl.con
-cic:/Cachan/SMC/muset/set_mu.con
-cic:/Cachan/SMC/muset/set_neg.con
-cic:/Cachan/SMC/muset/set_or.con
-cic:/Cachan/SMC/muset/set_renv.con
-cic:/Cachan/SMC/muset/set_tenv.con
-cic:/Cachan/SMC/muset/sre_put.con
-cic:/Cachan/SMC/muset/state_rel.con
-cic:/Cachan/SMC/muset/state_set.con
-cic:/Cachan/SMC/muset/te_ste_ok.con
-cic:/Cachan/SMC/muset/t_to_rel1.con
-cic:/Cachan/SMC/muset/t_to_rel.con
-cic:/Cachan/SMC/muset/var_env'_to_env''_to_env'.con
-cic:/Cachan/SMC/muset/ve''_to_be.con
-cic:/Cachan/SMC/muset/ve''_to_be_ok1.con
-cic:/Cachan/SMC/muset/ve''_to_be_ok2.con
-cic:/Cachan/SMC/muset/ve''_to_be_ok3.con
-cic:/Cachan/SMC/muset/ve''_to_be_ok.con
-cic:/Cachan/SMC/mu/singleton_add_empty.con
-cic:/Cachan/SMC/mu/singleton_cardinal_one.con
-cic:/Cachan/SMC/mu/Splus_nm.con
-cic:/Cachan/SMC/mu/trans_env.con
-cic:/Cachan/SMC/mu/two_power.con
-cic:/Cachan/SMC/mu/unprimed_var.con
-cic:/Cachan/SMC/mu/var_env''cardinal_one.con
-cic:/Cachan/SMC/mu/var_env_eq.con
-cic:/Cachan/SMC/mu/var_env''le.con
-cic:/Cachan/SMC/mu/var_env''le_refl.con
-cic:/Cachan/SMC/mu/var_env''le_trans.con
-cic:/Cachan/SMC/mu/var_env''M0.con
-cic:/Cachan/SMC/mu/var_env''singleton.con
-cic:/Cachan/SMC/mu/var_env'_to_env''.con
-cic:/Cachan/SMC/mu/var_env'_to_env''_lemma3.con
-cic:/Cachan/SMC/mu/var_env'_to_var_env''_lemma1.con
-cic:/Cachan/SMC/mu/var_env'_to_var_env''_lemma2.con
-cic:/Cachan/SMC/mu/var_lu.con
-cic:/Cachan/SMC/mu/var_lu_nat_lu.con
-cic:/Cachan/SMC/mu/zero_lt_pow.con
-cic:/Cachan/SMC/myMap/eqmap_equiv.con
-cic:/Cachan/SMC/myMap/F.con
-cic:/Cachan/SMC/myMap/f_OK.con
-cic:/Cachan/SMC/myMap/makeM2_MapDom_lemma.con
-cic:/Cachan/SMC/myMap/map_app_list1.con
-cic:/Cachan/SMC/myMap/map_app_list1_lemma_1.con
-cic:/Cachan/SMC/myMap/map_app_list1_lemma_2.con
-cic:/Cachan/SMC/myMap/map_app_list1_lemma_3.con
-cic:/Cachan/SMC/myMap/map_app_list1_lemma_4.con
-cic:/Cachan/SMC/myMap/MapDomRestrByApp1.con
-cic:/Cachan/SMC/myMap/MapDomRestrByApp1_lemma_1.con
-cic:/Cachan/SMC/myMap/MapDomRestrByApp1_lemma_2.con
-cic:/Cachan/SMC/myMap/MapDomRestrByApp1_lemma_3.con
-cic:/Cachan/SMC/myMap/MapDomRestrByApp1_lemma_4.con
-cic:/Cachan/SMC/myMap/MapDomRestrTo_DomBy.con
-cic:/Cachan/SMC/myMap/MapDomRestrTo_DomBy_lemma_1.con
-cic:/Cachan/SMC/myMap/MapDomRestrTo_DomBy_lemma_2.con
-cic:/Cachan/SMC/myMap/MapGet2.con
-cic:/Cachan/SMC/myMap/MapGet3.con
-cic:/Cachan/SMC/myMap/MapMerge_assoc.con
-cic:/Cachan/SMC/myMap/MapMerge_eq.con
-cic:/Cachan/SMC/myMap/MapMerge_neutral_left.con
-cic:/Cachan/SMC/myMap/MapMerge_neutral_right.con
-cic:/Cachan/SMC/myMap/Mapn.con
-cic:/Cachan/SMC/myMap/MapPut2.con
-cic:/Cachan/SMC/myMap/MapPut2_semantics.con
-cic:/Cachan/SMC/myMap/MapPut3.con
-cic:/Cachan/SMC/myMap/MapPut3_semantics.con
-cic:/Cachan/SMC/myMap/my_alist_of_map_lemma_1.con
-cic:/Cachan/SMC/myMap/my_alist_of_map_lemma_2.con
-cic:/Cachan/SMC/myMap/my_alist_of_map_lemma_3.con
-cic:/Cachan/SMC/myMap/my_fold_right_aapp.con
-cic:/Cachan/SMC/myMap/my_fold_right_lemma.con
-cic:/Cachan/SMC/myMap/myMapFold_as_fold_1.con
-cic:/Cachan/SMC/myMap/myMapFold_as_fold_2.con
-cic:/Cachan/SMC/myMap/myMapFold_as_fold.con
-cic:/Cachan/SMC/myMap/myMapFold_lemma.con
-cic:/Cachan/SMC/myMap/no_dup_alist.con
-cic:/Cachan/SMC/myMap/no_dup_alist_of_Map.con
-cic:/Cachan/SMC/myMap/op_eq_2.con
-cic:/Cachan/SMC/neg/BDDneg_1.con
-cic:/Cachan/SMC/neg/BDDneg_1_lemma.con
-cic:/Cachan/SMC/op/BDDand.con
-cic:/Cachan/SMC/op/BDDand_config_OK.con
-cic:/Cachan/SMC/op/BDDand_is_and.con
-cic:/Cachan/SMC/op/BDDand_list_OK.con
-cic:/Cachan/SMC/op/BDDand_list_OK_cons.con
-cic:/Cachan/SMC/op/BDDand_node_OK.con
-cic:/Cachan/SMC/op/BDDand_used_nodes_preserved.con
-cic:/Cachan/SMC/op/BDDand_var_le.con
-cic:/Cachan/SMC/op/BDDiff.con
-cic:/Cachan/SMC/op/BDDiff_config_OK.con
-cic:/Cachan/SMC/op/BDDiff_is_iff.con
-cic:/Cachan/SMC/op/BDDiff_list_OK.con
-cic:/Cachan/SMC/op/BDDiff_list_OK_cons.con
-cic:/Cachan/SMC/op/BDDiff_node_OK.con
-cic:/Cachan/SMC/op/BDDiff_used_nodes_preserved.con
-cic:/Cachan/SMC/op/BDDimpl.con
-cic:/Cachan/SMC/op/BDDimpl_config_OK.con
-cic:/Cachan/SMC/op/BDDimpl_is_impl.con
-cic:/Cachan/SMC/op/BDDimpl_list_OK.con
-cic:/Cachan/SMC/op/BDDimpl_list_OK_cons.con
-cic:/Cachan/SMC/op/BDDimpl_node_OK.con
-cic:/Cachan/SMC/op/BDDimpl_used_nodes_preserved.con
-cic:/Cachan/SMC/op/BDDneg.con
-cic:/Cachan/SMC/op/BDDneg_config_OK.con
-cic:/Cachan/SMC/op/BDDneg_is_neg.con
-cic:/Cachan/SMC/op/BDDneg_list_OK.con
-cic:/Cachan/SMC/op/BDDneg_list_OK_cons.con
-cic:/Cachan/SMC/op/BDDneg_node_OK.con
-cic:/Cachan/SMC/op/BDDneg_used_nodes_preserved.con
-cic:/Cachan/SMC/op/BDDneg_var_eq.con
-cic:/Cachan/SMC/op/BDDor.con
-cic:/Cachan/SMC/op/BDDor_config_OK.con
-cic:/Cachan/SMC/op/BDDor_is_or.con
-cic:/Cachan/SMC/op/BDDor_list_OK.con
-cic:/Cachan/SMC/op/BDDor_list_OK_cons.con
-cic:/Cachan/SMC/op/BDDor_node_OK.con
-cic:/Cachan/SMC/op/BDDor_used_nodes_preserved.con
-cic:/Cachan/SMC/op/BDDor_var_le.con
-cic:/Cachan/SMC/op/BDDvar_make.con
-cic:/Cachan/SMC/op/BDDvar_make_config_OK.con
-cic:/Cachan/SMC/op/BDDvar_make_is_var.con
-cic:/Cachan/SMC/op/BDDvar_make_list_OK.con
-cic:/Cachan/SMC/op/BDDvar_make_list_OK_cons.con
-cic:/Cachan/SMC/op/BDDvar_make_node_OK.con
-cic:/Cachan/SMC/op/BDDvar_make_used_nodes_preserved.con
-cic:/Cachan/SMC/or/BDDor_1.con
-cic:/Cachan/SMC/or/BDDor_1_lemma.con
-cic:/Cachan/SMC/quant/ad_list_neq.con
-cic:/Cachan/SMC/quant/and_eq.con
-cic:/Cachan/SMC/quant/and_le2.con
-cic:/Cachan/SMC/quant/and_le.con
-cic:/Cachan/SMC/quant/and_ok_inv.con
-cic:/Cachan/SMC/quant/and_x_free.con
-cic:/Cachan/SMC/quant/ap.con
-cic:/Cachan/SMC/quant/ap'.con
-cic:/Cachan/SMC/quant/ap'_eq_ap.con
-cic:/Cachan/SMC/quant/ap_neq_ap'.con
-cic:/Cachan/SMC/quant/BDDex.con
-cic:/Cachan/SMC/quant/BDDex_config_OK.con
-cic:/Cachan/SMC/quant/BDDex_is_ex.con
-cic:/Cachan/SMC/quant/BDDexl.con
-cic:/Cachan/SMC/quant/BDDexl_config_OK.con
-cic:/Cachan/SMC/quant/BDDexl_is_exl.con
-cic:/Cachan/SMC/quant/BDDex_list_OK.con
-cic:/Cachan/SMC/quant/BDDex_list_OK_cons.con
-cic:/Cachan/SMC/quant/BDDexl_lemma.con
-cic:/Cachan/SMC/quant/BDDexl_list_OK.con
-cic:/Cachan/SMC/quant/BDDexl_list_OK_cons.con
-cic:/Cachan/SMC/quant/BDDexl_node_OK.con
-cic:/Cachan/SMC/quant/BDDexl_used_nodes_preserved.con
-cic:/Cachan/SMC/quant/BDDex_node_OK.con
-cic:/Cachan/SMC/quant/BDDex_used_nodes_preserved.con
-cic:/Cachan/SMC/quant/BDDmu_all.con
-cic:/Cachan/SMC/quant/BDDmu_all_config_OK.con
-cic:/Cachan/SMC/quant/BDDmu_all_is_mu_all.con
-cic:/Cachan/SMC/quant/BDDmu_all_lemma.con
-cic:/Cachan/SMC/quant/BDDmu_all_list_OK.con
-cic:/Cachan/SMC/quant/BDDmu_all_list_OK_cons.con
-cic:/Cachan/SMC/quant/BDDmu_all_node_OK.con
-cic:/Cachan/SMC/quant/BDDmu_all_used_nodes_preserved.con
-cic:/Cachan/SMC/quant/BDDmu_ex.con
-cic:/Cachan/SMC/quant/BDDmu_ex_config_OK.con
-cic:/Cachan/SMC/quant/BDDmu_ex_is_mu_ex.con
-cic:/Cachan/SMC/quant/BDDmu_ex_lemma.con
-cic:/Cachan/SMC/quant/BDDmu_ex_list_OK.con
-cic:/Cachan/SMC/quant/BDDmu_ex_list_OK_cons.con
-cic:/Cachan/SMC/quant/BDDmu_ex_node_OK.con
-cic:/Cachan/SMC/quant/BDDmu_ex_used_nodes_preserved.con
-cic:/Cachan/SMC/quant/BDDreplace.con
-cic:/Cachan/SMC/quant/BDDreplace_config_OK.con
-cic:/Cachan/SMC/quant/BDDreplace_is_replace.con
-cic:/Cachan/SMC/quant/BDDreplacel.con
-cic:/Cachan/SMC/quant/BDDreplacel_config_OK.con
-cic:/Cachan/SMC/quant/BDDreplacel_is_replacel.con
-cic:/Cachan/SMC/quant/BDDreplace_list_OK.con
-cic:/Cachan/SMC/quant/BDDreplace_list_OK_cons.con
-cic:/Cachan/SMC/quant/BDDreplacel_lemma.con
-cic:/Cachan/SMC/quant/BDDreplacel_list_OK.con
-cic:/Cachan/SMC/quant/BDDreplacel_list_OK_cons.con
-cic:/Cachan/SMC/quant/BDDreplacel_node_OK.con
-cic:/Cachan/SMC/quant/BDDreplacel_used_nodes_preserved.con
-cic:/Cachan/SMC/quant/BDDreplace_node_OK.con
-cic:/Cachan/SMC/quant/BDDreplace_used_nodes_preserved.con
-cic:/Cachan/SMC/quant/BDDsubst.con
-cic:/Cachan/SMC/quant/BDDsubst_config_OK.con
-cic:/Cachan/SMC/quant/BDDsubst_is_subst1.con
-cic:/Cachan/SMC/quant/BDDsubst_is_subst.con
-cic:/Cachan/SMC/quant/BDDsubst_lemma.con
-cic:/Cachan/SMC/quant/BDDsubst_list_OK.con
-cic:/Cachan/SMC/quant/BDDsubst_list_OK_cons.con
-cic:/Cachan/SMC/quant/BDDsubst_node_OK.con
-cic:/Cachan/SMC/quant/BDDsubst_used_nodes_preserved.con
-cic:/Cachan/SMC/quant/BDDuniv.con
-cic:/Cachan/SMC/quant/BDDuniv_config_OK.con
-cic:/Cachan/SMC/quant/BDDuniv_is_univ.con
-cic:/Cachan/SMC/quant/BDDunivl.con
-cic:/Cachan/SMC/quant/BDDunivl_config_OK.con
-cic:/Cachan/SMC/quant/BDDuniv_list_OK.con
-cic:/Cachan/SMC/quant/BDDuniv_list_OK_cons.con
-cic:/Cachan/SMC/quant/BDDunivl_is_univl.con
-cic:/Cachan/SMC/quant/BDDunivl_lemma.con
-cic:/Cachan/SMC/quant/BDDunivl_list_OK.con
-cic:/Cachan/SMC/quant/BDDunivl_list_OK_cons.con
-cic:/Cachan/SMC/quant/BDDunivl_node_OK.con
-cic:/Cachan/SMC/quant/BDDunivl_used_nodes_preserved.con
-cic:/Cachan/SMC/quant/BDDuniv_node_OK.con
-cic:/Cachan/SMC/quant/BDDuniv_used_nodes_preserved.con
-cic:/Cachan/SMC/quant/BDDuniv_var_le.con
-cic:/Cachan/SMC/quant/be_eq.con
-cic:/Cachan/SMC/quant/be_eq_dec_complete.con
-cic:/Cachan/SMC/quant/be_eq_dec.con
-cic:/Cachan/SMC/quant/be_eq_dec_correct.con
-cic:/Cachan/SMC/quant/be_eq_dec_eq.con
-cic:/Cachan/SMC/quant/be_eq_eq_dec.con
-cic:/Cachan/SMC/quant/be_eq_le.con
-cic:/Cachan/SMC/quant/be_eq_refl.con
-cic:/Cachan/SMC/quant/be_eq_sym.con
-cic:/Cachan/SMC/quant/be_eq_trans.con
-cic:/Cachan/SMC/quant/be_ex.con
-cic:/Cachan/SMC/quant/be_le2.con
-cic:/Cachan/SMC/quant/be_le2_le.con
-cic:/Cachan/SMC/quant/be_le_antisym.con
-cic:/Cachan/SMC/quant/be_le.con
-cic:/Cachan/SMC/quant/be_le_le2.con
-cic:/Cachan/SMC/quant/be_le_not_1.con
-cic:/Cachan/SMC/quant/be_le_refl.con
-cic:/Cachan/SMC/quant/be_le_trans.con
-cic:/Cachan/SMC/quant/be_ok_be_x_free.con
-cic:/Cachan/SMC/quant/be_ok.ind
-cic:/Cachan/SMC/quant/be_ok_ind.con
-cic:/Cachan/SMC/quant/be_x_free_be_ok.con
-cic:/Cachan/SMC/quant/be_x_free.con
-cic:/Cachan/SMC/quant/bool_fun_and_ext.con
-cic:/Cachan/SMC/quant/bool_fun_exl.con
-cic:/Cachan/SMC/quant/bool_fun_exl_preserves_eq.con
-cic:/Cachan/SMC/quant/bool_fun_iff_ext.con
-cic:/Cachan/SMC/quant/bool_fun_impl_ext.con
-cic:/Cachan/SMC/quant/bool_fun_mu_all.con
-cic:/Cachan/SMC/quant/bool_fun_mu_all_preserves_eq.con
-cic:/Cachan/SMC/quant/bool_fun_mu_ex.con
-cic:/Cachan/SMC/quant/bool_fun_mu_ex_preserves_eq.con
-cic:/Cachan/SMC/quant/bool_fun_neg_ext.con
-cic:/Cachan/SMC/quant/bool_fun_of_be_ext.con
-cic:/Cachan/SMC/quant/bool_fun_or_ext.con
-cic:/Cachan/SMC/quant/bool_fun_replace.con
-cic:/Cachan/SMC/quant/bool_fun_replacel.con
-cic:/Cachan/SMC/quant/bool_fun_replacel_preserves_eq.con
-cic:/Cachan/SMC/quant/bool_fun_replace_preserves_eq.con
-cic:/Cachan/SMC/quant/bool_fun_restrict1.con
-cic:/Cachan/SMC/quant/bool_fun_restrict1_eq_restrict.con
-cic:/Cachan/SMC/quant/bool_fun_restrict_eq_subst.con
-cic:/Cachan/SMC/quant/bool_fun_subst1.con
-cic:/Cachan/SMC/quant/bool_fun_subst1_eq_subst.con
-cic:/Cachan/SMC/quant/bool_fun_subst.con
-cic:/Cachan/SMC/quant/bool_fun_subst_preserves_eq.con
-cic:/Cachan/SMC/quant/bool_fun_univl.con
-cic:/Cachan/SMC/quant/bool_fun_univl_preserves_eq.con
-cic:/Cachan/SMC/quant/bool_fun_var_ext.con
-cic:/Cachan/SMC/quant/bool_to_be.con
-cic:/Cachan/SMC/quant/bool_to_be_to_bf.con
-cic:/Cachan/SMC/quant/bool_to_bf.con
-cic:/Cachan/SMC/quant/eq_neg_eq.con
-cic:/Cachan/SMC/quant/eval_be'.con
-cic:/Cachan/SMC/quant/exl.con
-cic:/Cachan/SMC/quant/ex_le2.con
-cic:/Cachan/SMC/quant/exl_le2.con
-cic:/Cachan/SMC/quant/exl_OK.con
-cic:/Cachan/SMC/quant/exl_x_free.con
-cic:/Cachan/SMC/quant/ex_OK.con
-cic:/Cachan/SMC/quant/ex_x_free.con
-cic:/Cachan/SMC/quant/forall_.con
-cic:/Cachan/SMC/quant/forall_OK.con
-cic:/Cachan/SMC/quant/iff_eq.con
-cic:/Cachan/SMC/quant/iff_ok_inv.con
-cic:/Cachan/SMC/quant/impl_eq.con
-cic:/Cachan/SMC/quant/impl_le2.con
-cic:/Cachan/SMC/quant/impl_le.con
-cic:/Cachan/SMC/quant/impl_ok_inv.con
-cic:/Cachan/SMC/quant/impl_x_free.con
-cic:/Cachan/SMC/quant/in_lx'_1.con
-cic:/Cachan/SMC/quant/in_lx'_1_conv.con
-cic:/Cachan/SMC/quant/in_lx'.con
-cic:/Cachan/SMC/quant/length_lx_1_eq_lx'_1.con
-cic:/Cachan/SMC/quant/length_lx_eq_lx'.con
-cic:/Cachan/SMC/quant/lt_O_n_lx'_1.con
-cic:/Cachan/SMC/quant/lx_1.con
-cic:/Cachan/SMC/quant/lx'_1.con
-cic:/Cachan/SMC/quant/lx_1_neg_lx'_1.con
-cic:/Cachan/SMC/quant/lx.con
-cic:/Cachan/SMC/quant/lx'.con
-cic:/Cachan/SMC/quant/lx_neq_lx'.con
-cic:/Cachan/SMC/quant/mu_all_eq.con
-cic:/Cachan/SMC/quant/mu_all_eval.con
-cic:/Cachan/SMC/quant/mu_all_eval_ok.con
-cic:/Cachan/SMC/quant/mu_all_le2.con
-cic:/Cachan/SMC/quant/mu_all_le.con
-cic:/Cachan/SMC/quant/mu_all_x_free.con
-cic:/Cachan/SMC/quant/mu_ex_eq.con
-cic:/Cachan/SMC/quant/mu_ex_eval.con
-cic:/Cachan/SMC/quant/mu_ex_eval_ok.con
-cic:/Cachan/SMC/quant/mu_ex_le2.con
-cic:/Cachan/SMC/quant/mu_ex_le.con
-cic:/Cachan/SMC/quant/mu_ex_x_free.con
-cic:/Cachan/SMC/quant/neg_eq_eq.con
-cic:/Cachan/SMC/quant/neg_ok_inv.con
-cic:/Cachan/SMC/quant/or_eq.con
-cic:/Cachan/SMC/quant/or_le2.con
-cic:/Cachan/SMC/quant/or_le.con
-cic:/Cachan/SMC/quant/or_ok_inv.con
-cic:/Cachan/SMC/quant/replace.con
-cic:/Cachan/SMC/quant/replacel.con
-cic:/Cachan/SMC/quant/replace_le2.con
-cic:/Cachan/SMC/quant/replacel_le2.con
-cic:/Cachan/SMC/quant/replacel_OK.con
-cic:/Cachan/SMC/quant/replacel_x_free.con
-cic:/Cachan/SMC/quant/replace_OK.con
-cic:/Cachan/SMC/quant/replace_x_free.con
-cic:/Cachan/SMC/quant/restrict.con
-cic:/Cachan/SMC/quant/restrict_OK.con
-cic:/Cachan/SMC/quant/restrict_x_free.con
-cic:/Cachan/SMC/quant/subst.con
-cic:/Cachan/SMC/quant/subst_le2.con
-cic:/Cachan/SMC/quant/subst_ok.con
-cic:/Cachan/SMC/quant/subst_x_free.con
-cic:/Cachan/SMC/quant/univl.con
-cic:/Cachan/SMC/quant/univ_le2.con
-cic:/Cachan/SMC/quant/univl_le2.con
-cic:/Cachan/SMC/quant/univl_OK.con
-cic:/Cachan/SMC/quant/univl_x_free.con
-cic:/Cachan/SMC/quant/univ_x_free.con
-cic:/Cachan/SMC/quant/var_env'.con
-cic:/Cachan/SMC/quant/var_env''.con
-cic:/Cachan/SMC/quant/var_env_to_env'.con
-cic:/Cachan/SMC/quant/var_env'_to_env.con
-cic:/Cachan/SMC/quant/var_env''_to_env.con
-cic:/Cachan/SMC/quant/var_env''_to_env'.con
-cic:/Cachan/SMC/quant/var_ok_inv.con
-cic:/Cachan/SMC/tauto/BDDof_bool_expr.con
-cic:/Cachan/SMC/tauto/BDDof_bool_expr_correct.con
-cic:/Cachan/SMC/tauto/init_list_OK.con
-cic:/Cachan/SMC/tauto/is_tauto.con
-cic:/Cachan/SMC/tauto/is_tauto_lemma.con
-cic:/Cachan/SMC/univ/BDDuniv_1.con
-cic:/Cachan/SMC/univ/BDDuniv_1_lemma.con
-cic:/Coq/Arith/Between/bet_eq.con
-cic:/Coq/Arith/Between/between.ind
-cic:/Coq/Arith/Between/between_ind.con
-cic:/Coq/Arith/Between/between_in_int.con
-cic:/Coq/Arith/Between/between_le.con
-cic:/Coq/Arith/Between/between_not_exists.con
-cic:/Coq/Arith/Between/between_or_exists.con
-cic:/Coq/Arith/Between/between_restr.con
-cic:/Coq/Arith/Between/between_Sk_l.con
-cic:/Coq/Arith/Between/event_O.con
-cic:/Coq/Arith/Between/eventually.con
-cic:/Coq/Arith/Between/exists_between.ind
-cic:/Coq/Arith/Between/exists_between_ind.con
-cic:/Coq/Arith/Between/exists_in_int.con
-cic:/Coq/Arith/Between/exists_le_S.con
-cic:/Coq/Arith/Between/exists_lt.con
-cic:/Coq/Arith/Between/exists_S_le.con
-cic:/Coq/Arith/Between/in_int_between.con
-cic:/Coq/Arith/Between/in_int.con
-cic:/Coq/Arith/Between/in_int_exists.con
-cic:/Coq/Arith/Between/in_int_intro.con
-cic:/Coq/Arith/Between/in_int_lt.con
-cic:/Coq/Arith/Between/in_int_p_Sq.con
-cic:/Coq/Arith/Between/in_int_S.con
-cic:/Coq/Arith/Between/in_int_Sp_q.con
-cic:/Coq/Arith/Between/nth_le.con
-cic:/Coq/Arith/Between/P_nth.ind
-cic:/Coq/Arith/Between/P_nth_ind.con
-cic:/Coq/Arith/Bool_nat/lt_ge_dec.con
-cic:/Coq/Arith/Bool_nat/nat_eq_bool.con
-cic:/Coq/Arith/Bool_nat/nat_ge_lt_bool.con
-cic:/Coq/Arith/Bool_nat/nat_gt_le_bool.con
-cic:/Coq/Arith/Bool_nat/nat_le_gt_bool.con
-cic:/Coq/Arith/Bool_nat/nat_lt_ge_bool.con
-cic:/Coq/Arith/Bool_nat/nat_noteq_bool.con
-cic:/Coq/Arith/Bool_nat/notzerop_bool.con
-cic:/Coq/Arith/Bool_nat/notzerop.con
-cic:/Coq/Arith/Bool_nat/zerop_bool.con
-cic:/Coq/Arith/Compare_dec/dec_ge.con
-cic:/Coq/Arith/Compare_dec/dec_gt.con
-cic:/Coq/Arith/Compare_dec/dec_le.con
-cic:/Coq/Arith/Compare_dec/dec_lt.con
-cic:/Coq/Arith/Compare_dec/gt_eq_gt_dec.con
-cic:/Coq/Arith/Compare_dec/le_ge_dec.con
-cic:/Coq/Arith/Compare_dec/le_gt_dec.con
-cic:/Coq/Arith/Compare_dec/le_le_S_dec.con
-cic:/Coq/Arith/Compare_dec/le_lt_dec.con
-cic:/Coq/Arith/Compare_dec/le_lt_eq_dec.con
-cic:/Coq/Arith/Compare_dec/lt_eq_lt_dec.con
-cic:/Coq/Arith/Compare_dec/not_eq.con
-cic:/Coq/Arith/Compare_dec/not_ge.con
-cic:/Coq/Arith/Compare_dec/not_gt.con
-cic:/Coq/Arith/Compare_dec/not_le.con
-cic:/Coq/Arith/Compare_dec/not_lt.con
-cic:/Coq/Arith/Compare_dec/zerop.con
-cic:/Coq/Arith/Compare/discrete_nat.con
-cic:/Coq/Arith/Compare/le_dec.con
-cic:/Coq/Arith/Compare/le_decide.con
-cic:/Coq/Arith/Compare/le_le_S_eq.con
-cic:/Coq/Arith/Compare/le_or_le_S.con
-cic:/Coq/Arith/Compare/lt_or_eq.con
-cic:/Coq/Arith/Compare/Pcompare.con
-cic:/Coq/Arith/Div2/div2.con
-cic:/Coq/Arith/Div2/div2_even.con
-cic:/Coq/Arith/Div2/div2_odd.con
-cic:/Coq/Arith/Div2/double.con
-cic:/Coq/Arith/Div2/double_even.con
-cic:/Coq/Arith/Div2/double_odd.con
-cic:/Coq/Arith/Div2/double_plus.con
-cic:/Coq/Arith/Div2/double_S.con
-cic:/Coq/Arith/Div2/even_2n.con
-cic:/Coq/Arith/Div2/even_div2.con
-cic:/Coq/Arith/Div2/even_double.con
-cic:/Coq/Arith/Div2/even_odd_div2.con
-cic:/Coq/Arith/Div2/even_odd_double.con
-cic:/Coq/Arith/Div2/ind_0_1_SS.con
-cic:/Coq/Arith/Div2/lt_div2.con
-cic:/Coq/Arith/Div2/odd_div2.con
-cic:/Coq/Arith/Div2/odd_double.con
-cic:/Coq/Arith/Div2/odd_S2n.con
-cic:/Coq/Arith/EqNat/beq_nat.con
-cic:/Coq/Arith/EqNat/beq_nat_eq.con
-cic:/Coq/Arith/EqNat/beq_nat_refl.con
-cic:/Coq/Arith/EqNat/eq_eq_nat.con
-cic:/Coq/Arith/EqNat/eq_nat.con
-cic:/Coq/Arith/EqNat/eq_nat_decide.con
-cic:/Coq/Arith/EqNat/eq_nat_elim.con
-cic:/Coq/Arith/EqNat/eq_nat_eq.con
-cic:/Coq/Arith/EqNat/eq_nat_refl.con
-cic:/Coq/Arith/Euclid/diveucl.ind
-cic:/Coq/Arith/Euclid/diveucl_ind.con
-cic:/Coq/Arith/Euclid/diveucl_rec.con
-cic:/Coq/Arith/Euclid/diveucl_rect.con
-cic:/Coq/Arith/Euclid/eucl_dev.con
-cic:/Coq/Arith/Euclid/modulo.con
-cic:/Coq/Arith/Euclid/quotient.con
-cic:/Coq/Arith/Even/even_even_plus.con
-cic:/Coq/Arith/Even/even.ind
-cic:/Coq/Arith/Even/even_ind.con
-cic:/Coq/Arith/Even/even_mult_aux.con
-cic:/Coq/Arith/Even/even_mult_inv_l.con
-cic:/Coq/Arith/Even/even_mult_inv_r.con
-cic:/Coq/Arith/Even/even_mult_l.con
-cic:/Coq/Arith/Even/even_mult_r.con
-cic:/Coq/Arith/Even/even_odd_dec.con
-cic:/Coq/Arith/Even/even_or_odd.con
-cic:/Coq/Arith/Even/even_plus_aux.con
-cic:/Coq/Arith/Even/even_plus_even_inv_l.con
-cic:/Coq/Arith/Even/even_plus_even_inv_r.con
-cic:/Coq/Arith/Even/even_plus_odd_inv_l.con
-cic:/Coq/Arith/Even/even_plus_odd_inv_r.con
-cic:/Coq/Arith/Even/not_even_and_odd.con
-cic:/Coq/Arith/Even/odd_even_plus.con
-cic:/Coq/Arith/Even/odd_ind.con
-cic:/Coq/Arith/Even/odd_mult.con
-cic:/Coq/Arith/Even/odd_mult_inv_l.con
-cic:/Coq/Arith/Even/odd_mult_inv_r.con
-cic:/Coq/Arith/Even/odd_plus_even_inv_l.con
-cic:/Coq/Arith/Even/odd_plus_even_inv_r.con
-cic:/Coq/Arith/Even/odd_plus_l.con
-cic:/Coq/Arith/Even/odd_plus_odd_inv_l.con
-cic:/Coq/Arith/Even/odd_plus_odd_inv_r.con
-cic:/Coq/Arith/Even/odd_plus_r.con
-cic:/Coq/Arith/Factorial/fact.con
-cic:/Coq/Arith/Factorial/fact_le.con
-cic:/Coq/Arith/Factorial/fact_neq_0.con
-cic:/Coq/Arith/Factorial/lt_O_fact.con
-cic:/Coq/Arith/Gt/gt_asym.con
-cic:/Coq/Arith/Gt/gt_irrefl.con
-cic:/Coq/Arith/Gt/gt_le_S.con
-cic:/Coq/Arith/Gt/gt_le_trans.con
-cic:/Coq/Arith/Gt/gt_not_le.con
-cic:/Coq/Arith/Gt/gt_n_S.con
-cic:/Coq/Arith/Gt/gt_O_eq.con
-cic:/Coq/Arith/Gt/gt_pred.con
-cic:/Coq/Arith/Gt/gt_S.con
-cic:/Coq/Arith/Gt/gt_S_le.con
-cic:/Coq/Arith/Gt/gt_S_n.con
-cic:/Coq/Arith/Gt/gt_Sn_n.con
-cic:/Coq/Arith/Gt/gt_Sn_O.con
-cic:/Coq/Arith/Gt/gt_trans.con
-cic:/Coq/Arith/Gt/gt_trans_S.con
-cic:/Coq/Arith/Gt/le_gt_S.con
-cic:/Coq/Arith/Gt/le_gt_trans.con
-cic:/Coq/Arith/Gt/le_not_gt.con
-cic:/Coq/Arith/Gt/le_S_gt.con
-cic:/Coq/Arith/Gt/plus_gt_compat_l.con
-cic:/Coq/Arith/Gt/plus_gt_reg_l.con
-cic:/Coq/Arith/Le/le_antisym.con
-cic:/Coq/Arith/Le/le_elim_rel.con
-cic:/Coq/Arith/Le/le_n_O_eq.con
-cic:/Coq/Arith/Le/le_n_S.con
-cic:/Coq/Arith/Le/le_n_Sn.con
-cic:/Coq/Arith/Le/le_O_n.con
-cic:/Coq/Arith/Le/le_pred.con
-cic:/Coq/Arith/Le/le_pred_n.con
-cic:/Coq/Arith/Le/le_refl.con
-cic:/Coq/Arith/Le/le_S_n.con
-cic:/Coq/Arith/Le/le_Sn_le.con
-cic:/Coq/Arith/Le/le_Sn_n.con
-cic:/Coq/Arith/Le/le_Sn_O.con
-cic:/Coq/Arith/Le/le_trans.con
-cic:/Coq/Arith/Lt/le_lt_n_Sm.con
-cic:/Coq/Arith/Lt/le_lt_or_eq.con
-cic:/Coq/Arith/Lt/le_lt_trans.con
-cic:/Coq/Arith/Lt/le_not_lt.con
-cic:/Coq/Arith/Lt/le_or_lt.con
-cic:/Coq/Arith/Lt/lt_asym.con
-cic:/Coq/Arith/Lt/lt_irrefl.con
-cic:/Coq/Arith/Lt/lt_le_S.con
-cic:/Coq/Arith/Lt/lt_le_trans.con
-cic:/Coq/Arith/Lt/lt_le_weak.con
-cic:/Coq/Arith/Lt/lt_n_O.con
-cic:/Coq/Arith/Lt/lt_not_le.con
-cic:/Coq/Arith/Lt/lt_n_S.con
-cic:/Coq/Arith/Lt/lt_n_Sm_le.con
-cic:/Coq/Arith/Lt/lt_n_Sn.con
-cic:/Coq/Arith/Lt/lt_O_neq.con
-cic:/Coq/Arith/Lt/lt_O_Sn.con
-cic:/Coq/Arith/Lt/lt_pred.con
-cic:/Coq/Arith/Lt/lt_pred_n_n.con
-cic:/Coq/Arith/Lt/lt_S.con
-cic:/Coq/Arith/Lt/lt_S_n.con
-cic:/Coq/Arith/Lt/lt_trans.con
-cic:/Coq/Arith/Lt/nat_total_order.con
-cic:/Coq/Arith/Lt/neq_O_lt.con
-cic:/Coq/Arith/Lt/S_pred.con
-cic:/Coq/Arith/Max/le_max_l.con
-cic:/Coq/Arith/Max/le_max_r.con
-cic:/Coq/Arith/Max/max_case2.con
-cic:/Coq/Arith/Max/max_case.con
-cic:/Coq/Arith/Max/max_comm.con
-cic:/Coq/Arith/Max/max.con
-cic:/Coq/Arith/Max/max_dec.con
-cic:/Coq/Arith/Max/max_l.con
-cic:/Coq/Arith/Max/max_r.con
-cic:/Coq/Arith/Max/max_SS.con
-cic:/Coq/Arith/Min/le_min_l.con
-cic:/Coq/Arith/Min/le_min_r.con
-cic:/Coq/Arith/Min/min_case2.con
-cic:/Coq/Arith/Min/min_case.con
-cic:/Coq/Arith/Min/min_comm.con
-cic:/Coq/Arith/Min/min.con
-cic:/Coq/Arith/Min/min_dec.con
-cic:/Coq/Arith/Min/min_l.con
-cic:/Coq/Arith/Min/min_r.con
-cic:/Coq/Arith/Min/min_SS.con
-cic:/Coq/Arith/Minus/le_minus.con
-cic:/Coq/Arith/Minus/le_plus_minus.con
-cic:/Coq/Arith/Minus/le_plus_minus_r.con
-cic:/Coq/Arith/Minus/lt_minus.con
-cic:/Coq/Arith/Minus/lt_O_minus_lt.con
-cic:/Coq/Arith/Minus/minus_n_n.con
-cic:/Coq/Arith/Minus/minus_n_O.con
-cic:/Coq/Arith/Minus/minus_plus.con
-cic:/Coq/Arith/Minus/minus_plus_simpl_l_reverse.con
-cic:/Coq/Arith/Minus/minus_Sn_m.con
-cic:/Coq/Arith/Minus/not_le_minus_0.con
-cic:/Coq/Arith/Minus/plus_minus.con
-cic:/Coq/Arith/Minus/pred_of_minus.con
-cic:/Coq/Arith/Mult/mult_0_l.con
-cic:/Coq/Arith/Mult/mult_0_r.con
-cic:/Coq/Arith/Mult/mult_1_l.con
-cic:/Coq/Arith/Mult/mult_1_r.con
-cic:/Coq/Arith/Mult/mult_acc_aux.con
-cic:/Coq/Arith/Mult/mult_acc.con
-cic:/Coq/Arith/Mult/mult_assoc.con
-cic:/Coq/Arith/Mult/mult_assoc_reverse.con
-cic:/Coq/Arith/Mult/mult_comm.con
-cic:/Coq/Arith/Mult/mult_le_compat.con
-cic:/Coq/Arith/Mult/mult_le_compat_l.con
-cic:/Coq/Arith/Mult/mult_le_compat_r.con
-cic:/Coq/Arith/Mult/mult_lt_compat_r.con
-cic:/Coq/Arith/Mult/mult_minus_distr_r.con
-cic:/Coq/Arith/Mult/mult_O_le.con
-cic:/Coq/Arith/Mult/mult_plus_distr_l.con
-cic:/Coq/Arith/Mult/mult_plus_distr_r.con
-cic:/Coq/Arith/Mult/mult_S_le_reg_l.con
-cic:/Coq/Arith/Mult/mult_S_lt_compat_l.con
-cic:/Coq/Arith/Mult/mult_tail_mult.con
-cic:/Coq/Arith/Mult/odd_even_lem.con
-cic:/Coq/Arith/Mult/tail_mult.con
-cic:/Coq/Arith/Peano_dec/dec_eq_nat.con
-cic:/Coq/Arith/Peano_dec/eq_nat_dec.con
-cic:/Coq/Arith/Peano_dec/O_or_S.con
-cic:/Coq/Arith/Plus/le_plus_l.con
-cic:/Coq/Arith/Plus/le_plus_r.con
-cic:/Coq/Arith/Plus/le_plus_trans.con
-cic:/Coq/Arith/Plus/lt_plus_trans.con
-cic:/Coq/Arith/Plus/plus_0_l.con
-cic:/Coq/Arith/Plus/plus_0_r.con
-cic:/Coq/Arith/Plus/plus_acc.con
-cic:/Coq/Arith/Plus/plus_assoc.con
-cic:/Coq/Arith/Plus/plus_assoc_reverse.con
-cic:/Coq/Arith/Plus/plus_comm.con
-cic:/Coq/Arith/Plus/plus_is_O.con
-cic:/Coq/Arith/Plus/plus_is_one.con
-cic:/Coq/Arith/Plus/plus_le_compat.con
-cic:/Coq/Arith/Plus/plus_le_compat_l.con
-cic:/Coq/Arith/Plus/plus_le_compat_r.con
-cic:/Coq/Arith/Plus/plus_le_lt_compat.con
-cic:/Coq/Arith/Plus/plus_le_reg_l.con
-cic:/Coq/Arith/Plus/plus_lt_compat.con
-cic:/Coq/Arith/Plus/plus_lt_compat_l.con
-cic:/Coq/Arith/Plus/plus_lt_compat_r.con
-cic:/Coq/Arith/Plus/plus_lt_le_compat.con
-cic:/Coq/Arith/Plus/plus_lt_reg_l.con
-cic:/Coq/Arith/Plus/plus_permute_2_in_4.con
-cic:/Coq/Arith/Plus/plus_permute.con
-cic:/Coq/Arith/Plus/plus_reg_l.con
-cic:/Coq/Arith/Plus/plus_Snm_nSm.con
-cic:/Coq/Arith/Plus/plus_tail_plus.con
-cic:/Coq/Arith/Plus/tail_plus.con
-cic:/Coq/Arith/Wf_nat/acc_lt_rel.con
-cic:/Coq/Arith/Wf_nat/gtof.con
-cic:/Coq/Arith/Wf_nat/gt_wf_ind.con
-cic:/Coq/Arith/Wf_nat/gt_wf_rec.con
-cic:/Coq/Arith/Wf_nat/induction_gtof1.con
-cic:/Coq/Arith/Wf_nat/induction_gtof2.con
-cic:/Coq/Arith/Wf_nat/induction_ltof1.con
-cic:/Coq/Arith/Wf_nat/induction_ltof2.con
-cic:/Coq/Arith/Wf_nat/inv_lt_rel.con
-cic:/Coq/Arith/Wf_nat/ltof.con
-cic:/Coq/Arith/Wf_nat/lt_wf.con
-cic:/Coq/Arith/Wf_nat/lt_wf_double_ind.con
-cic:/Coq/Arith/Wf_nat/lt_wf_double_rec.con
-cic:/Coq/Arith/Wf_nat/lt_wf_ind.con
-cic:/Coq/Arith/Wf_nat/lt_wf_rec1.con
-cic:/Coq/Arith/Wf_nat/lt_wf_rec.con
-cic:/Coq/Arith/Wf_nat/well_founded_gtof.con
-cic:/Coq/Arith/Wf_nat/well_founded_inv_lt_rel_compat.con
-cic:/Coq/Arith/Wf_nat/well_founded_inv_rel_inv_lt_rel.con
-cic:/Coq/Arith/Wf_nat/well_founded_lt_compat.con
-cic:/Coq/Arith/Wf_nat/well_founded_ltof.con
-cic:/Coq/Bool/Bool/absoption_andb.con
-cic:/Coq/Bool/Bool/absoption_orb.con
-cic:/Coq/Bool/Bool/andb_assoc.con
-cic:/Coq/Bool/Bool/andb_b_false.con
-cic:/Coq/Bool/Bool/andb_b_true.con
-cic:/Coq/Bool/Bool/andb_comm.con
-cic:/Coq/Bool/Bool/andb.con
-cic:/Coq/Bool/Bool/andb_false_b.con
-cic:/Coq/Bool/Bool/andb_false_elim.con
-cic:/Coq/Bool/Bool/andb_false_intro1.con
-cic:/Coq/Bool/Bool/andb_false_intro2.con
-cic:/Coq/Bool/Bool/andb_neg_b.con
-cic:/Coq/Bool/Bool/andb_prop2.con
-cic:/Coq/Bool/Bool/andb_prop.con
-cic:/Coq/Bool/Bool/andb_true_b.con
-cic:/Coq/Bool/Bool/andb_true_eq.con
-cic:/Coq/Bool/Bool/andb_true_intro2.con
-cic:/Coq/Bool/Bool/andb_true_intro.con
-cic:/Coq/Bool/Bool/bool_1.con
-cic:/Coq/Bool/Bool/bool_2.con
-cic:/Coq/Bool/Bool/bool_3.con
-cic:/Coq/Bool/Bool/bool_4.con
-cic:/Coq/Bool/Bool/bool_5.con
-cic:/Coq/Bool/Bool/bool_6.con
-cic:/Coq/Bool/Bool/demorgan1.con
-cic:/Coq/Bool/Bool/demorgan2.con
-cic:/Coq/Bool/Bool/demorgan3.con
-cic:/Coq/Bool/Bool/demorgan4.con
-cic:/Coq/Bool/Bool/diff_false_true.con
-cic:/Coq/Bool/Bool/diff_true_false.con
-cic:/Coq/Bool/Bool/eqb.con
-cic:/Coq/Bool/Bool/eqb_eq.con
-cic:/Coq/Bool/BoolEq/beq_eq_not_false.con
-cic:/Coq/Bool/BoolEq/beq_eq_true.con
-cic:/Coq/Bool/BoolEq/beq_false_not_eq.con
-cic:/Coq/Bool/Bool/eqb_negb1.con
-cic:/Coq/Bool/Bool/eqb_negb2.con
-cic:/Coq/Bool/Bool/eqb_prop.con
-cic:/Coq/Bool/Bool/eqb_refl.con
-cic:/Coq/Bool/Bool/eqb_reflx.con
-cic:/Coq/Bool/Bool/eqb_subst.con
-cic:/Coq/Bool/BoolEq/eq_dec.con
-cic:/Coq/Bool/BoolEq/exists_beq_eq.con
-cic:/Coq/Bool/BoolEq/not_eq_false_beq.con
-cic:/Coq/Bool/Bool/eq_true_false_abs.con
-cic:/Coq/Bool/Bool/false_xorb.con
-cic:/Coq/Bool/Bool/ifb.con
-cic:/Coq/Bool/Bool/if_negb.con
-cic:/Coq/Bool/Bool/implb.con
-cic:/Coq/Bool/Bool/Is_true.con
-cic:/Coq/Bool/Bool/Is_true_eq_left.con
-cic:/Coq/Bool/Bool/Is_true_eq_right.con
-cic:/Coq/Bool/Bool/Is_true_eq_true2.con
-cic:/Coq/Bool/Bool/Is_true_eq_true.con
-cic:/Coq/Bool/Bool/leb.con
-cic:/Coq/Bool/Bool/negb_andb.con
-cic:/Coq/Bool/Bool/negb.con
-cic:/Coq/Bool/Bool/negb_elim.con
-cic:/Coq/Bool/Bool/negb_intro.con
-cic:/Coq/Bool/Bool/negb_orb.con
-cic:/Coq/Bool/Bool/negb_sym.con
-cic:/Coq/Bool/Bool/no_fixpoint_negb.con
-cic:/Coq/Bool/Bool/not_false_is_true.con
-cic:/Coq/Bool/Bool/not_true_is_false.con
-cic:/Coq/Bool/Bool/orb_assoc.con
-cic:/Coq/Bool/Bool/orb_b_false.con
-cic:/Coq/Bool/Bool/orb_b_true.con
-cic:/Coq/Bool/Bool/orb_comm.con
-cic:/Coq/Bool/Bool/orb.con
-cic:/Coq/Bool/Bool/orb_false_b.con
-cic:/Coq/Bool/Bool/orb_false_elim.con
-cic:/Coq/Bool/Bool/orb_false_intro.con
-cic:/Coq/Bool/Bool/orb_neg_b.con
-cic:/Coq/Bool/Bool/orb_prop2.con
-cic:/Coq/Bool/Bool/orb_prop.con
-cic:/Coq/Bool/Bool/orb_true_b.con
-cic:/Coq/Bool/Bool/orb_true_elim.con
-cic:/Coq/Bool/Bool/orb_true_intro.con
-cic:/Coq/Bool/Bool/true_xorb.con
-cic:/Coq/Bool/Bool/xorb_assoc.con
-cic:/Coq/Bool/Bool/xorb_comm.con
-cic:/Coq/Bool/Bool/xorb.con
-cic:/Coq/Bool/Bool/xorb_eq.con
-cic:/Coq/Bool/Bool/xorb_false.con
-cic:/Coq/Bool/Bool/xorb_move_l_r_1.con
-cic:/Coq/Bool/Bool/xorb_move_l_r_2.con
-cic:/Coq/Bool/Bool/xorb_move_r_l_1.con
-cic:/Coq/Bool/Bool/xorb_move_r_l_2.con
-cic:/Coq/Bool/Bool/xorb_nilpotent.con
-cic:/Coq/Bool/Bool/xorb_true.con
-cic:/Coq/Bool/Bvector/Bcons.con
-cic:/Coq/Bool/Bvector/Bhigh.con
-cic:/Coq/Bool/Bvector/Blow.con
-cic:/Coq/Bool/Bvector/Bneg.con
-cic:/Coq/Bool/Bvector/Bnil.con
-cic:/Coq/Bool/Bvector/BshiftL.con
-cic:/Coq/Bool/Bvector/BshiftL_iter.con
-cic:/Coq/Bool/Bvector/BshiftRa.con
-cic:/Coq/Bool/Bvector/BshiftRa_iter.con
-cic:/Coq/Bool/Bvector/BshiftRl.con
-cic:/Coq/Bool/Bvector/BshiftRl_iter.con
-cic:/Coq/Bool/Bvector/Bsign.con
-cic:/Coq/Bool/Bvector/BVand.con
-cic:/Coq/Bool/Bvector/Bvect_false.con
-cic:/Coq/Bool/Bvector/Bvector.con
-cic:/Coq/Bool/Bvector/Bvect_true.con
-cic:/Coq/Bool/Bvector/BVor.con
-cic:/Coq/Bool/Bvector/BVxor.con
-cic:/Coq/Bool/Bvector/Vbinary.con
-cic:/Coq/Bool/Bvector/Vconst.con
-cic:/Coq/Bool/Bvector/vector.ind
-cic:/Coq/Bool/Bvector/vector_ind.con
-cic:/Coq/Bool/Bvector/vector_rec.con
-cic:/Coq/Bool/Bvector/vector_rect.con
-cic:/Coq/Bool/Bvector/Vextend.con
-cic:/Coq/Bool/Bvector/Vhead.con
-cic:/Coq/Bool/Bvector/Vlast.con
-cic:/Coq/Bool/Bvector/Vshiftin.con
-cic:/Coq/Bool/Bvector/Vshiftout.con
-cic:/Coq/Bool/Bvector/Vshiftrepeat.con
-cic:/Coq/Bool/Bvector/Vtail.con
-cic:/Coq/Bool/Bvector/Vtrunc.con
-cic:/Coq/Bool/Bvector/Vunary.con
-cic:/Coq/Bool/DecBool/ifdec.con
-cic:/Coq/Bool/DecBool/ifdec_left.con
-cic:/Coq/Bool/DecBool/ifdec_right.con
-cic:/Coq/Bool/IfProp/Iffalse_inv.con
-cic:/Coq/Bool/IfProp/IfProp_false.con
-cic:/Coq/Bool/IfProp/IfProp.ind
-cic:/Coq/Bool/IfProp/IfProp_ind.con
-cic:/Coq/Bool/IfProp/IfProp_or.con
-cic:/Coq/Bool/IfProp/IfProp_sum.con
-cic:/Coq/Bool/IfProp/IfProp_true.con
-cic:/Coq/Bool/IfProp/Iftrue_inv.con
-cic:/Coq/Bool/Sumbool/bool_eq_ind.con
-cic:/Coq/Bool/Sumbool/bool_eq_rec.con
-cic:/Coq/Bool/Sumbool/bool_of_sumbool.con
-cic:/Coq/Bool/Sumbool/sumbool_and.con
-cic:/Coq/Bool/Sumbool/sumbool_not.con
-cic:/Coq/Bool/Sumbool/sumbool_of_bool.con
-cic:/Coq/Bool/Sumbool/sumbool_or.con
-cic:/Coq/Bool/Zerob/zerob.con
-cic:/Coq/Bool/Zerob/zerob_false_elim.con
-cic:/Coq/Bool/Zerob/zerob_false_intro.con
-cic:/Coq/Bool/Zerob/zerob_true_elim.con
-cic:/Coq/Bool/Zerob/zerob_true_intro.con
-cic:/Coq/field/Field_Compl/appT.con
-cic:/Coq/field/Field_Compl/assoc_2nd.con
-cic:/Coq/field/Field_Compl/field_rel_option.ind
-cic:/Coq/field/Field_Compl/field_rel_option_ind.con
-cic:/Coq/field/Field_Compl/field_rel_option_rec.con
-cic:/Coq/field/Field_Compl/field_rel_option_rect.con
-cic:/Coq/field/Field_Compl/fstT.con
-cic:/Coq/field/Field_Compl/listT.ind
-cic:/Coq/field/Field_Compl/listT_ind.con
-cic:/Coq/field/Field_Compl/listT_rec.con
-cic:/Coq/field/Field_Compl/listT_rect.con
-cic:/Coq/field/Field_Compl/mem.con
-cic:/Coq/field/Field_Compl/prodT.ind
-cic:/Coq/field/Field_Compl/prodT_ind.con
-cic:/Coq/field/Field_Compl/prodT_rec.con
-cic:/Coq/field/Field_Compl/prodT_rect.con
-cic:/Coq/field/Field_Compl/sndT.con
-cic:/Coq/field/Field_Theory/A.con
-cic:/Coq/field/Field_Theory/Adiv.con
-cic:/Coq/field/Field_Theory/Aeq.con
-cic:/Coq/field/Field_Theory/Ainv.con
-cic:/Coq/field/Field_Theory/AinvT_r.con
-cic:/Coq/field/Field_Theory/Aminus.con
-cic:/Coq/field/Field_Theory/Amult.con
-cic:/Coq/field/Field_Theory/AmultT_1l.con
-cic:/Coq/field/Field_Theory/AmultT_1r.con
-cic:/Coq/field/Field_Theory/AmultT_AplusT_distr.con
-cic:/Coq/field/Field_Theory/AmultT_assoc.con
-cic:/Coq/field/Field_Theory/AmultT_Ol.con
-cic:/Coq/field/Field_Theory/AmultT_Or.con
-cic:/Coq/field/Field_Theory/AmultT_sym.con
-cic:/Coq/field/Field_Theory/Aone.con
-cic:/Coq/field/Field_Theory/Aopp.con
-cic:/Coq/field/Field_Theory/Aplus.con
-cic:/Coq/field/Field_Theory/AplusT_AoppT_r.con
-cic:/Coq/field/Field_Theory/AplusT_assoc.con
-cic:/Coq/field/Field_Theory/AplusT_Ol.con
-cic:/Coq/field/Field_Theory/AplusT_sym.con
-cic:/Coq/field/Field_Theory/assoc.con
-cic:/Coq/field/Field_Theory/assoc_correct.con
-cic:/Coq/field/Field_Theory/assoc_mult.con
-cic:/Coq/field/Field_Theory/assoc_mult_correct1.con
-cic:/Coq/field/Field_Theory/assoc_mult_correct.con
-cic:/Coq/field/Field_Theory/assoc_plus_correct.con
-cic:/Coq/field/Field_Theory/Azero.con
-cic:/Coq/field/Field_Theory/distrib.con
-cic:/Coq/field/Field_Theory/distrib_correct.con
-cic:/Coq/field/Field_Theory/distrib_EAopp.con
-cic:/Coq/field/Field_Theory/distrib_main.con
-cic:/Coq/field/Field_Theory/distrib_mult_left.con
-cic:/Coq/field/Field_Theory/distrib_mult_left_correct.con
-cic:/Coq/field/Field_Theory/distrib_mult_right.con
-cic:/Coq/field/Field_Theory/distrib_mult_right_correct.con
-cic:/Coq/field/Field_Theory/eqExprA.con
-cic:/Coq/field/Field_Theory/eqExprA_O.con
-cic:/Coq/field/Field_Theory/eq_nat_dec.con
-cic:/Coq/field/Field_Theory/ExprA.ind
-cic:/Coq/field/Field_Theory/ExprA_ind.con
-cic:/Coq/field/Field_Theory/ExprA_rec.con
-cic:/Coq/field/Field_Theory/ExprA_rect.con
-cic:/Coq/field/Field_Theory/Field_Theory.ind
-cic:/Coq/field/Field_Theory/Field_Theory_ind.con
-cic:/Coq/field/Field_Theory/Field_Theory_rec.con
-cic:/Coq/field/Field_Theory/Field_Theory_rect.con
-cic:/Coq/field/Field_Theory/interp_ExprA.con
-cic:/Coq/field/Field_Theory/inverse_correct.con
-cic:/Coq/field/Field_Theory/inverse_simplif.con
-cic:/Coq/field/Field_Theory/merge_mult.con
-cic:/Coq/field/Field_Theory/merge_mult_correct1.con
-cic:/Coq/field/Field_Theory/merge_mult_correct.con
-cic:/Coq/field/Field_Theory/merge_plus.con
-cic:/Coq/field/Field_Theory/merge_plus_correct1.con
-cic:/Coq/field/Field_Theory/merge_plus_correct.con
-cic:/Coq/field/Field_Theory/monom_remove.con
-cic:/Coq/field/Field_Theory/monom_remove_correct.con
-cic:/Coq/field/Field_Theory/monom_simplif.con
-cic:/Coq/field/Field_Theory/monom_simplif_correct.con
-cic:/Coq/field/Field_Theory/monom_simplif_rem.con
-cic:/Coq/field/Field_Theory/monom_simplif_rem_correct.con
-cic:/Coq/field/Field_Theory/mult_eq.con
-cic:/Coq/field/Field_Theory/multiply_aux.con
-cic:/Coq/field/Field_Theory/multiply_aux_correct.con
-cic:/Coq/field/Field_Theory/multiply.con
-cic:/Coq/field/Field_Theory/multiply_correct.con
-cic:/Coq/field/Field_Theory/mult_of_list.con
-cic:/Coq/field/Field_Theory/r_AmultT_mult.con
-cic:/Coq/field/Field_Theory/r_AplusT_plus.con
-cic:/Coq/field/Field_Theory/Rmult_neq_0_reg.con
-cic:/Coq/field/Field_Theory/RT.con
-cic:/Coq/field/Field_Theory/Th_inv_def.con
-cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con
-cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con
-cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con
-cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con
-cic:/Coq/fourier/Fourier_util/Rfourier_le.con
-cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con
-cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con
-cic:/Coq/fourier/Fourier_util/Rfourier_lt.con
-cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con
-cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con
-cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con
-cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con
-cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con
-cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con
-cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con
-cic:/Coq/fourier/Fourier_util/Rle_not_lt.con
-cic:/Coq/fourier/Fourier_util/Rle_zero_1.con
-cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con
-cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con
-cic:/Coq/fourier/Fourier_util/Rlt_not_le.con
-cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con
-cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con
-cic:/Coq/fourier/Fourier_util/Rnot_le_le.con
-cic:/Coq/fourier/Fourier_util/Rnot_lt0.con
-cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con
-cic:/Coq/Init/Datatypes/bool.ind
-cic:/Coq/Init/Datatypes/bool_ind.con
-cic:/Coq/Init/Datatypes/bool_rec.con
-cic:/Coq/Init/Datatypes/bool_rect.con
-cic:/Coq/Init/Datatypes/comparison.ind
-cic:/Coq/Init/Datatypes/comparison_ind.con
-cic:/Coq/Init/Datatypes/comparison_rec.con
-cic:/Coq/Init/Datatypes/comparison_rect.con
-cic:/Coq/Init/Datatypes/CompOpp.con
-cic:/Coq/Init/Datatypes/Empty_set.ind
-cic:/Coq/Init/Datatypes/Empty_set_ind.con
-cic:/Coq/Init/Datatypes/Empty_set_rec.con
-cic:/Coq/Init/Datatypes/Empty_set_rect.con
-cic:/Coq/Init/Datatypes/fst.con
-cic:/Coq/Init/Datatypes/identity.ind
-cic:/Coq/Init/Datatypes/identity_ind.con
-cic:/Coq/Init/Datatypes/identity_rec.con
-cic:/Coq/Init/Datatypes/identity_rect.con
-cic:/Coq/Init/Datatypes/injective_projections.con
-cic:/Coq/Init/Datatypes/nat.ind
-cic:/Coq/Init/Datatypes/nat_ind.con
-cic:/Coq/Init/Datatypes/nat_rec.con
-cic:/Coq/Init/Datatypes/nat_rect.con
-cic:/Coq/Init/Datatypes/option.ind
-cic:/Coq/Init/Datatypes/option_ind.con
-cic:/Coq/Init/Datatypes/option_rec.con
-cic:/Coq/Init/Datatypes/option_rect.con
-cic:/Coq/Init/Datatypes/prod.ind
-cic:/Coq/Init/Datatypes/prod_ind.con
-cic:/Coq/Init/Datatypes/prod_rec.con
-cic:/Coq/Init/Datatypes/prod_rect.con
-cic:/Coq/Init/Datatypes/snd.con
-cic:/Coq/Init/Datatypes/sum.ind
-cic:/Coq/Init/Datatypes/sum_ind.con
-cic:/Coq/Init/Datatypes/sum_rec.con
-cic:/Coq/Init/Datatypes/sum_rect.con
-cic:/Coq/Init/Datatypes/surjective_pairing.con
-cic:/Coq/Init/Datatypes/unit.ind
-cic:/Coq/Init/Datatypes/unit_ind.con
-cic:/Coq/Init/Datatypes/unit_rec.con
-cic:/Coq/Init/Datatypes/unit_rect.con
-cic:/Coq/Init/Logic/absurd.con
-cic:/Coq/Init/Logic/all.con
-cic:/Coq/Init/Logic/and.ind
-cic:/Coq/Init/Logic/and_ind.con
-cic:/Coq/Init/Logic/and_rec.con
-cic:/Coq/Init/Logic/and_rect.con
-cic:/Coq/Init/Logic/eq.ind
-cic:/Coq/Init/Logic/eq_ind.con
-cic:/Coq/Init/Logic/eq_ind_r.con
-cic:/Coq/Init/Logic/eq_rec.con
-cic:/Coq/Init/Logic/eq_rec_r.con
-cic:/Coq/Init/Logic/eq_rect.con
-cic:/Coq/Init/Logic/eq_rect_r.con
-cic:/Coq/Init/Logic/ex2.ind
-cic:/Coq/Init/Logic/ex2_ind.con
-cic:/Coq/Init/Logic/ex.ind
-cic:/Coq/Init/Logic/ex_ind.con
-cic:/Coq/Init/Logic/False.ind
-cic:/Coq/Init/Logic/False_ind.con
-cic:/Coq/Init/Logic/False_rec.con
-cic:/Coq/Init/Logic/False_rect.con
-cic:/Coq/Init/Logic/f_equal2.con
-cic:/Coq/Init/Logic/f_equal3.con
-cic:/Coq/Init/Logic/f_equal4.con
-cic:/Coq/Init/Logic/f_equal5.con
-cic:/Coq/Init/Logic/f_equal.con
-cic:/Coq/Init/Logic/gen.con
-cic:/Coq/Init/Logic/iff.con
-cic:/Coq/Init/Logic/iff_refl.con
-cic:/Coq/Init/Logic/iff_sym.con
-cic:/Coq/Init/Logic/iff_trans.con
-cic:/Coq/Init/Logic/IF_then_else.con
-cic:/Coq/Init/Logic/inst.con
-cic:/Coq/Init/Logic/not.con
-cic:/Coq/Init/Logic/or.ind
-cic:/Coq/Init/Logic/or_ind.con
-cic:/Coq/Init/Logic/proj1.con
-cic:/Coq/Init/Logic/proj2.con
-cic:/Coq/Init/Logic/sym_eq.con
-cic:/Coq/Init/Logic/sym_equal.con
-cic:/Coq/Init/Logic/sym_not_eq.con
-cic:/Coq/Init/Logic/sym_not_equal.con
-cic:/Coq/Init/Logic/trans_eq.con
-cic:/Coq/Init/Logic/trans_equal.con
-cic:/Coq/Init/Logic/True.ind
-cic:/Coq/Init/Logic/True_ind.con
-cic:/Coq/Init/Logic/True_rec.con
-cic:/Coq/Init/Logic/True_rect.con
-cic:/Coq/Init/Logic_Type/congr_id.con
-cic:/Coq/Init/Logic_Type/fstT.con
-cic:/Coq/Init/Logic_Type/identity_ind_r.con
-cic:/Coq/Init/Logic_Type/identity_rec_r.con
-cic:/Coq/Init/Logic_Type/identity_rect_r.con
-cic:/Coq/Init/Logic_Type/notT.con
-cic:/Coq/Init/Logic_Type/prodT_curry.con
-cic:/Coq/Init/Logic_Type/prodT.ind
-cic:/Coq/Init/Logic_Type/prodT_ind.con
-cic:/Coq/Init/Logic_Type/prodT_rec.con
-cic:/Coq/Init/Logic_Type/prodT_rect.con
-cic:/Coq/Init/Logic_Type/prodT_uncurry.con
-cic:/Coq/Init/Logic_Type/sndT.con
-cic:/Coq/Init/Logic_Type/sym_id.con
-cic:/Coq/Init/Logic_Type/sym_not_id.con
-cic:/Coq/Init/Logic_Type/trans_id.con
-cic:/Coq/Init/Peano/eq_add_S.con
-cic:/Coq/Init/Peano/eq_S.con
-cic:/Coq/Init/Peano/ge.con
-cic:/Coq/Init/Peano/gt.con
-cic:/Coq/Init/Peano/IsSucc.con
-cic:/Coq/Init/Peano/le.ind
-cic:/Coq/Init/Peano/le_ind.con
-cic:/Coq/Init/Peano/lt.con
-cic:/Coq/Init/Peano/minus.con
-cic:/Coq/Init/Peano/mult.con
-cic:/Coq/Init/Peano/mult_n_O.con
-cic:/Coq/Init/Peano/mult_n_Sm.con
-cic:/Coq/Init/Peano/nat_case.con
-cic:/Coq/Init/Peano/nat_double_ind.con
-cic:/Coq/Init/Peano/not_eq_S.con
-cic:/Coq/Init/Peano/n_Sn.con
-cic:/Coq/Init/Peano/O_S.con
-cic:/Coq/Init/Peano/plus.con
-cic:/Coq/Init/Peano/plus_n_O.con
-cic:/Coq/Init/Peano/plus_n_Sm.con
-cic:/Coq/Init/Peano/plus_O_n.con
-cic:/Coq/Init/Peano/plus_Sn_m.con
-cic:/Coq/Init/Peano/pred.con
-cic:/Coq/Init/Peano/pred_Sn.con
-cic:/Coq/Init/Specif/absurd_set.con
-cic:/Coq/Init/Specif/bool_choice.con
-cic:/Coq/Init/Specif/Choice2.con
-cic:/Coq/Init/Specif/Choice.con
-cic:/Coq/Init/Specif/error.con
-cic:/Coq/Init/Specif/Exc.con
-cic:/Coq/Init/Specif/except.con
-cic:/Coq/Init/Specif/proj1_sig.con
-cic:/Coq/Init/Specif/proj2_sig.con
-cic:/Coq/Init/Specif/projS1.con
-cic:/Coq/Init/Specif/projS2.con
-cic:/Coq/Init/Specif/projT1.con
-cic:/Coq/Init/Specif/projT2.con
-cic:/Coq/Init/Specif/sig2.ind
-cic:/Coq/Init/Specif/sig2_ind.con
-cic:/Coq/Init/Specif/sig2_rec.con
-cic:/Coq/Init/Specif/sig2_rect.con
-cic:/Coq/Init/Specif/sig.ind
-cic:/Coq/Init/Specif/sig_ind.con
-cic:/Coq/Init/Specif/sig_rec.con
-cic:/Coq/Init/Specif/sig_rect.con
-cic:/Coq/Init/Specif/sigS2.ind
-cic:/Coq/Init/Specif/sigS2_ind.con
-cic:/Coq/Init/Specif/sigS2_rec.con
-cic:/Coq/Init/Specif/sigS2_rect.con
-cic:/Coq/Init/Specif/sigS.ind
-cic:/Coq/Init/Specif/sigS_ind.con
-cic:/Coq/Init/Specif/sigS_rec.con
-cic:/Coq/Init/Specif/sigS_rect.con
-cic:/Coq/Init/Specif/sigT.ind
-cic:/Coq/Init/Specif/sigT_ind.con
-cic:/Coq/Init/Specif/sigT_rec.con
-cic:/Coq/Init/Specif/sigT_rect.con
-cic:/Coq/Init/Specif/sumbool.ind
-cic:/Coq/Init/Specif/sumbool_ind.con
-cic:/Coq/Init/Specif/sumbool_rec.con
-cic:/Coq/Init/Specif/sumbool_rect.con
-cic:/Coq/Init/Specif/sumor.ind
-cic:/Coq/Init/Specif/sumor_ind.con
-cic:/Coq/Init/Specif/sumor_rec.con
-cic:/Coq/Init/Specif/sumor_rect.con
-cic:/Coq/Init/Specif/value.con
-cic:/Coq/Init/Wf/Acc.ind
-cic:/Coq/Init/Wf/Acc_ind.con
-cic:/Coq/Init/Wf/Acc_inv.con
-cic:/Coq/Init/Wf/Acc_inv_dep.con
-cic:/Coq/Init/Wf/Acc_iter_2.con
-cic:/Coq/Init/Wf/Acc_iter.con
-cic:/Coq/Init/Wf/Acc_rec.con
-cic:/Coq/Init/Wf/Acc_rect.con
-cic:/Coq/Init/Wf/Fix.con
-cic:/Coq/Init/Wf/Fix_eq.con
-cic:/Coq/Init/Wf/Fix_F.con
-cic:/Coq/Init/Wf/Fix_F_eq.con
-cic:/Coq/Init/Wf/Fix_F_inv.con
-cic:/Coq/Init/Wf/well_founded.con
-cic:/Coq/Init/Wf/well_founded_ind.con
-cic:/Coq/Init/Wf/well_founded_induction.con
-cic:/Coq/Init/Wf/well_founded_induction_type_2.con
-cic:/Coq/Init/Wf/well_founded_induction_type.con
-cic:/Coq/IntMap/Adalloc/ad_alloc_opt_allocates_1.con
-cic:/Coq/IntMap/Adalloc/ad_alloc_opt_allocates.con
-cic:/Coq/IntMap/Adalloc/ad_alloc_opt.con
-cic:/Coq/IntMap/Adalloc/ad_alloc_opt_optimal_1.con
-cic:/Coq/IntMap/Adalloc/ad_alloc_opt_optimal.con
-cic:/Coq/IntMap/Adalloc/ad_le_antisym.con
-cic:/Coq/IntMap/Adalloc/ad_le.con
-cic:/Coq/IntMap/Adalloc/ad_le_double_mono.con
-cic:/Coq/IntMap/Adalloc/ad_le_double_mono_conv.con
-cic:/Coq/IntMap/Adalloc/ad_le_double_plus_un_mono.con
-cic:/Coq/IntMap/Adalloc/ad_le_double_plus_un_mono_conv.con
-cic:/Coq/IntMap/Adalloc/ad_le_lt_trans.con
-cic:/Coq/IntMap/Adalloc/ad_le_refl.con
-cic:/Coq/IntMap/Adalloc/ad_le_trans.con
-cic:/Coq/IntMap/Adalloc/ad_lt_double_mono.con
-cic:/Coq/IntMap/Adalloc/ad_lt_double_mono_conv.con
-cic:/Coq/IntMap/Adalloc/ad_lt_double_plus_un_mono.con
-cic:/Coq/IntMap/Adalloc/ad_lt_double_plus_un_mono_conv.con
-cic:/Coq/IntMap/Adalloc/ad_lt_le_trans.con
-cic:/Coq/IntMap/Adalloc/ad_lt_le_weak.con
-cic:/Coq/IntMap/Adalloc/ad_lt_trans.con
-cic:/Coq/IntMap/Adalloc/ad_min_choice.con
-cic:/Coq/IntMap/Adalloc/ad_min.con
-cic:/Coq/IntMap/Adalloc/ad_min_le_1.con
-cic:/Coq/IntMap/Adalloc/ad_min_le_2.con
-cic:/Coq/IntMap/Adalloc/ad_min_le_3.con
-cic:/Coq/IntMap/Adalloc/ad_min_le_4.con
-cic:/Coq/IntMap/Adalloc/ad_min_le_5.con
-cic:/Coq/IntMap/Adalloc/ad_min_lt_3.con
-cic:/Coq/IntMap/Adalloc/ad_min_lt_4.con
-cic:/Coq/IntMap/Adalloc/ad_of_nat.con
-cic:/Coq/IntMap/Adalloc/ad_of_nat_of_ad.con
-cic:/Coq/IntMap/Adalloc/nat_le_complete.con
-cic:/Coq/IntMap/Adalloc/nat_le_complete_conv.con
-cic:/Coq/IntMap/Adalloc/nat_le.con
-cic:/Coq/IntMap/Adalloc/nat_le_correct.con
-cic:/Coq/IntMap/Adalloc/nat_le_correct_conv.con
-cic:/Coq/IntMap/Adalloc/nat_of_ad.con
-cic:/Coq/IntMap/Adalloc/nat_of_ad_double.con
-cic:/Coq/IntMap/Adalloc/nat_of_ad_double_plus_un.con
-cic:/Coq/IntMap/Adalloc/nat_of_ad_of_nat.con
-cic:/Coq/IntMap/Addec/ad_bit_0_0_not_double_plus_un.con
-cic:/Coq/IntMap/Addec/ad_bit_0_1_not_double.con
-cic:/Coq/IntMap/Addec/ad_bit_0_neq.con
-cic:/Coq/IntMap/Addec/ad_div_bit_eq.con
-cic:/Coq/IntMap/Addec/ad_div_bit_neq.con
-cic:/Coq/IntMap/Addec/ad_div_eq.con
-cic:/Coq/IntMap/Addec/ad_div_neq.con
-cic:/Coq/IntMap/Addec/ad_double_or_double_plus_un.con
-cic:/Coq/IntMap/Addec/ad_eq_1.con
-cic:/Coq/IntMap/Addec/ad_eq_comm.con
-cic:/Coq/IntMap/Addec/ad_eq_complete.con
-cic:/Coq/IntMap/Addec/ad_eq.con
-cic:/Coq/IntMap/Addec/ad_eq_correct.con
-cic:/Coq/IntMap/Addec/ad_neq.con
-cic:/Coq/IntMap/Addec/ad_not_div_2_not_double.con
-cic:/Coq/IntMap/Addec/ad_not_div_2_not_double_plus_un.con
-cic:/Coq/IntMap/Addec/ad_xor_eq_false.con
-cic:/Coq/IntMap/Addec/ad_xor_eq_true.con
-cic:/Coq/IntMap/Addr/ad_bit_0.con
-cic:/Coq/IntMap/Addr/ad_bit_0_correct.con
-cic:/Coq/IntMap/Addr/ad_bit_1.con
-cic:/Coq/IntMap/Addr/ad_bit.con
-cic:/Coq/IntMap/Addr/ad_div_2.con
-cic:/Coq/IntMap/Addr/ad_div_2_correct.con
-cic:/Coq/IntMap/Addr/ad_div_2_double.con
-cic:/Coq/IntMap/Addr/ad_div_2_double_plus_un.con
-cic:/Coq/IntMap/Addr/ad_double_bit_0.con
-cic:/Coq/IntMap/Addr/ad_double.con
-cic:/Coq/IntMap/Addr/ad_double_div_2.con
-cic:/Coq/IntMap/Addr/ad_double_inj.con
-cic:/Coq/IntMap/Addr/ad_double_plus_un_bit_0.con
-cic:/Coq/IntMap/Addr/ad_double_plus_un.con
-cic:/Coq/IntMap/Addr/ad_double_plus_un_div_2.con
-cic:/Coq/IntMap/Addr/ad_double_plus_un_inj.con
-cic:/Coq/IntMap/Addr/ad_faithful_1.con
-cic:/Coq/IntMap/Addr/ad_faithful_2.con
-cic:/Coq/IntMap/Addr/ad_faithful_3.con
-cic:/Coq/IntMap/Addr/ad_faithful_4.con
-cic:/Coq/IntMap/Addr/ad_faithful.con
-cic:/Coq/IntMap/Addr/adf_xor_assoc.con
-cic:/Coq/IntMap/Addr/adf_xor.con
-cic:/Coq/IntMap/Addr/adf_xor_eq.con
-cic:/Coq/IntMap/Addr/ad.ind
-cic:/Coq/IntMap/Addr/ad_ind.con
-cic:/Coq/IntMap/Addr/ad_neg_bit_0_1.con
-cic:/Coq/IntMap/Addr/ad_neg_bit_0_2.con
-cic:/Coq/IntMap/Addr/ad_neg_bit_0.con
-cic:/Coq/IntMap/Addr/ad_rec.con
-cic:/Coq/IntMap/Addr/ad_rect.con
-cic:/Coq/IntMap/Addr/ad_same_bit_0.con
-cic:/Coq/IntMap/Addr/ad_sum.con
-cic:/Coq/IntMap/Addr/ad_xor_assoc.con
-cic:/Coq/IntMap/Addr/ad_xor_bit_0.con
-cic:/Coq/IntMap/Addr/ad_xor_comm.con
-cic:/Coq/IntMap/Addr/ad_xor.con
-cic:/Coq/IntMap/Addr/ad_xor_div_2.con
-cic:/Coq/IntMap/Addr/ad_xor_eq.con
-cic:/Coq/IntMap/Addr/ad_xor_neutral_left.con
-cic:/Coq/IntMap/Addr/ad_xor_neutral_right.con
-cic:/Coq/IntMap/Addr/ad_xor_nilpotent.con
-cic:/Coq/IntMap/Addr/ad_xor_sem_1.con
-cic:/Coq/IntMap/Addr/ad_xor_sem_2.con
-cic:/Coq/IntMap/Addr/ad_xor_sem_3.con
-cic:/Coq/IntMap/Addr/ad_xor_sem_4.con
-cic:/Coq/IntMap/Addr/ad_xor_sem_5.con
-cic:/Coq/IntMap/Addr/ad_xor_sem_6.con
-cic:/Coq/IntMap/Addr/ad_xor_semantics.con
-cic:/Coq/IntMap/Addr/eqf.con
-cic:/Coq/IntMap/Addr/eqf_refl.con
-cic:/Coq/IntMap/Addr/eqf_sym.con
-cic:/Coq/IntMap/Addr/eqf_trans.con
-cic:/Coq/IntMap/Addr/eqf_xor_1.con
-cic:/Coq/IntMap/Addr/p_xor.con
-cic:/Coq/IntMap/Adist/ad_pdist_comm.con
-cic:/Coq/IntMap/Adist/ad_pdist.con
-cic:/Coq/IntMap/Adist/ad_pdist_eq_1.con
-cic:/Coq/IntMap/Adist/ad_pdist_eq_2.con
-cic:/Coq/IntMap/Adist/ad_pdist_ultra.con
-cic:/Coq/IntMap/Adist/ad_plength_1.con
-cic:/Coq/IntMap/Adist/ad_plength.con
-cic:/Coq/IntMap/Adist/ad_plength_first_one.con
-cic:/Coq/IntMap/Adist/ad_plength_infty.con
-cic:/Coq/IntMap/Adist/ad_plength_lb.con
-cic:/Coq/IntMap/Adist/ad_plength_one.con
-cic:/Coq/IntMap/Adist/ad_plength_ub.con
-cic:/Coq/IntMap/Adist/ad_plength_ultra_1.con
-cic:/Coq/IntMap/Adist/ad_plength_ultra.con
-cic:/Coq/IntMap/Adist/ad_plength_zeros.con
-cic:/Coq/IntMap/Adist/le_ni_le.con
-cic:/Coq/IntMap/Adist/natinf.ind
-cic:/Coq/IntMap/Adist/natinf_ind.con
-cic:/Coq/IntMap/Adist/natinf_rec.con
-cic:/Coq/IntMap/Adist/natinf_rect.con
-cic:/Coq/IntMap/Adist/ni_le_antisym.con
-cic:/Coq/IntMap/Adist/ni_le.con
-cic:/Coq/IntMap/Adist/ni_le_le.con
-cic:/Coq/IntMap/Adist/ni_le_min_1.con
-cic:/Coq/IntMap/Adist/ni_le_min_2.con
-cic:/Coq/IntMap/Adist/ni_le_min_induc.con
-cic:/Coq/IntMap/Adist/ni_le_refl.con
-cic:/Coq/IntMap/Adist/ni_le_total.con
-cic:/Coq/IntMap/Adist/ni_le_trans.con
-cic:/Coq/IntMap/Adist/ni_min_assoc.con
-cic:/Coq/IntMap/Adist/ni_min_case.con
-cic:/Coq/IntMap/Adist/ni_min_comm.con
-cic:/Coq/IntMap/Adist/ni_min.con
-cic:/Coq/IntMap/Adist/ni_min_idemp.con
-cic:/Coq/IntMap/Adist/ni_min_inf_l.con
-cic:/Coq/IntMap/Adist/ni_min_inf_r.con
-cic:/Coq/IntMap/Adist/ni_min_O_l.con
-cic:/Coq/IntMap/Adist/ni_min_O_r.con
-cic:/Coq/IntMap/Fset/FSet.con
-cic:/Coq/IntMap/Fset/FSetDelta.con
-cic:/Coq/IntMap/Fset/FSetDiff.con
-cic:/Coq/IntMap/Fset/FSet_Dom.con
-cic:/Coq/IntMap/Fset/FSetInter.con
-cic:/Coq/IntMap/Fset/FSetUnion.con
-cic:/Coq/IntMap/Fset/in_dom.con
-cic:/Coq/IntMap/Fset/in_dom_delta.con
-cic:/Coq/IntMap/Fset/in_dom_M0.con
-cic:/Coq/IntMap/Fset/in_dom_M1_1.con
-cic:/Coq/IntMap/Fset/in_dom_M1_2.con
-cic:/Coq/IntMap/Fset/in_dom_M1.con
-cic:/Coq/IntMap/Fset/in_dom_merge.con
-cic:/Coq/IntMap/Fset/in_dom_none.con
-cic:/Coq/IntMap/Fset/in_dom_put_behind.con
-cic:/Coq/IntMap/Fset/in_dom_put.con
-cic:/Coq/IntMap/Fset/in_dom_remove.con
-cic:/Coq/IntMap/Fset/in_dom_restrby.con
-cic:/Coq/IntMap/Fset/in_dom_restrto.con
-cic:/Coq/IntMap/Fset/in_dom_some.con
-cic:/Coq/IntMap/Fset/in_FSet.con
-cic:/Coq/IntMap/Fset/in_FSet_delta.con
-cic:/Coq/IntMap/Fset/in_FSet_diff.con
-cic:/Coq/IntMap/Fset/in_FSet_inter.con
-cic:/Coq/IntMap/Fset/in_FSet_union.con
-cic:/Coq/IntMap/Fset/MapDom.con
-cic:/Coq/IntMap/Fset/MapDom_Dom.con
-cic:/Coq/IntMap/Fset/MapDomRestrBy.con
-cic:/Coq/IntMap/Fset/MapDomRestrBy_semantics.con
-cic:/Coq/IntMap/Fset/MapDomRestrTo.con
-cic:/Coq/IntMap/Fset/MapDomRestrTo_semantics.con
-cic:/Coq/IntMap/Fset/MapDom_semantics_1.con
-cic:/Coq/IntMap/Fset/MapDom_semantics_2.con
-cic:/Coq/IntMap/Fset/MapDom_semantics_3.con
-cic:/Coq/IntMap/Fset/MapDom_semantics_4.con
-cic:/Coq/IntMap/Lsort/aapp_length.con
-cic:/Coq/IntMap/Lsort/ad_bit_0_gt.con
-cic:/Coq/IntMap/Lsort/ad_bit_0_less.con
-cic:/Coq/IntMap/Lsort/ad_comp_double_monotonic.con
-cic:/Coq/IntMap/Lsort/ad_comp_double_plus_un_monotonic.con
-cic:/Coq/IntMap/Lsort/ad_comp_monotonic.con
-cic:/Coq/IntMap/Lsort/ad_double_monotonic.con
-cic:/Coq/IntMap/Lsort/ad_double_plus_un_monotonic.con
-cic:/Coq/IntMap/Lsort/ad_ind_double.con
-cic:/Coq/IntMap/Lsort/ad_less_1.con
-cic:/Coq/IntMap/Lsort/ad_less.con
-cic:/Coq/IntMap/Lsort/ad_less_def_1.con
-cic:/Coq/IntMap/Lsort/ad_less_def_2.con
-cic:/Coq/IntMap/Lsort/ad_less_def_3.con
-cic:/Coq/IntMap/Lsort/ad_less_def_4.con
-cic:/Coq/IntMap/Lsort/ad_less_not_refl.con
-cic:/Coq/IntMap/Lsort/ad_less_total.con
-cic:/Coq/IntMap/Lsort/ad_less_trans.con
-cic:/Coq/IntMap/Lsort/ad_less_z.con
-cic:/Coq/IntMap/Lsort/ad_monotonic.con
-cic:/Coq/IntMap/Lsort/ad_rec_double.con
-cic:/Coq/IntMap/Lsort/ad_z_less_1.con
-cic:/Coq/IntMap/Lsort/ad_z_less_2.con
-cic:/Coq/IntMap/Lsort/alist_canonical.con
-cic:/Coq/IntMap/Lsort/alist_conc_sorted.con
-cic:/Coq/IntMap/Lsort/alist_nth_ad_aapp_1.con
-cic:/Coq/IntMap/Lsort/alist_nth_ad_aapp_2.con
-cic:/Coq/IntMap/Lsort/alist_nth_ad.con
-cic:/Coq/IntMap/Lsort/alist_nth_ad_semantics.con
-cic:/Coq/IntMap/Lsort/alist_of_Map_nth_ad.con
-cic:/Coq/IntMap/Lsort/alist_of_Map_sorts_1.con
-cic:/Coq/IntMap/Lsort/alist_of_Map_sorts1.con
-cic:/Coq/IntMap/Lsort/alist_of_Map_sorts2.con
-cic:/Coq/IntMap/Lsort/alist_of_Map_sorts.con
-cic:/Coq/IntMap/Lsort/alist_semantics_nth_ad.con
-cic:/Coq/IntMap/Lsort/alist_semantics_same_tail.con
-cic:/Coq/IntMap/Lsort/alist_semantics_tail.con
-cic:/Coq/IntMap/Lsort/alist_sorted_1.con
-cic:/Coq/IntMap/Lsort/alist_sorted_1_imp_2.con
-cic:/Coq/IntMap/Lsort/alist_sorted_2.con
-cic:/Coq/IntMap/Lsort/alist_sorted_2_imp.con
-cic:/Coq/IntMap/Lsort/alist_sorted.con
-cic:/Coq/IntMap/Lsort/alist_sorted_imp_1.con
-cic:/Coq/IntMap/Lsort/alist_sorted_tail.con
-cic:/Coq/IntMap/Lsort/alist_too_low.con
-cic:/Coq/IntMap/Lsort/app_length.con
-cic:/Coq/IntMap/Lsort/interval_split.con
-cic:/Coq/IntMap/Mapaxioms/eqmap.con
-cic:/Coq/IntMap/Mapaxioms/eqmap_refl.con
-cic:/Coq/IntMap/Mapaxioms/eqmap_sym.con
-cic:/Coq/IntMap/Mapaxioms/eqmap_trans.con
-cic:/Coq/IntMap/Mapaxioms/eqm_refl.con
-cic:/Coq/IntMap/Mapaxioms/eqm_sym.con
-cic:/Coq/IntMap/Mapaxioms/eqm_trans.con
-cic:/Coq/IntMap/Mapaxioms/FSetDelta_assoc.con
-cic:/Coq/IntMap/Mapaxioms/FSet_ext.con
-cic:/Coq/IntMap/Mapaxioms/FSetInter_assoc.con
-cic:/Coq/IntMap/Mapaxioms/FSetInter_comm.con
-cic:/Coq/IntMap/Mapaxioms/FSetInter_idempotent.con
-cic:/Coq/IntMap/Mapaxioms/FSetInter_M0_s.con
-cic:/Coq/IntMap/Mapaxioms/FSetInter_s_M0.con
-cic:/Coq/IntMap/Mapaxioms/FSetInter_Union_l.con
-cic:/Coq/IntMap/Mapaxioms/FSetInter_Union_r.con
-cic:/Coq/IntMap/Mapaxioms/FSetUnion_assoc.con
-cic:/Coq/IntMap/Mapaxioms/FSetUnion_comm.con
-cic:/Coq/IntMap/Mapaxioms/FSetUnion_idempotent.con
-cic:/Coq/IntMap/Mapaxioms/FSetUnion_Inter_l.con
-cic:/Coq/IntMap/Mapaxioms/FSetUnion_Inter_r.con
-cic:/Coq/IntMap/Mapaxioms/FSetUnion_M0_s.con
-cic:/Coq/IntMap/Mapaxioms/FSetUnion_s_M0.con
-cic:/Coq/IntMap/Mapaxioms/MapDelta_as_DomRestrBy_2.con
-cic:/Coq/IntMap/Mapaxioms/MapDelta_as_DomRestrBy.con
-cic:/Coq/IntMap/Mapaxioms/MapDelta_as_Merge.con
-cic:/Coq/IntMap/Mapaxioms/MapDelta_empty_m_1.con
-cic:/Coq/IntMap/Mapaxioms/MapDelta_empty_m.con
-cic:/Coq/IntMap/Mapaxioms/MapDelta_ext.con
-cic:/Coq/IntMap/Mapaxioms/MapDelta_ext_l.con
-cic:/Coq/IntMap/Mapaxioms/MapDelta_ext_r.con
-cic:/Coq/IntMap/Mapaxioms/MapDelta_m_empty_1.con
-cic:/Coq/IntMap/Mapaxioms/MapDelta_m_empty.con
-cic:/Coq/IntMap/Mapaxioms/MapDelta_nilpotent.con
-cic:/Coq/IntMap/Mapaxioms/MapDelta_sym.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_By_comm.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_By.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_Dom.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_empty_m_1.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_empty_m.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_ext.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_ext_l.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_ext_r.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_m_empty_1.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_m_empty.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_m_m_1.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_m_m.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_To_comm.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_To.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrTo_assoc.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrTo_By_comm.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrTo_By.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrTo_Dom.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrTo_empty_m_1.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrTo_empty_m.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrTo_ext.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrTo_ext_l.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrTo_ext_r.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrTo_idempotent.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrTo_m_empty_1.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrTo_m_empty.con
-cic:/Coq/IntMap/Mapaxioms/MapDomRestrTo_To_comm.con
-cic:/Coq/IntMap/Mapaxioms/MapDom_Split_1.con
-cic:/Coq/IntMap/Mapaxioms/MapDom_Split_2.con
-cic:/Coq/IntMap/Mapaxioms/MapDom_Split_3.con
-cic:/Coq/IntMap/Mapaxioms/MapMerge_assoc.con
-cic:/Coq/IntMap/Mapaxioms/MapMerge_DomRestrBy.con
-cic:/Coq/IntMap/Mapaxioms/MapMerge_DomRestrTo.con
-cic:/Coq/IntMap/Mapaxioms/MapMerge_empty_l.con
-cic:/Coq/IntMap/Mapaxioms/MapMerge_empty_m_1.con
-cic:/Coq/IntMap/Mapaxioms/MapMerge_empty_m.con
-cic:/Coq/IntMap/Mapaxioms/MapMerge_empty_r.con
-cic:/Coq/IntMap/Mapaxioms/MapMerge_ext.con
-cic:/Coq/IntMap/Mapaxioms/MapMerge_ext_l.con
-cic:/Coq/IntMap/Mapaxioms/MapMerge_ext_r.con
-cic:/Coq/IntMap/Mapaxioms/MapMerge_idempotent.con
-cic:/Coq/IntMap/Mapaxioms/MapMerge_m_empty_1.con
-cic:/Coq/IntMap/Mapaxioms/MapMerge_m_empty.con
-cic:/Coq/IntMap/Mapaxioms/MapMerge_RestrTo_l.con
-cic:/Coq/IntMap/Mapaxioms/MapPut_as_Merge.con
-cic:/Coq/IntMap/Mapaxioms/MapPut_behind_as_Merge.con
-cic:/Coq/IntMap/Mapaxioms/MapPut_behind_ext.con
-cic:/Coq/IntMap/Mapaxioms/MapPut_ext.con
-cic:/Coq/IntMap/Mapaxioms/MapRemove_as_RestrBy.con
-cic:/Coq/IntMap/Mapaxioms/MapRemove_ext.con
-cic:/Coq/IntMap/Mapc/alist_of_Map_of_alist_c.con
-cic:/Coq/IntMap/Mapcanon/M2_eqmap_1.con
-cic:/Coq/IntMap/Mapcanon/M2_eqmap_2.con
-cic:/Coq/IntMap/Mapcanon/makeM2_canon.con
-cic:/Coq/IntMap/Mapcanon/mapcanon_exists_1.con
-cic:/Coq/IntMap/Mapcanon/mapcanon_exists_2.con
-cic:/Coq/IntMap/Mapcanon/mapcanon_exists.con
-cic:/Coq/IntMap/Mapcanon/MapCanonicalize.con
-cic:/Coq/IntMap/Mapcanon/mapcanon.ind
-cic:/Coq/IntMap/Mapcanon/mapcanon_ind.con
-cic:/Coq/IntMap/Mapcanon/mapcanon_M2_1.con
-cic:/Coq/IntMap/Mapcanon/mapcanon_M2_2.con
-cic:/Coq/IntMap/Mapcanon/mapcanon_M2.con
-cic:/Coq/IntMap/Mapcanon/mapcanon_unique.con
-cic:/Coq/IntMap/Mapcanon/MapCollect_canon.con
-cic:/Coq/IntMap/Mapcanon/MapDelta_canon.con
-cic:/Coq/IntMap/Mapcanon/MapDom_canon.con
-cic:/Coq/IntMap/Mapcanon/MapDomRestrBy_canon.con
-cic:/Coq/IntMap/Mapcanon/MapDomRestrTo_canon.con
-cic:/Coq/IntMap/Mapcanon/MapFold_canon_1.con
-cic:/Coq/IntMap/Mapcanon/MapFold_canon.con
-cic:/Coq/IntMap/Mapcanon/MapMerge_canon.con
-cic:/Coq/IntMap/Mapcanon/Map_of_alist_canon.con
-cic:/Coq/IntMap/Mapcanon/MapPut1_canon.con
-cic:/Coq/IntMap/Mapcanon/MapPut_behind_canon.con
-cic:/Coq/IntMap/Mapcanon/MapPut_canon.con
-cic:/Coq/IntMap/Mapcanon/MapRemove_canon.con
-cic:/Coq/IntMap/Mapcanon/MapSubset_c_1.con
-cic:/Coq/IntMap/Mapcanon/MapSubset_c_2.con
-cic:/Coq/IntMap/Mapcard/length_as_fold_2.con
-cic:/Coq/IntMap/Mapcard/length_as_fold.con
-cic:/Coq/IntMap/Mapcard/MapCard_as_Fold_1.con
-cic:/Coq/IntMap/Mapcard/MapCard_as_Fold.con
-cic:/Coq/IntMap/Mapcard/MapCard_as_length.con
-cic:/Coq/IntMap/Mapcard/MapCard_Dom.con
-cic:/Coq/IntMap/Mapcard/MapCard_Dom_Put_behind.con
-cic:/Coq/IntMap/Mapcard/MapCard_ext.con
-cic:/Coq/IntMap/Mapcard/MapCard_is_not_O.con
-cic:/Coq/IntMap/Mapcard/MapCard_is_O.con
-cic:/Coq/IntMap/Mapcard/MapCard_is_one.con
-cic:/Coq/IntMap/Mapcard/MapCard_is_one_unique.con
-cic:/Coq/IntMap/Mapcard/MapCard_is_Sn.con
-cic:/Coq/IntMap/Mapcard/MapCard_M0.con
-cic:/Coq/IntMap/Mapcard/MapCard_M1.con
-cic:/Coq/IntMap/Mapcard/MapCard_makeM2.con
-cic:/Coq/IntMap/Mapcard/MapCard_Put_1.con
-cic:/Coq/IntMap/Mapcard/MapCard_Put_1_conv.con
-cic:/Coq/IntMap/Mapcard/MapCard_Put1_equals_2.con
-cic:/Coq/IntMap/Mapcard/MapCard_Put_2.con
-cic:/Coq/IntMap/Mapcard/MapCard_Put_2_conv.con
-cic:/Coq/IntMap/Mapcard/MapCard_Put_behind_Put.con
-cic:/Coq/IntMap/Mapcard/MapCard_Put_behind_sum.con
-cic:/Coq/IntMap/Mapcard/MapCard_Put_lb.con
-cic:/Coq/IntMap/Mapcard/MapCard_Put_sum.con
-cic:/Coq/IntMap/Mapcard/MapCard_Put_ub.con
-cic:/Coq/IntMap/Mapcard/MapCard_Remove_1.con
-cic:/Coq/IntMap/Mapcard/MapCard_Remove_1_conv.con
-cic:/Coq/IntMap/Mapcard/MapCard_Remove_2.con
-cic:/Coq/IntMap/Mapcard/MapCard_Remove_2_conv.con
-cic:/Coq/IntMap/Mapcard/MapCard_Remove_lb.con
-cic:/Coq/IntMap/Mapcard/MapCard_Remove_sum.con
-cic:/Coq/IntMap/Mapcard/MapCard_Remove_ub.con
-cic:/Coq/IntMap/Mapcard/MapDomRestrBy_Card_lb.con
-cic:/Coq/IntMap/Mapcard/MapDomRestrBy_Card_ub_l.con
-cic:/Coq/IntMap/Mapcard/MapDomRestrTo_Card_ub_l.con
-cic:/Coq/IntMap/Mapcard/MapDomRestrTo_Card_ub_r.con
-cic:/Coq/IntMap/Mapcard/MapMerge_Card_disjoint.con
-cic:/Coq/IntMap/Mapcard/MapMerge_Card_lb_l.con
-cic:/Coq/IntMap/Mapcard/MapMerge_Card_lb_r.con
-cic:/Coq/IntMap/Mapcard/MapMerge_Card_ub.con
-cic:/Coq/IntMap/Mapcard/MapMerge_disjoint_Card.con
-cic:/Coq/IntMap/Mapcard/MapMerge_Restr_Card.con
-cic:/Coq/IntMap/Mapcard/MapSplit_Card.con
-cic:/Coq/IntMap/Mapcard/MapSubset_card_eq_1.con
-cic:/Coq/IntMap/Mapcard/MapSubset_card_eq.con
-cic:/Coq/IntMap/Mapcard/MapSubset_Card_le.con
-cic:/Coq/IntMap/Mapc/FSetDelta_assoc_c.con
-cic:/Coq/IntMap/Mapc/FSet_ext_c.con
-cic:/Coq/IntMap/Mapc/FSetInter_assoc_c.con
-cic:/Coq/IntMap/Mapc/FSetInter_comm_c.con
-cic:/Coq/IntMap/Mapc/FSetInter_idempotent.con
-cic:/Coq/IntMap/Mapc/FSetInter_M0_s_c.con
-cic:/Coq/IntMap/Mapc/FSetInter_s_M0_c.con
-cic:/Coq/IntMap/Mapc/FSetInter_Union_l_c.con
-cic:/Coq/IntMap/Mapc/FSetInter_Union_r.con
-cic:/Coq/IntMap/Mapc/FSetUnion_assoc_c.con
-cic:/Coq/IntMap/Mapc/FSetUnion_comm_c.con
-cic:/Coq/IntMap/Mapc/FSetUnion_idempotent.con
-cic:/Coq/IntMap/Mapc/FSetUnion_Inter_l_c.con
-cic:/Coq/IntMap/Mapc/FSetUnion_Inter_r.con
-cic:/Coq/IntMap/Mapc/FSetUnion_M0_s_c.con
-cic:/Coq/IntMap/Mapc/FSetUnion_s_M0_c.con
-cic:/Coq/IntMap/Mapc/FSubset_antisym_c.con
-cic:/Coq/IntMap/Mapc/MapDelta_as_DomRestrBy_2_c.con
-cic:/Coq/IntMap/Mapc/MapDelta_as_DomRestrBy_c.con
-cic:/Coq/IntMap/Mapc/MapDelta_as_Merge_c.con
-cic:/Coq/IntMap/Mapc/MapDelta_disjoint_c.con
-cic:/Coq/IntMap/Mapc/MapDelta_nilpotent_c.con
-cic:/Coq/IntMap/Mapc/MapDelta_sym_c.con
-cic:/Coq/IntMap/Mapc/MapDisjoint_empty_c.con
-cic:/Coq/IntMap/Mapc/MapDomRestrBy_By_c.con
-cic:/Coq/IntMap/Mapc/MapDomRestrBy_By_comm_c.con
-cic:/Coq/IntMap/Mapc/MapDomRestrBy_Dom_c.con
-cic:/Coq/IntMap/Mapc/MapDomRestrBy_To_c.con
-cic:/Coq/IntMap/Mapc/MapDomRestrBy_To_comm_c.con
-cic:/Coq/IntMap/Mapc/MapDomRestrTo_assoc_c.con
-cic:/Coq/IntMap/Mapc/MapDomRestrTo_By_c.con
-cic:/Coq/IntMap/Mapc/MapDomRestrTo_By_comm_c.con
-cic:/Coq/IntMap/Mapc/MapDomRestrTo_Dom_c.con
-cic:/Coq/IntMap/Mapc/MapDomRestrTo_idempotent_c.con
-cic:/Coq/IntMap/Mapc/MapDomRestrTo_To_comm_c.con
-cic:/Coq/IntMap/Mapc/MapDom_Split_1_c.con
-cic:/Coq/IntMap/Mapc/MapDom_Split_2_c.con
-cic:/Coq/IntMap/Mapc/MapDom_Split_3_c.con
-cic:/Coq/IntMap/Mapc/MapMerge_assoc_c.con
-cic:/Coq/IntMap/Mapc/MapMerge_DomRestrBy_c.con
-cic:/Coq/IntMap/Mapc/MapMerge_DomRestrTo_c.con
-cic:/Coq/IntMap/Mapc/MapMerge_empty_m_c.con
-cic:/Coq/IntMap/Mapc/MapMerge_idempotent_c.con
-cic:/Coq/IntMap/Mapc/MapMerge_RestrTo_l_c.con
-cic:/Coq/IntMap/Mapc/Map_of_alist_of_Map_c.con
-cic:/Coq/IntMap/Mapc/MapPut_as_Merge_c.con
-cic:/Coq/IntMap/Mapc/MapPut_behind_as_Merge_c.con
-cic:/Coq/IntMap/Mapc/MapRemove_as_RestrBy_c.con
-cic:/Coq/IntMap/Mapc/MapSubset_antisym_c.con
-cic:/Coq/IntMap/Map/eqm.con
-cic:/Coq/IntMap/Mapfold/DMerge.con
-cic:/Coq/IntMap/Mapfold/in_dom_DMerge_1.con
-cic:/Coq/IntMap/Mapfold/in_dom_DMerge_2.con
-cic:/Coq/IntMap/Mapfold/in_dom_DMerge_3.con
-cic:/Coq/IntMap/Mapfold/MapFold1_as_Fold_1.con
-cic:/Coq/IntMap/Mapfold/MapFold1_as_Fold.con
-cic:/Coq/IntMap/Mapfold/MapFold1_ext.con
-cic:/Coq/IntMap/Mapfold/MapFold_distr_l.con
-cic:/Coq/IntMap/Mapfold/MapFold_distr_r_1.con
-cic:/Coq/IntMap/Mapfold/MapFold_distr_r.con
-cic:/Coq/IntMap/Mapfold/MapFold_ext.con
-cic:/Coq/IntMap/Mapfold/MapFold_ext_f_1.con
-cic:/Coq/IntMap/Mapfold/MapFold_ext_f.con
-cic:/Coq/IntMap/Mapfold/MapFold_Merge_disjoint_1.con
-cic:/Coq/IntMap/Mapfold/MapFold_Merge_disjoint.con
-cic:/Coq/IntMap/Mapfold/MapFold_orb_1.con
-cic:/Coq/IntMap/Mapfold/MapFold_orb.con
-cic:/Coq/IntMap/Mapfold/MapFold_Put_behind_disjoint_2.con
-cic:/Coq/IntMap/Mapfold/MapFold_Put_behind_disjoint.con
-cic:/Coq/IntMap/Mapfold/MapFold_Put_disjoint_1.con
-cic:/Coq/IntMap/Mapfold/MapFold_Put_disjoint_2.con
-cic:/Coq/IntMap/Mapfold/MapFold_Put_disjoint.con
-cic:/Coq/IntMap/Mapiter/aapp.con
-cic:/Coq/IntMap/Mapiter/acons.con
-cic:/Coq/IntMap/Mapiter/ad_comp_double_inj.con
-cic:/Coq/IntMap/Mapiter/ad_comp_double_plus_un_inj.con
-cic:/Coq/IntMap/Mapiter/ad_inj.con
-cic:/Coq/IntMap/Mapiter/alist.con
-cic:/Coq/IntMap/Mapiter/alist_MapMerge_semantics.con
-cic:/Coq/IntMap/Mapiter/alist_MapMerge_semantics_disjoint.con
-cic:/Coq/IntMap/Mapiter/alist_of_Map.con
-cic:/Coq/IntMap/Mapiter/alist_of_Map_of_alist.con
-cic:/Coq/IntMap/Mapiter/alist_of_Map_semantics_1_1.con
-cic:/Coq/IntMap/Mapiter/alist_of_Map_semantics_1.con
-cic:/Coq/IntMap/Mapiter/alist_of_Map_semantics.con
-cic:/Coq/IntMap/Mapiter/alist_semantics_app.con
-cic:/Coq/IntMap/Mapiter/alist_semantics.con
-cic:/Coq/IntMap/Mapiter/alist_semantics_disjoint_comm.con
-cic:/Coq/IntMap/Mapiter/anil.con
-cic:/Coq/IntMap/Mapiter/fold_right_aapp.con
-cic:/Coq/IntMap/Mapiter/MapCollect1.con
-cic:/Coq/IntMap/Mapiter/MapCollect_as_Fold.con
-cic:/Coq/IntMap/Mapiter/MapCollect.con
-cic:/Coq/IntMap/Mapiter/MapFold1.con
-cic:/Coq/IntMap/Mapiter/MapFold1_state.con
-cic:/Coq/IntMap/Mapiter/MapFold_as_fold_1.con
-cic:/Coq/IntMap/Mapiter/MapFold_as_fold.con
-cic:/Coq/IntMap/Mapiter/MapFold.con
-cic:/Coq/IntMap/Mapiter/MapFold_empty.con
-cic:/Coq/IntMap/Mapiter/MapFold_M1.con
-cic:/Coq/IntMap/Mapiter/MapFold_state.con
-cic:/Coq/IntMap/Mapiter/MapFold_state_stateless_1.con
-cic:/Coq/IntMap/Mapiter/MapFold_state_stateless.con
-cic:/Coq/IntMap/Mapiter/Map_of_alist.con
-cic:/Coq/IntMap/Mapiter/Map_of_alist_of_Map.con
-cic:/Coq/IntMap/Mapiter/Map_of_alist_semantics.con
-cic:/Coq/IntMap/Mapiter/MapSweep1.con
-cic:/Coq/IntMap/Mapiter/MapSweep2.con
-cic:/Coq/IntMap/Mapiter/MapSweep.con
-cic:/Coq/IntMap/Mapiter/MapSweep_semantics_1_1.con
-cic:/Coq/IntMap/Mapiter/MapSweep_semantics_1.con
-cic:/Coq/IntMap/Mapiter/MapSweep_semantics_2_1.con
-cic:/Coq/IntMap/Mapiter/MapSweep_semantics_2_2.con
-cic:/Coq/IntMap/Mapiter/MapSweep_semantics_2.con
-cic:/Coq/IntMap/Mapiter/MapSweep_semantics_3_1.con
-cic:/Coq/IntMap/Mapiter/MapSweep_semantics_3.con
-cic:/Coq/IntMap/Mapiter/MapSweep_semantics_4_1.con
-cic:/Coq/IntMap/Mapiter/MapSweep_semantics_4.con
-cic:/Coq/IntMap/Mapiter/pair_sp.con
-cic:/Coq/IntMap/Maplists/ad_in_elems_in_list.con
-cic:/Coq/IntMap/Maplists/ad_in_list_app_1.con
-cic:/Coq/IntMap/Maplists/ad_in_list_app.con
-cic:/Coq/IntMap/Maplists/ad_in_list.con
-cic:/Coq/IntMap/Maplists/ad_in_list_forms_circuit.con
-cic:/Coq/IntMap/Maplists/ad_in_list_l.con
-cic:/Coq/IntMap/Maplists/ad_in_list_of_dom_in_dom.con
-cic:/Coq/IntMap/Maplists/ad_in_list_r.con
-cic:/Coq/IntMap/Maplists/ad_in_list_rev.con
-cic:/Coq/IntMap/Maplists/ad_list_app_length.con
-cic:/Coq/IntMap/Maplists/ad_list_app_rev.con
-cic:/Coq/IntMap/Maplists/ad_list_card.con
-cic:/Coq/IntMap/Maplists/ad_list_Elems.con
-cic:/Coq/IntMap/Maplists/ad_list_has_circuit_stutters.con
-cic:/Coq/IntMap/Maplists/ad_list_not_stutters_card.con
+cic:/CoRN/algebra/Basics/well_founded_ltof.con
+cic:/CoRN/algebra/Basics/well_founded_induction_type.con
+cic:/CoRN/algebra/Basics/well_founded.con
+cic:/CoRN/algebra/Basics/surj_not.con
+cic:/CoRN/algebra/Basics/surj_lt_subproof.con
+cic:/CoRN/algebra/Basics/surj_lt.con
+cic:/CoRN/algebra/Basics/surj_le_subproof.con
+cic:/CoRN/algebra/Basics/surj_le.con
+cic:/CoRN/algebra/Basics/surj_eq_subproof.con
+cic:/CoRN/algebra/Basics/surj_eq.con
+cic:/CoRN/algebra/Basics/proper_caseZ_diff_subproof0.con
+cic:/CoRN/algebra/Basics/proper_caseZ_diff_subproof.con
+cic:/CoRN/algebra/Basics/proper_caseZ_diff.con
+cic:/CoRN/algebra/Basics/pred_succ_Z_ind.con
+cic:/CoRN/algebra/Basics/power.con
+cic:/CoRN/algebra/Basics/p_is_some_anti_convert.con
+cic:/CoRN/algebra/Basics/not_r_sumbool_rec.con
+cic:/CoRN/algebra/Basics/not_l_sumbool_rec.con
+cic:/CoRN/algebra/Basics/nats_Z_ind.con
+cic:/CoRN/algebra/Basics/nat_fac_gtzero.con
+cic:/CoRN/algebra/Basics/minus4_subproof1.con
+cic:/CoRN/algebra/Basics/minus4_subproof0.con
+cic:/CoRN/algebra/Basics/minus4_subproof.con
+cic:/CoRN/algebra/Basics/minus4.con
+cic:/CoRN/algebra/Basics/minus3_subproof1.con
+cic:/CoRN/algebra/Basics/minus3_subproof0.con
+cic:/CoRN/algebra/Basics/minus3_subproof.con
+cic:/CoRN/algebra/Basics/minus3.con
+cic:/CoRN/algebra/Basics/min_convert_is_NEG.con
+cic:/CoRN/algebra/Basics/ltof.con
+cic:/CoRN/algebra/Basics/lt_z_two.con
+cic:/CoRN/algebra/Basics/lt_wf_rect.con
+cic:/CoRN/algebra/Basics/lt_mult_right.con
+cic:/CoRN/algebra/Basics/lt_lt_minus_subproof.con
+cic:/CoRN/algebra/Basics/lt_lt_minus.con
+cic:/CoRN/algebra/Basics/lt_le_dec.con
+cic:/CoRN/algebra/Basics/lt_O_positive_to_nat.con
+cic:/CoRN/algebra/Basics/le_pred.con
+cic:/CoRN/algebra/Basics/le_mult_right.con
+cic:/CoRN/algebra/Basics/inject_nat_convert.con
+cic:/CoRN/algebra/Basics/induction_ltof2T.con
+cic:/CoRN/algebra/Basics/fac.con
+cic:/CoRN/algebra/Basics/diff_Z_ind_subproof.con
+cic:/CoRN/algebra/Basics/diff_Z_ind.con
+cic:/CoRN/algebra/Basics/convert_is_POS.con
+cic:/CoRN/algebra/Basics/caseZ_diff_Pos.con
+cic:/CoRN/algebra/Basics/caseZ_diff_O.con
+cic:/CoRN/algebra/Basics/caseZ_diff_Neg.con
+cic:/CoRN/algebra/Basics/caseZ_diff.con
+cic:/CoRN/algebra/Basics/anti_convert_pred_convert.con
+cic:/CoRN/algebra/Basics/Zodd_Zeven_min1.con
+cic:/CoRN/algebra/Basics/Zmult_minus_distr_r.con
+cic:/CoRN/algebra/Basics/Zmult_absorb.con
+cic:/CoRN/algebra/Basics/Zlt_reg_mult_l.con
+cic:/CoRN/algebra/Basics/Zlt_opp.con
+cic:/CoRN/algebra/Basics/Zlt_conv_mult_l.con
+cic:/CoRN/algebra/Basics/Zgt_not_eq.con
+cic:/CoRN/algebra/Basics/Z_to_nat_correct.con
+cic:/CoRN/algebra/Basics/Z_to_nat.con
+cic:/CoRN/algebra/Basics/Z_exh.con
+cic:/CoRN/algebra/Basics/POS_anti_convert.con
+cic:/CoRN/algebra/Basics/NEG_anti_convert.con
+cic:/CoRN/algebra/Basics/Acc_iter.con
+cic:/CoRN/algebra/Basics/Acc_inv.con
+cic:/CoRN/algebra/Basics/Acc_ind.con
+cic:/CoRN/algebra/Basics/Acc.ind
+cic:/CoRN/algebra/CAbGroups/zmult_zero.con
+cic:/CoRN/algebra/CAbGroups/zmult_wd.con
+cic:/CoRN/algebra/CAbGroups/zmult_plus.con
+cic:/CoRN/algebra/CAbGroups/zmult_plus'.con
+cic:/CoRN/algebra/CAbGroups/zmult_one.con
+cic:/CoRN/algebra/CAbGroups/zmult_mult.con
+cic:/CoRN/algebra/CAbGroups/zmult_min_one.con
+cic:/CoRN/algebra/CAbGroups/zmult_char_subproof1.con
+cic:/CoRN/algebra/CAbGroups/zmult_char_subproof0.con
+cic:/CoRN/algebra/CAbGroups/zmult_char_subproof.con
+cic:/CoRN/algebra/CAbGroups/zmult_char.con
+cic:/CoRN/algebra/CAbGroups/zmult_Zero.con
+cic:/CoRN/algebra/CAbGroups/zmult.con
+cic:/CoRN/algebra/CAbGroups/plus_runit.con
+cic:/CoRN/algebra/CAbGroups/plus_rext.con
+cic:/CoRN/algebra/CAbGroups/plus_is_fun.con
+cic:/CoRN/algebra/CAbGroups/plus_fun.con
+cic:/CoRN/algebra/CAbGroups/plus_cancel_ap_lft.con
+cic:/CoRN/algebra/CAbGroups/op_lft_resp_ap.con
+cic:/CoRN/algebra/CAbGroups/nmult_wd.con
+cic:/CoRN/algebra/CAbGroups/nmult_plus.con
+cic:/CoRN/algebra/CAbGroups/nmult_plus'.con
+cic:/CoRN/algebra/CAbGroups/nmult_one.con
+cic:/CoRN/algebra/CAbGroups/nmult_mult.con
+cic:/CoRN/algebra/CAbGroups/nmult_inv.con
+cic:/CoRN/algebra/CAbGroups/nmult_Zero.con
+cic:/CoRN/algebra/CAbGroups/nmult.con
+cic:/CoRN/algebra/CAbGroups/minus_plus.con
+cic:/CoRN/algebra/CAbGroups/isabgrp_scrr.con
+cic:/CoRN/algebra/CAbGroups/is_CAbGroup.con
+cic:/CoRN/algebra/CAbGroups/inv_inv'.con
+cic:/CoRN/algebra/CAbGroups/cag_proof.con
+cic:/CoRN/algebra/CAbGroups/cag_op_inv.con
+cic:/CoRN/algebra/CAbGroups/cag_crr.con
+cic:/CoRN/algebra/CAbGroups/cag_commutes_unfolded.con
+cic:/CoRN/algebra/CAbGroups/cag_commutes.con
+cic:/CoRN/algebra/CAbGroups/cag_ap_cancel_lft.con
+cic:/CoRN/algebra/CAbGroups/assoc_1.con
+cic:/CoRN/algebra/CAbGroups/CAbGroup_rect.con
+cic:/CoRN/algebra/CAbGroups/CAbGroup_rec.con
+cic:/CoRN/algebra/CAbGroups/CAbGroup_is_CAbGroup.con
+cic:/CoRN/algebra/CAbGroups/CAbGroup_ind.con
+cic:/CoRN/algebra/CAbGroups/CAbGroup.ind
+cic:/CoRN/algebra/CAbGroups/Build_SubCAbGroup.con
+cic:/CoRN/algebra/CAbGroups/Build_CSemiGroup'.con
+cic:/CoRN/algebra/CAbGroups/Build_CMonoid'.con
+cic:/CoRN/algebra/CAbGroups/Build_CGroup'.con
+cic:/CoRN/algebra/CAbGroups/Build_CAbGroup'.con
+cic:/CoRN/algebra/CAbMonoids/isabgrp_scrr.con
+cic:/CoRN/algebra/CAbMonoids/is_CAbMonoid.con
+cic:/CoRN/algebra/CAbMonoids/cam_proof.con
+cic:/CoRN/algebra/CAbMonoids/cam_crr.con
+cic:/CoRN/algebra/CAbMonoids/cam_commutes_unfolded.con
+cic:/CoRN/algebra/CAbMonoids/cam_commutes.con
+cic:/CoRN/algebra/CAbMonoids/CAbMonoid_rect.con
+cic:/CoRN/algebra/CAbMonoids/CAbMonoid_rec.con
+cic:/CoRN/algebra/CAbMonoids/CAbMonoid_is_CAbMonoid.con
+cic:/CoRN/algebra/CAbMonoids/CAbMonoid_ind.con
+cic:/CoRN/algebra/CAbMonoids/CAbMonoid.ind
+cic:/CoRN/algebra/CAbMonoids/Build_SubCAbMonoid.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/tau_surj.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/tau_strext.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/tau_is_fun.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/tau.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/sigst_strext.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/sigst_is_fun.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/sigst_inj.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/sigst.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/cswdpredR.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/cswdpred.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/cspredR.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/cspred.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/cs_is_comod.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/cs_is_coideal.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/cs_as_comod.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/cs_as_coideal.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/Rtau_surj.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/Rtau_strext.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/Rtau_is_fun.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/Rtau.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/Rsigst_strext.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/Rsigst_is_fun.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/Rsigst_inj.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/Rsigst.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/RingHomTheorem.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/RdivCsR.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/ModHomTheorem.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/CsR.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/Cs.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/AdivCs.con
+cic:/CoRN/algebra/CIdeals/is_ideal_rect.con
+cic:/CoRN/algebra/CIdeals/is_ideal_rec.con
+cic:/CoRN/algebra/CIdeals/is_ideal_ind.con
+cic:/CoRN/algebra/CIdeals/is_ideal.ind
+cic:/CoRN/algebra/CIdeals/is_coideal_rect.con
+cic:/CoRN/algebra/CIdeals/is_coideal_rec.con
+cic:/CoRN/algebra/CIdeals/is_coideal_ind.con
+cic:/CoRN/algebra/CIdeals/is_coideal.ind
+cic:/CoRN/algebra/CIdeals/idprpl.con
+cic:/CoRN/algebra/CIdeals/idproof.con
+cic:/CoRN/algebra/CIdeals/idpred.con
+cic:/CoRN/algebra/CIdeals/ideal_rect.con
+cic:/CoRN/algebra/CIdeals/ideal_rec.con
+cic:/CoRN/algebra/CIdeals/ideal_is_ideal.con
+cic:/CoRN/algebra/CIdeals/ideal_ind.con
+cic:/CoRN/algebra/CIdeals/ideal_as_CSetoid.con
+cic:/CoRN/algebra/CIdeals/ideal.ind
+cic:/CoRN/algebra/CIdeals/idax.con
+cic:/CoRN/algebra/CIdeals/coideal_wd.con
+cic:/CoRN/algebra/CIdeals/coideal_rect.con
+cic:/CoRN/algebra/CIdeals/coideal_rec.con
+cic:/CoRN/algebra/CIdeals/coideal_plus.con
+cic:/CoRN/algebra/CIdeals/coideal_nonzero.con
+cic:/CoRN/algebra/CIdeals/coideal_nontriv.con
+cic:/CoRN/algebra/CIdeals/coideal_mult.con
+cic:/CoRN/algebra/CIdeals/coideal_is_coideal.con
+cic:/CoRN/algebra/CIdeals/coideal_ind.con
+cic:/CoRN/algebra/CIdeals/coideal_as_CSetoid.con
+cic:/CoRN/algebra/CIdeals/coideal_apzero.con
+cic:/CoRN/algebra/CIdeals/coideal.ind
+cic:/CoRN/algebra/CIdeals/ciproof.con
+cic:/CoRN/algebra/CIdeals/cipred.con
+cic:/CoRN/algebra/CIdeals/ciplus.con
+cic:/CoRN/algebra/CIdeals/cinontriv.con
+cic:/CoRN/algebra/CIdeals/cimult.con
+cic:/CoRN/algebra/CIdeals/ciapzero.con
+cic:/CoRN/algebra/CLogic/weird_mon_covers.con
+cic:/CoRN/algebra/CLogic/to_Codd_even.con
+cic:/CoRN/algebra/CLogic/to_Codd.con
+cic:/CoRN/algebra/CLogic/to_Ceven.con
+cic:/CoRN/algebra/CLogic/toCle.con
+cic:/CoRN/algebra/CLogic/toCProp_rect.con
+cic:/CoRN/algebra/CLogic/toCProp_rec.con
+cic:/CoRN/algebra/CLogic/toCProp_lt.con
+cic:/CoRN/algebra/CLogic/toCProp_ind.con
+cic:/CoRN/algebra/CLogic/toCProp_e.con
+cic:/CoRN/algebra/CLogic/toCProp_Zlt.con
+cic:/CoRN/algebra/CLogic/toCProp.ind
+cic:/CoRN/algebra/CLogic/str_finite_or_elim.con
+cic:/CoRN/algebra/CLogic/sig2T_rect.con
+cic:/CoRN/algebra/CLogic/sig2T_rec.con
+cic:/CoRN/algebra/CLogic/sig2T_ind.con
+cic:/CoRN/algebra/CLogic/sig2T.ind
+cic:/CoRN/algebra/CLogic/proj2b_sig2T.con
+cic:/CoRN/algebra/CLogic/proj2a_sig2T.con
+cic:/CoRN/algebra/CLogic/proj2_sigT.con
+cic:/CoRN/algebra/CLogic/proj1_sigT.con
+cic:/CoRN/algebra/CLogic/proj1_sig2T.con
+cic:/CoRN/algebra/CLogic/pred_lt.con
+cic:/CoRN/algebra/CLogic/plus_pred_pred_plus.con
+cic:/CoRN/algebra/CLogic/plus_eq_one_imp_eq_zero.con
+cic:/CoRN/algebra/CLogic/odd_induction.con
+cic:/CoRN/algebra/CLogic/odd_ind.con
+cic:/CoRN/algebra/CLogic/odd_double_ind.con
+cic:/CoRN/algebra/CLogic/not_r_sum_rec.con
+cic:/CoRN/algebra/CLogic/not_r_cor_rect.con
+cic:/CoRN/algebra/CLogic/not_not_lt.con
+cic:/CoRN/algebra/CLogic/not_l_sum_rec.con
+cic:/CoRN/algebra/CLogic/not_l_cor_rect.con
+cic:/CoRN/algebra/CLogic/nat_nat_pos.con
+cic:/CoRN/algebra/CLogic/nat_mon_imp_mon'.con
+cic:/CoRN/algebra/CLogic/nat_mon_imp_inj.con
+cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon_le.con
+cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon.con
+cic:/CoRN/algebra/CLogic/nat_less_n_pred.con
+cic:/CoRN/algebra/CLogic/nat_less_n_pred'.con
+cic:/CoRN/algebra/CLogic/nat_complete_double_induction.con
+cic:/CoRN/algebra/CLogic/nat_complete_double_ind.con
+cic:/CoRN/algebra/CLogic/my_Cle_ind.con
+cic:/CoRN/algebra/CLogic/mon_fun_covers.con
+cic:/CoRN/algebra/CLogic/member_app.con
+cic:/CoRN/algebra/CLogic/member.con
+cic:/CoRN/algebra/CLogic/lt_pred'.con
+cic:/CoRN/algebra/CLogic/lt_8.con
+cic:/CoRN/algebra/CLogic/lt_5.con
+cic:/CoRN/algebra/CLogic/lt_10.con
+cic:/CoRN/algebra/CLogic/le_2.con
+cic:/CoRN/algebra/CLogic/le_1.con
+cic:/CoRN/algebra/CLogic/kseq_prop.con
+cic:/CoRN/algebra/CLogic/four_induction.con
+cic:/CoRN/algebra/CLogic/four_ind.con
+cic:/CoRN/algebra/CLogic/finite_or_elim.con
+cic:/CoRN/algebra/CLogic/even_plus_n_n.con
+cic:/CoRN/algebra/CLogic/even_or_odd_plus_gt.con
+cic:/CoRN/algebra/CLogic/even_or_odd_plus.con
+cic:/CoRN/algebra/CLogic/even_induction.con
+cic:/CoRN/algebra/CLogic/even_ind.con
+cic:/CoRN/algebra/CLogic/choice.con
+cic:/CoRN/algebra/CLogic/absolu_2.con
+cic:/CoRN/algebra/CLogic/absolu_1.con
+cic:/CoRN/algebra/CLogic/Zsgn_5.con
+cic:/CoRN/algebra/CLogic/Zsgn_4.con
+cic:/CoRN/algebra/CLogic/Zsgn_3.con
+cic:/CoRN/algebra/CLogic/Zsgn_2.con
+cic:/CoRN/algebra/CLogic/Zsgn_1.con
+cic:/CoRN/algebra/CLogic/Zmult_Sm_Sn.con
+cic:/CoRN/algebra/CLogic/Zlts.con
+cic:/CoRN/algebra/CLogic/Zgt_mult_reg_absorb_l.con
+cic:/CoRN/algebra/CLogic/Zgt_mult_conv_absorb_l.con
+cic:/CoRN/algebra/CLogic/ZL9.con
+cic:/CoRN/algebra/CLogic/ZL4'.con
+cic:/CoRN/algebra/CLogic/Ttransitive.con
+cic:/CoRN/algebra/CLogic/Tsymmetric.con
+cic:/CoRN/algebra/CLogic/Trelation.con
+cic:/CoRN/algebra/CLogic/Treflexive.con
+cic:/CoRN/algebra/CLogic/Tequiv.con
+cic:/CoRN/algebra/CLogic/S_predn.con
+cic:/CoRN/algebra/CLogic/Not.con
+cic:/CoRN/algebra/CLogic/Iff_trans.con
+cic:/CoRN/algebra/CLogic/Iff_sym.con
+cic:/CoRN/algebra/CLogic/Iff_right.con
+cic:/CoRN/algebra/CLogic/Iff_refl.con
+cic:/CoRN/algebra/CLogic/Iff_left.con
+cic:/CoRN/algebra/CLogic/Iff_imp_imp.con
+cic:/CoRN/algebra/CLogic/Iff.con
+cic:/CoRN/algebra/CLogic/Ctransitive.con
+cic:/CoRN/algebra/CLogic/Csymmetric.con
+cic:/CoRN/algebra/CLogic/Crelation.con
+cic:/CoRN/algebra/CLogic/Creflexive.con
+cic:/CoRN/algebra/CLogic/Cpred_succ_Z_ind.con
+cic:/CoRN/algebra/CLogic/Codd_to.con
+cic:/CoRN/algebra/CLogic/Codd_rect.con
+cic:/CoRN/algebra/CLogic/Codd_rec.con
+cic:/CoRN/algebra/CLogic/Codd_ind.con
+cic:/CoRN/algebra/CLogic/Codd_even_to.con
+cic:/CoRN/algebra/CLogic/Codd.ind
+cic:/CoRN/algebra/CLogic/Cnats_Z_ind.con
+cic:/CoRN/algebra/CLogic/Cnat_total_order.con
+cic:/CoRN/algebra/CLogic/Cnat_double_ind.con
+cic:/CoRN/algebra/CLogic/Clt_to.con
+cic:/CoRN/algebra/CLogic/Clt_le_weak.con
+cic:/CoRN/algebra/CLogic/Clt.con
+cic:/CoRN/algebra/CLogic/Cle_to.con
+cic:/CoRN/algebra/CLogic/Cle_rect.con
+cic:/CoRN/algebra/CLogic/Cle_rec.con
+cic:/CoRN/algebra/CLogic/Cle_n_S.con
+cic:/CoRN/algebra/CLogic/Cle_le_S_eq.con
+cic:/CoRN/algebra/CLogic/Cle_ind.con
+cic:/CoRN/algebra/CLogic/Cle.ind
+cic:/CoRN/algebra/CLogic/Ceven_to.con
+cic:/CoRN/algebra/CLogic/Ceven_rect.con
+cic:/CoRN/algebra/CLogic/Ceven_rec.con
+cic:/CoRN/algebra/CLogic/Ceven_ind.con
+cic:/CoRN/algebra/CLogic/Cequiv.con
+cic:/CoRN/algebra/CLogic/Cdiff_Z_ind_subproof.con
+cic:/CoRN/algebra/CLogic/Cdiff_Z_ind.con
+cic:/CoRN/algebra/CLogic/Cdecidable.con
+cic:/CoRN/algebra/CLogic/CdeMorgan_ex_all.con
+cic:/CoRN/algebra/CLogic/Ccontrapos'.con
+cic:/CoRN/algebra/CLogic/CZlt_to.con
+cic:/CoRN/algebra/CLogic/CZ_exh.con
+cic:/CoRN/algebra/CLogic/CTrue_rect.con
+cic:/CoRN/algebra/CLogic/CTrue_rec.con
+cic:/CoRN/algebra/CLogic/CTrue_ind.con
+cic:/CoRN/algebra/CLogic/CTrue.ind
+cic:/CoRN/algebra/CLogic/CProp.con
+cic:/CoRN/algebra/CLogic/COr_rect.con
+cic:/CoRN/algebra/CLogic/COr_rec.con
+cic:/CoRN/algebra/CLogic/COr_ind.con
+cic:/CoRN/algebra/CLogic/COr.ind
+cic:/CoRN/algebra/CLogic/CNot_Not_or.con
+cic:/CoRN/algebra/CLogic/CNot.con
+cic:/CoRN/algebra/CLogic/CFalse_rect.con
+cic:/CoRN/algebra/CLogic/CFalse_rec.con
+cic:/CoRN/algebra/CLogic/CFalse_ind.con
+cic:/CoRN/algebra/CLogic/CFalse.ind
+cic:/CoRN/algebra/CLogic/CAnd_rect.con
+cic:/CoRN/algebra/CLogic/CAnd_rec.con
+cic:/CoRN/algebra/CLogic/CAnd_proj2.con
+cic:/CoRN/algebra/CLogic/CAnd_proj1.con
+cic:/CoRN/algebra/CLogic/CAnd_ind.con
+cic:/CoRN/algebra/CLogic/CAnd.ind
+cic:/CoRN/algebra/CModule_Homomorphisms/mh_strext.con
+cic:/CoRN/algebra/CModule_Homomorphisms/mh_pres_zero.con
+cic:/CoRN/algebra/CModule_Homomorphisms/mh_pres_unit.con
+cic:/CoRN/algebra/CModule_Homomorphisms/mh_pres_plus.con
+cic:/CoRN/algebra/CModule_Homomorphisms/mh_pres_mult.con
+cic:/CoRN/algebra/CModule_Homomorphisms/mh_pres_minus.con
+cic:/CoRN/algebra/CModule_Homomorphisms/mh_apzero.con
+cic:/CoRN/algebra/CModule_Homomorphisms/hommap.con
+cic:/CoRN/algebra/CModule_Homomorphisms/hom3.con
+cic:/CoRN/algebra/CModule_Homomorphisms/hom2.con
+cic:/CoRN/algebra/CModule_Homomorphisms/hom1.con
+cic:/CoRN/algebra/CModule_Homomorphisms/fun_pres_unit.con
+cic:/CoRN/algebra/CModule_Homomorphisms/fun_pres_plus.con
+cic:/CoRN/algebra/CModule_Homomorphisms/fun_pres_mult.con
+cic:/CoRN/algebra/CModule_Homomorphisms/ModHom_rect.con
+cic:/CoRN/algebra/CModule_Homomorphisms/ModHom_rec.con
+cic:/CoRN/algebra/CModule_Homomorphisms/ModHom_ind.con
+cic:/CoRN/algebra/CModule_Homomorphisms/ModHom.ind
+cic:/CoRN/algebra/CModules/submod_rect.con
+cic:/CoRN/algebra/CModules/submod_rec.con
+cic:/CoRN/algebra/CModules/submod_is_submod.con
+cic:/CoRN/algebra/CModules/submod_ind.con
+cic:/CoRN/algebra/CModules/submod_as_CSetoid.con
+cic:/CoRN/algebra/CModules/submod.ind
+cic:/CoRN/algebra/CModules/smzero.con
+cic:/CoRN/algebra/CModules/smproof.con
+cic:/CoRN/algebra/CModules/smpred.con
+cic:/CoRN/algebra/CModules/smplus.con
+cic:/CoRN/algebra/CModules/smmult.con
+cic:/CoRN/algebra/CModules/rm_proof.con
+cic:/CoRN/algebra/CModules/rm_pl2.con
+cic:/CoRN/algebra/CModules/rm_pl1.con
+cic:/CoRN/algebra/CModules/rm_one.con
+cic:/CoRN/algebra/CModules/rm_mult.con
+cic:/CoRN/algebra/CModules/rm_mu.con
+cic:/CoRN/algebra/CModules/rm_crr.con
+cic:/CoRN/algebra/CModules/mu_zerox.con
+cic:/CoRN/algebra/CModules/mu_strext.con
+cic:/CoRN/algebra/CModules/mu_plus2.con
+cic:/CoRN/algebra/CModules/mu_plus1.con
+cic:/CoRN/algebra/CModules/mu_one.con
+cic:/CoRN/algebra/CModules/mu_mult.con
+cic:/CoRN/algebra/CModules/mu_minusonex.con
+cic:/CoRN/algebra/CModules/mu_minusax.con
+cic:/CoRN/algebra/CModules/mu_azero.con
+cic:/CoRN/algebra/CModules/mu_axap0_xap0.con
+cic:/CoRN/algebra/CModules/mu_axap0_aap0.con
+cic:/CoRN/algebra/CModules/mu_aminusx.con
+cic:/CoRN/algebra/CModules/mu0help2.con
+cic:/CoRN/algebra/CModules/mu0help.con
+cic:/CoRN/algebra/CModules/is_submod_rect.con
+cic:/CoRN/algebra/CModules/is_submod_rec.con
+cic:/CoRN/algebra/CModules/is_submod_ind.con
+cic:/CoRN/algebra/CModules/is_submod.ind
+cic:/CoRN/algebra/CModules/is_comod_rect.con
+cic:/CoRN/algebra/CModules/is_comod_rec.con
+cic:/CoRN/algebra/CModules/is_comod_ind.con
+cic:/CoRN/algebra/CModules/is_comod.ind
+cic:/CoRN/algebra/CModules/is_RModule_rect.con
+cic:/CoRN/algebra/CModules/is_RModule_rec.con
+cic:/CoRN/algebra/CModules/is_RModule_ind.con
+cic:/CoRN/algebra/CModules/is_RModule.ind
+cic:/CoRN/algebra/CModules/comod_wd.con
+cic:/CoRN/algebra/CModules/comod_rect.con
+cic:/CoRN/algebra/CModules/comod_rec.con
+cic:/CoRN/algebra/CModules/comod_plus.con
+cic:/CoRN/algebra/CModules/comod_nonzero.con
+cic:/CoRN/algebra/CModules/comod_mult.con
+cic:/CoRN/algebra/CModules/comod_is_comod.con
+cic:/CoRN/algebra/CModules/comod_ind.con
+cic:/CoRN/algebra/CModules/comod_as_CSetoid.con
+cic:/CoRN/algebra/CModules/comod_apzero.con
+cic:/CoRN/algebra/CModules/comod.ind
+cic:/CoRN/algebra/CModules/cmproof.con
+cic:/CoRN/algebra/CModules/cmpred.con
+cic:/CoRN/algebra/CModules/cmplus.con
+cic:/CoRN/algebra/CModules/cmmult.con
+cic:/CoRN/algebra/CModules/cmapzero.con
+cic:/CoRN/algebra/CModules/R_is_RModule.con
+cic:/CoRN/algebra/CModules/R_as_RModule.con
+cic:/CoRN/algebra/CModules/RModule_rect.con
+cic:/CoRN/algebra/CModules/RModule_rec.con
+cic:/CoRN/algebra/CModules/RModule_is_RModule.con
+cic:/CoRN/algebra/CModules/RModule_ind.con
+cic:/CoRN/algebra/CModules/RModule.ind
+cic:/matita/dama/bishop_set/le_le_eq.con
+cic:/matita/dama/bishop_set/le_antisymmetric.con
+cic:/matita/dama/bishop_set/eq_trans_.con
+cic:/matita/dama/bishop_set/eq_sym_.con
+cic:/matita/dama/bishop_set/eq_sym.con
+cic:/matita/dama/bishop_set/eq_reflexive.con
+cic:/matita/dama/bishop_set/eq.con
+cic:/matita/dama/bishop_set/bs_symmetric.con
+cic:/matita/dama/bishop_set/bs_cotransitive.con
+cic:/matita/dama/bishop_set/bs_coreflexive.con
+cic:/matita/dama/bishop_set/bs_carr.con
+cic:/matita/dama/bishop_set/bs_apart.con
+cic:/matita/dama/bishop_set/bishop_set_rect.con
+cic:/matita/dama/bishop_set/bishop_set_rec.con
+cic:/matita/dama/bishop_set/bishop_set_of_ordered_set.con
+cic:/matita/dama/bishop_set/bishop_set_ind.con
+cic:/matita/dama/bishop_set/bishop_set.ind
+cic:/matita/dama/bishop_set_rewrite/le_rewr.con
+cic:/matita/dama/bishop_set_rewrite/le_rewl.con
+cic:/matita/dama/bishop_set_rewrite/exc_rewr.con
+cic:/matita/dama/bishop_set_rewrite/exc_rewl.con
+cic:/matita/dama/bishop_set_rewrite/eq_trans.con
+cic:/matita/dama/bishop_set_rewrite/ap_rewr.con
+cic:/matita/dama/bishop_set_rewrite/ap_rewl.con
+cic:/matita/dama/cprop_connectives/transitive.con
+cic:/matita/dama/cprop_connectives/symmetric.con
+cic:/matita/dama/cprop_connectives/reflexive.con
+cic:/matita/dama/cprop_connectives/exT_rect.con
+cic:/matita/dama/cprop_connectives/exT_rec.con
+cic:/matita/dama/cprop_connectives/exT_ind.con
+cic:/matita/dama/cprop_connectives/exT.ind
+cic:/matita/dama/cprop_connectives/cotransitive.con
+cic:/matita/dama/cprop_connectives/coreflexive.con
+cic:/matita/dama/cprop_connectives/antisymmetric.con
+cic:/matita/dama/cprop_connectives/Or_rect.con
+cic:/matita/dama/cprop_connectives/Or_rec.con
+cic:/matita/dama/cprop_connectives/Or_ind.con
+cic:/matita/dama/cprop_connectives/Or.ind
+cic:/matita/dama/cprop_connectives/Not.con
+cic:/matita/dama/cprop_connectives/False_rect.con
+cic:/matita/dama/cprop_connectives/False_rec.con
+cic:/matita/dama/cprop_connectives/False_ind.con
+cic:/matita/dama/cprop_connectives/False.ind
+cic:/matita/dama/cprop_connectives/And_rect.con
+cic:/matita/dama/cprop_connectives/And_rec.con
+cic:/matita/dama/cprop_connectives/And_ind.con
+cic:/matita/dama/cprop_connectives/And.ind
+cic:/matita/dama/ordered_set/os_excess.con
+cic:/matita/dama/ordered_set/os_cotransitive.con
+cic:/matita/dama/ordered_set/os_coreflexive.con
+cic:/matita/dama/ordered_set/os_carr.con
+cic:/matita/dama/ordered_set/ordered_set_rect.con
+cic:/matita/dama/ordered_set/ordered_set_rec.con
+cic:/matita/dama/ordered_set/ordered_set_ind.con
+cic:/matita/dama/ordered_set/ordered_set.ind
+cic:/matita/dama/ordered_set/le_transitive.con
+cic:/matita/dama/ordered_set/le_reflexive.con
+cic:/matita/dama/ordered_set/le.con
+cic:/matita/dama/ordered_set/exc_le_variance.con
+cic:/matita/dama/sequence/sequence.con
+cic:/matita/dama/sequence/fun_of_sequence.con
+cic:/matita/dama/supremum/upper_bound.con
+cic:/matita/dama/supremum/uniq_supremum.con
+cic:/matita/dama/supremum/strong_sup.con
+cic:/matita/dama/supremum/increasing.con
+cic:/matita/higher_order_defs/functions/symmetric2.con
+cic:/matita/higher_order_defs/functions/symmetric.con
+cic:/matita/higher_order_defs/functions/surjective.con
+cic:/matita/higher_order_defs/functions/monotonic.con
+cic:/matita/higher_order_defs/functions/injective.con
+cic:/matita/higher_order_defs/functions/eq_f_g_h.con
+cic:/matita/higher_order_defs/functions/distributive2.con
+cic:/matita/higher_order_defs/functions/distributive.con
+cic:/matita/higher_order_defs/functions/compose.con
+cic:/matita/higher_order_defs/functions/associative.con
+cic:/matita/higher_order_defs/relations/transitive.con
+cic:/matita/higher_order_defs/relations/tight_apart.con
+cic:/matita/higher_order_defs/relations/symmetric.con
+cic:/matita/higher_order_defs/relations/relation.con
+cic:/matita/higher_order_defs/relations/reflexive.con
+cic:/matita/higher_order_defs/relations/irreflexive.con
+cic:/matita/higher_order_defs/relations/cotransitive.con
+cic:/matita/higher_order_defs/relations/antisymmetric.con
+cic:/matita/logic/connectives/proj2.con
+cic:/matita/logic/connectives/proj1.con
+cic:/matita/logic/connectives/iff.con
+cic:/matita/logic/connectives/ex_ind.con
+cic:/matita/logic/connectives/ex2_ind.con
+cic:/matita/logic/connectives/ex2.ind
+cic:/matita/logic/connectives/ex.ind
+cic:/matita/logic/connectives/decidable.con
+cic:/matita/logic/connectives/absurd.con
+cic:/matita/logic/connectives/True_rect.con
+cic:/matita/logic/connectives/True_rec.con
+cic:/matita/logic/connectives/True_ind.con
+cic:/matita/logic/connectives/True.ind
+cic:/matita/logic/connectives/Or_ind.con
+cic:/matita/logic/connectives/Or_ind'.con
+cic:/matita/logic/connectives/Or.ind
+cic:/matita/logic/connectives/Not.con
+cic:/matita/logic/connectives/False_rect.con
+cic:/matita/logic/connectives/False_rec.con
+cic:/matita/logic/connectives/False_ind.con
+cic:/matita/logic/connectives/False.ind
+cic:/matita/logic/connectives/And_rect.con
+cic:/matita/logic/connectives/And_rec.con
+cic:/matita/logic/connectives/And_ind.con
+cic:/matita/logic/connectives/And.ind
+cic:/matita/logic/equality/transitive_eq.con
+cic:/matita/logic/equality/trans_sym_eq.con
+cic:/matita/logic/equality/trans_eq.con
+cic:/matita/logic/equality/symmetric_eq.con
+cic:/matita/logic/equality/sym_eq.con
+cic:/matita/logic/equality/reflexive_eq.con
+cic:/matita/logic/equality/nu_left_inv.con
+cic:/matita/logic/equality/nu_inv.con
+cic:/matita/logic/equality/nu_constant.con
+cic:/matita/logic/equality/nu.con
+cic:/matita/logic/equality/eq_to_eq_to_eq_p_q.con
+cic:/matita/logic/equality/eq_rect.con
+cic:/matita/logic/equality/eq_rect'.con
+cic:/matita/logic/equality/eq_rec.con
+cic:/matita/logic/equality/eq_ind.con
+cic:/matita/logic/equality/eq_f2.con
+cic:/matita/logic/equality/eq_f.con
+cic:/matita/logic/equality/eq_f'.con
+cic:/matita/logic/equality/eq_elim_r.con
+cic:/matita/logic/equality/eq_elim_r'.con
+cic:/matita/logic/equality/eq_elim_r''.con
+cic:/matita/logic/equality/eq_OF_eq2.con
+cic:/matita/logic/equality/eq_OF_eq1.con
+cic:/matita/logic/equality/eq_OF_eq.con
+cic:/matita/logic/equality/eq.ind
+cic:/matita/logic/equality/comp.con
+cic:/matita/nat/nat/pred_Sn.con
+cic:/matita/nat/nat/pred.con
+cic:/matita/nat/nat/not_zero.con
+cic:/matita/nat/nat/not_eq_n_Sn.con
+cic:/matita/nat/nat/not_eq_S.con
+cic:/matita/nat/nat/not_eq_O_S.con
+cic:/matita/nat/nat/nat_rect.con
+cic:/matita/nat/nat/nat_rec.con
+cic:/matita/nat/nat/nat_ind.con
+cic:/matita/nat/nat/nat_elim2.con
+cic:/matita/nat/nat/nat_case1.con
+cic:/matita/nat/nat/nat_case.con
+cic:/matita/nat/nat/nat.ind
+cic:/matita/nat/nat/injective_S.con
+cic:/matita/nat/nat/inj_S.con
+cic:/matita/nat/nat/decidable_eq_nat.con

diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml
index 4f99dd05783aaf1554a0699bb9da1f48c66b89c7..71ba8ddc284720f3ec8bed7fa0ed08c34b41d6d6 100644 (file)
--- a/helm/software/components/ng_kernel/check.ml
+++ b/helm/software/components/ng_kernel/check.ml
@@ -12,8 +12,7 @@
 (* $Id$ *)
 
 let debug = true
-let ignore_exc = true
-let ignore_exc_new_typing = true
+let ignore_exc = false
 let rank_all_dependencies = false
 let trust_environment = false
 
@@ -186,14 +185,7 @@ let _ =
     (fun u ->
        let u= OCic2NCic.nuri_of_ouri u in
       indent := 0;
-      try NCicTypeChecker.typecheck_obj (NCicLibrary.get_obj u)
-      with 
-      | NCicTypeChecker.AssertFailure s
-      | NCicTypeChecker.TypeCheckerFailure s
-      | NCicEnvironment.ObjectNotFound s
-      | NCicEnvironment.BadDependency s as e ->
-         prerr_endline ("######### " ^ Lazy.force s);
-         if not ignore_exc_new_typing then raise e)
+      NCicTypeChecker.typecheck_obj (NCicLibrary.get_obj u))
     alluris;
   let dopo = Unix.gettimeofday () in
   Gc.compact ();

diff --git a/helm/software/components/ng_kernel/test.ma b/helm/software/components/ng_kernel/test.ma
index 36a2d9f722cb7485d43613344acb86caa718cef2..ff017315c685abc8b3b177565e65e8fe9eb93b23 100644 (file)
--- a/helm/software/components/ng_kernel/test.ma
+++ b/helm/software/components/ng_kernel/test.ma
@@ -12,15 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-inductive nat : Set \def
-| O : nat
-| S : nat -> nat.
-
-let rec a m n :=
-match m with
- [ O => n
- | S x => S (a x n)].
+include "nat/plus.ma".
 
+(*
 let rec f n := 
   match n with
   [ O => O
@@ -30,21 +24,21 @@ let rec f n :=
              | S q => 
                   let rec h y := 
                     match y with 
-                    [ O => a (f m) (g q)
+                    [ O => f m + g q
                     | S w => h w]
                   in
                     h q] 
            in 
              g m].
+*)
 
-coinductive conat : Set \def
-| OO : conat
-| OS : conat -> conat.
-
-inductive wrap : Set \def
-| w : conat -> wrap
-| ws : wrap -> wrap.
-
-let corec h (n:nat) \def
-g (ws (w (h n)))
-and g x \def OO.
\ No newline at end of file
+let rec f n := 
+  match n with
+  [ O => O
+  | S m => g m
+  ]
+and g m :=
+ match m with
+  [ O => O
+  | S n => f n
+  ].
\ No newline at end of file