Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (681 entries) |

Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7 entries) |

Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |

Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (35 entries) |

Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |

Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (363 entries) |

Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (100 entries) |

Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |

Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 entries) |

Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (31 entries) |

Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (24 entries) |

Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (92 entries) |

Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |

# Global Index

## A

And [constructor, in PropiL]AndFree [definition, in PropiL]

and_dec [instance, in Base]

app_equi_proper [instance, in Base]

app_incl_proper [instance, in Base]

assn [definition, in PropcL]

## B

Base [library]bent [definition, in PropcL]

bent_iff_unsat [lemma, in PropcL]

bool_eq_dec [instance, in Base]

b2s [definition, in PropiL]

## C

card [definition, in Base]Cardinality [section, in Base]

Cardinality.X [variable, in Base]

card_equi_proper [instance, in Base]

card_or [lemma, in Base]

card_lt [lemma, in Base]

card_equi [lemma, in Base]

card_ex [lemma, in Base]

card_0 [lemma, in Base]

card_cons_rem [lemma, in Base]

card_eq [lemma, in Base]

card_le [lemma, in Base]

card_not_in_rem [lemma, in Base]

card_in_rem [lemma, in Base]

cent [definition, in PropcL]

cent_solved_sat [lemma, in PropcL]

cent_sat [lemma, in PropcL]

cent_weak [lemma, in PropcL]

CharAnd [definition, in PropiL]

CharFal [definition, in PropiL]

CharImp [definition, in PropiL]

CharOr [definition, in PropiL]

clause [definition, in PropiL]

Consistency [definition, in PropiL]

cons_equi_proper [instance, in Base]

cons_incl_proper [instance, in Base]

context [definition, in PropiL]

Cut [definition, in PropiL]

c2f [definition, in PropiL]

## D

dec [definition, in Base]Decidability [section, in PropiL]

Decidability_GK3c.B0 [variable, in PropcL]

Decidability_GK3c.A0 [variable, in PropcL]

Decidability_GK3c [section, in PropcL]

Decidability.A0 [variable, in PropiL]

Decidability.s0 [variable, in PropiL]

decider [definition, in PropcL]

decision [definition, in Base]

dec_prop_iff [lemma, in Base]

dec_DM_impl [lemma, in Base]

dec_DM_and [lemma, in Base]

dec_DN [lemma, in Base]

depth [definition, in PropiL]

disjoint [definition, in Base]

disjoint_app [lemma, in Base]

disjoint_cons [lemma, in Base]

disjoint_nil' [lemma, in Base]

disjoint_nil [lemma, in Base]

disjoint_incl [lemma, in Base]

disjoint_symm [lemma, in Base]

disjoint_forall [lemma, in Base]

DM_exists [lemma, in Base]

DM_or [lemma, in Base]

DNF [definition, in PropcL]

Dupfree [section, in Base]

dupfree [inductive, in Base]

Dupfree [section, in Base]

dupfree [inductive, in Base]

dupfreeC [constructor, in Base]

dupfreeC [constructor, in Base]

dupfreeN [constructor, in Base]

dupfreeN [constructor, in Base]

dupfree_inv [definition, in Base]

dupfree_in_power [lemma, in Base]

dupfree_power [lemma, in Base]

dupfree_undup [lemma, in Base]

dupfree_card [lemma, in Base]

dupfree_dec [lemma, in Base]

dupfree_filter [lemma, in Base]

dupfree_map [lemma, in Base]

dupfree_app [lemma, in Base]

dupfree_cons [lemma, in Base]

dupfree_inv [definition, in Base]

dupfree_in_power [lemma, in Base]

dupfree_power [lemma, in Base]

dupfree_undup [lemma, in Base]

dupfree_card [lemma, in Base]

dupfree_dec [lemma, in Base]

dupfree_filter [lemma, in Base]

dupfree_map [lemma, in Base]

dupfree_app [lemma, in Base]

dupfree_cons [lemma, in Base]

Dupfree.X [variable, in Base]

Dupfree.X [variable, in Base]

## E

EntailmentRelationProperties [section, in PropiL]EntailmentRelationProperties.E [variable, in PropiL]

EntailmentRelationProperties.F [variable, in PropiL]

EntailRelAllProps [definition, in PropiL]

EntailRelAllProps_ext [lemma, in PropiL]

Equi [definition, in PropiL]

Equi [section, in Base]

equi [definition, in Base]

equi_rotate [lemma, in Base]

equi_shift [lemma, in Base]

equi_swap [lemma, in Base]

equi_dup [lemma, in Base]

equi_push [lemma, in Base]

equi_Equivalence [instance, in Base]

Equi.X [variable, in Base]

eval [definition, in PropcL]

## F

Fal [constructor, in PropiL]FalFree [definition, in PropiL]

False_dec [instance, in Base]

FCI [module, in Base]

FCI [module, in Base]

FCI.C [definition, in Base]

FCI.C [definition, in Base]

FCI.closure [lemma, in Base]

FCI.closure [lemma, in Base]

FCI.F [definition, in Base]

FCI.F [definition, in Base]

FCI.FCI [section, in Base]

FCI.FCI [section, in Base]

FCI.FCI.step [variable, in Base]

FCI.FCI.step [variable, in Base]

FCI.FCI.V [variable, in Base]

FCI.FCI.V [variable, in Base]

FCI.FCI.X [variable, in Base]

FCI.FCI.X [variable, in Base]

FCI.fp [lemma, in Base]

FCI.fp [lemma, in Base]

FCI.incl [lemma, in Base]

FCI.incl [lemma, in Base]

FCI.ind [lemma, in Base]

FCI.ind [lemma, in Base]

FCI.it_incl [lemma, in Base]

FCI.it_incl [lemma, in Base]

FCI.pick [lemma, in Base]

FCI.pick [lemma, in Base]

filter [definition, in Base]

FilterComm [section, in Base]

FilterComm.p [variable, in Base]

FilterComm.q [variable, in Base]

FilterComm.X [variable, in Base]

FilterLemmas [section, in Base]

FilterLemmas_pq.q [variable, in Base]

FilterLemmas_pq.p [variable, in Base]

FilterLemmas_pq.X [variable, in Base]

FilterLemmas_pq [section, in Base]

FilterLemmas.p [variable, in Base]

FilterLemmas.X [variable, in Base]

filter_comm [lemma, in Base]

filter_and [lemma, in Base]

filter_pq_eq [lemma, in Base]

filter_pq_mono [lemma, in Base]

filter_fst' [lemma, in Base]

filter_fst [lemma, in Base]

filter_app [lemma, in Base]

filter_id [lemma, in Base]

filter_mono [lemma, in Base]

filter_incl [lemma, in Base]

FK [definition, in PropiL]

form [inductive, in PropiL]

form_eq_dec [instance, in PropiL]

FP [definition, in Base]

FS [definition, in PropiL]

## G

Gamma [definition, in PropiL]Gammac [definition, in PropcL]

gen [inductive, in PropiL]

genA [lemma, in PropiL]

genAL [constructor, in PropiL]

genAR [constructor, in PropiL]

genCW [lemma, in PropiL]

genF [constructor, in PropiL]

genIL [constructor, in PropiL]

genIR [constructor, in PropiL]

genOL [constructor, in PropiL]

genOR1 [constructor, in PropiL]

genOR2 [constructor, in PropiL]

genV [constructor, in PropiL]

genW [lemma, in PropiL]

gen_DN [lemma, in PropiL]

gen_DN' [lemma, in PropiL]

gen_lambda [lemma, in PropiL]

gen_iff_tab [lemma, in PropiL]

gen_tab [lemma, in PropiL]

gen_iff_nd [lemma, in PropiL]

gen_nd [lemma, in PropiL]

gen_NoNVar [lemma, in PropiL]

gen_NoVar [lemma, in PropiL]

gen_EntailRelation [lemma, in PropiL]

gen_subst [lemma, in PropiL]

gen_or [lemma, in PropiL]

gen_and_both [lemma, in PropiL]

gen_and [lemma, in PropiL]

gen_fal [lemma, in PropiL]

gen_imp [lemma, in PropiL]

gen_cons [lemma, in PropiL]

gen_NoFal [lemma, in PropiL]

gen_cut [lemma, in PropiL]

gen_GCut [lemma, in PropiL]

gen_mono [lemma, in PropiL]

gk3c [inductive, in PropcL]

gk3cA [lemma, in PropcL]

gk3cAL [constructor, in PropcL]

gk3cAR [constructor, in PropcL]

gk3cC [constructor, in PropcL]

gk3cCut [definition, in PropcL]

gk3cCutE [lemma, in PropcL]

gk3cCut_iff_ndc [lemma, in PropcL]

gk3cDNL [lemma, in PropcL]

gk3cDNL_iff [lemma, in PropcL]

gk3cDNL_inv [lemma, in PropcL]

gk3cDNL_invCut [lemma, in PropcL]

gk3cDNR [lemma, in PropcL]

gk3cDNR_iff [lemma, in PropcL]

gk3cDNR_inv [lemma, in PropcL]

gk3cDNR_invCut [lemma, in PropcL]

gk3cE [lemma, in PropcL]

gk3cF [constructor, in PropcL]

gk3cFL [lemma, in PropcL]

gk3cFL_iff [lemma, in PropcL]

gk3cFL_inv [lemma, in PropcL]

gk3cFL_invCut [lemma, in PropcL]

gk3cFR [lemma, in PropcL]

gk3cFR_iff [lemma, in PropcL]

gk3cFR_inv [lemma, in PropcL]

gk3cFR_invCut [lemma, in PropcL]

gk3cIL [constructor, in PropcL]

gk3cIR [constructor, in PropcL]

gk3cLC [lemma, in PropcL]

gk3cLW [lemma, in PropcL]

gk3cOL [constructor, in PropcL]

gk3cOR [constructor, in PropcL]

gk3cRC [lemma, in PropcL]

gk3cRW [lemma, in PropcL]

gk3cTF [lemma, in PropcL]

gk3cTF' [lemma, in PropcL]

gk3cW [lemma, in PropcL]

gk3c_iff_sem [lemma, in PropcL]

gk3c_dec_ref [lemma, in PropcL]

gk3c_refute [lemma, in PropcL]

gk3c_bent [lemma, in PropcL]

gk3c_bentG [lemma, in PropcL]

gk3c_dec [lemma, in PropcL]

gk3c_iff_sem [lemma, in PropcL]

gk3c_dec_ref [lemma, in PropcL]

gk3c_refute [lemma, in PropcL]

gk3c_bent [lemma, in PropcL]

gk3c_bentG [lemma, in PropcL]

gk3c_dec [lemma, in PropcL]

gk3c_lambdac [lemma, in PropcL]

gk3c_tab_NegImpFree [lemma, in PropcL]

gk3c_tab_NegImpFreeG [lemma, in PropcL]

gk3c_tab_ImpFreeG [lemma, in PropcL]

gk3c_iff_ndc [lemma, in PropcL]

gk3c_Cut [lemma, in PropcL]

gk3c_GCut [lemma, in PropcL]

gk3c_GCut_Fal [lemma, in PropcL]

gk3c_GCut_Var [lemma, in PropcL]

gk3c_Peirce_Cut [definition, in PropcL]

gk3c_Cut [section, in PropcL]

gk3c_ndc [lemma, in PropcL]

gk3c_ndcG [lemma, in PropcL]

gk3c_NV [lemma, in PropcL]

gk3c_NV' [lemma, in PropcL]

gk3c_con [lemma, in PropcL]

gk3c_NF [lemma, in PropcL]

gk3c_NF1 [lemma, in PropcL]

gk3c_NF' [lemma, in PropcL]

gk3c_emptyR [lemma, in PropcL]

Glivenko [lemma, in PropcL]

Glivenko_refute [lemma, in PropcL]

goal [definition, in PropiL]

goalc [definition, in PropcL]

goalc_eq_dec [instance, in PropcL]

goal_eq_dec [instance, in PropiL]

## H

hil [inductive, in PropiL]hilA [constructor, in PropiL]

hilAI [constructor, in PropiL]

hilAK [lemma, in PropiL]

hilAL [constructor, in PropiL]

hilAR [constructor, in PropiL]

hilAS [lemma, in PropiL]

hilc [inductive, in PropcL]

hilc [inductive, in PropcL]

hilcA [constructor, in PropcL]

hilcA [constructor, in PropcL]

hilcAI [constructor, in PropcL]

hilcAI [constructor, in PropcL]

hilcAK [lemma, in PropcL]

hilcAK [lemma, in PropcL]

hilcAL [constructor, in PropcL]

hilcAL [constructor, in PropcL]

hilcAR [constructor, in PropcL]

hilcAR [constructor, in PropcL]

hilcAS [lemma, in PropcL]

hilcAS [lemma, in PropcL]

hilcD [lemma, in PropcL]

hilcD [lemma, in PropcL]

hilcDN [constructor, in PropcL]

hilcDN [constructor, in PropcL]

hilcI [lemma, in PropcL]

hilcI [lemma, in PropcL]

hilcK [constructor, in PropcL]

hilcK [constructor, in PropcL]

hilcMP [constructor, in PropcL]

hilcMP [constructor, in PropcL]

hilcOE [constructor, in PropcL]

hilcOE [constructor, in PropcL]

hilcOL [constructor, in PropcL]

hilcOL [constructor, in PropcL]

hilcOR [constructor, in PropcL]

hilcOR [constructor, in PropcL]

hilcS [constructor, in PropcL]

hilcS [constructor, in PropcL]

hilc_iff_ndc [lemma, in PropcL]

hilc_ndc [lemma, in PropcL]

hilc_iff_ndc [lemma, in PropcL]

hilc_ndc [lemma, in PropcL]

hilD [lemma, in PropiL]

hilE [constructor, in PropiL]

hilI [lemma, in PropiL]

hilK [constructor, in PropiL]

hilMP [constructor, in PropiL]

hilOE [constructor, in PropiL]

hilOL [constructor, in PropiL]

hilOR [constructor, in PropiL]

hilS [constructor, in PropiL]

hil_iff_nd [lemma, in PropiL]

hil_nd [lemma, in PropiL]

## I

iff_dec [instance, in Base]Imp [constructor, in PropiL]

ImpFree [definition, in PropiL]

ImpFreeA [definition, in PropcL]

impl_dec [instance, in Base]

inclp [definition, in Base]

Inclusion [section, in Base]

Inclusion.X [variable, in Base]

incl_equi_proper [instance, in Base]

incl_preorder [instance, in Base]

incl_app_left [lemma, in Base]

incl_lrcons [lemma, in Base]

incl_rcons [lemma, in Base]

incl_sing [lemma, in Base]

incl_lcons [lemma, in Base]

incl_shift [lemma, in Base]

incl_nil_eq [lemma, in Base]

incl_map [lemma, in Base]

incl_nil [lemma, in Base]

in_rem_iff [lemma, in Base]

in_filter_iff [lemma, in Base]

in_equi_proper [instance, in Base]

in_incl_proper [instance, in Base]

in_cons_neq [lemma, in Base]

in_sing [lemma, in Base]

it [definition, in Base]

Iteration [section, in Base]

Iteration.f [variable, in Base]

Iteration.X [variable, in Base]

it_fp [lemma, in Base]

it_ind [lemma, in Base]

## L

Lambda [definition, in PropiL]Lambdac [definition, in PropcL]

lambdac_gk3c [lemma, in PropcL]

lambdac_gk3c [lemma, in PropcL]

lambdac_ind [lemma, in PropcL]

lambdac_closure [lemma, in PropcL]

lambda_gen [lemma, in PropiL]

lambda_ind [lemma, in PropiL]

lambda_closure [lemma, in PropiL]

list_cc [lemma, in Base]

list_exists_not_incl [lemma, in Base]

list_exists_DM [lemma, in Base]

list_exists_dec [instance, in Base]

list_forall_dec [instance, in Base]

list_sigma_forall [lemma, in Base]

list_in_dec [instance, in Base]

list_eq_dec [instance, in Base]

list_cycle [lemma, in Base]

## M

Membership [section, in Base]Membership.X [variable, in Base]

Monotonicity [definition, in PropiL]

## N

nat_le_dec [instance, in Base]nat_eq_dec [instance, in Base]

nd [inductive, in PropiL]

ndA [constructor, in PropiL]

ndAE [constructor, in PropiL]

ndAI [constructor, in PropiL]

ndc [inductive, in PropcL]

ndcA [constructor, in PropcL]

ndcAE [constructor, in PropcL]

ndcAI [constructor, in PropcL]

ndcC [constructor, in PropcL]

ndcE [lemma, in PropcL]

ndcIE [constructor, in PropcL]

ndcII [constructor, in PropcL]

ndcOE [constructor, in PropcL]

ndcOIL [constructor, in PropcL]

ndcOIR [constructor, in PropcL]

ndcW [lemma, in PropcL]

ndCW [lemma, in PropiL]

ndcW1 [lemma, in PropcL]

ndc_hilc [lemma, in PropcL]

ndc_dec_gk3c [lemma, in PropcL]

ndc_hilc [lemma, in PropcL]

ndc_dec_gk3c [lemma, in PropcL]

ndc_gk3c [lemma, in PropcL]

ndc_gk3cCut [lemma, in PropcL]

ndc_iff_sem [lemma, in PropcL]

ndc_dec_bent [lemma, in PropcL]

ndc_EntailRelation [lemma, in PropcL]

ndc_cons [lemma, in PropcL]

ndc_bent [lemma, in PropcL]

ndc_refute [lemma, in PropcL]

ndc_subst [lemma, in PropcL]

ndc_or [lemma, in PropcL]

ndc_and [lemma, in PropcL]

ndc_fal [lemma, in PropcL]

ndc_imp [lemma, in PropcL]

ndc_cut [lemma, in PropcL]

ndc_mono [lemma, in PropcL]

ndc_refl [lemma, in PropcL]

ndDN [lemma, in PropcL]

ndE [constructor, in PropiL]

ndIE [constructor, in PropiL]

ndII [constructor, in PropiL]

ndOE [constructor, in PropiL]

ndOIL [constructor, in PropiL]

ndOIR [constructor, in PropiL]

ndW [lemma, in PropiL]

nd_ndc_NegImpFree [lemma, in PropcL]

nd_ndc_ImpFree [lemma, in PropcL]

nd_embeds_ndc [lemma, in PropcL]

nd_ndc [lemma, in PropcL]

nd_dec [lemma, in PropiL]

nd_OrARcut [lemma, in PropiL]

nd_OrCut [lemma, in PropiL]

nd_hil [lemma, in PropiL]

nd_onesided [lemma, in PropiL]

nd_EntailRelation [lemma, in PropiL]

nd_cons [lemma, in PropiL]

nd_NoFal [lemma, in PropiL]

nd_gen [lemma, in PropiL]

nd_subst [lemma, in PropiL]

nd_or [lemma, in PropiL]

nd_and [lemma, in PropiL]

nd_fal [lemma, in PropiL]

nd_imp [lemma, in PropiL]

nd_cut [lemma, in PropiL]

nd_mono [lemma, in PropiL]

nd_refl [lemma, in PropiL]

neg [definition, in PropcL]

Neg [constructor, in PropiL]

negative [definition, in PropiL]

neg_incl [lemma, in PropcL]

neg_in [lemma, in PropcL]

Not [definition, in PropiL]

not_in_cons [lemma, in Base]

not_dec [instance, in Base]

## O

Or [constructor, in PropiL]OrAR [definition, in PropiL]

OrAR_mono_nd [lemma, in PropiL]

OrAR_mono [lemma, in PropiL]

OrFree [definition, in PropiL]

or_dec [instance, in Base]

## P

phi [definition, in PropcL]Pos [constructor, in PropiL]

positive [definition, in PropiL]

power [definition, in Base]

power [definition, in Base]

PowerRep [section, in Base]

PowerRep [section, in Base]

PowerRep.X [variable, in Base]

PowerRep.X [variable, in Base]

power_extensional [lemma, in Base]

power_nil [lemma, in Base]

power_incl [lemma, in Base]

power_extensional [lemma, in Base]

power_nil [lemma, in Base]

power_incl [lemma, in Base]

PropcL [library]

PropiL [library]

provider [definition, in PropcL]

## R

rec [inductive, in PropcL]recNA [constructor, in PropcL]

recNF [constructor, in PropcL]

recNI [constructor, in PropcL]

recNil [constructor, in PropcL]

recNO [constructor, in PropcL]

recNV [constructor, in PropcL]

recNV' [constructor, in PropcL]

recPA [constructor, in PropcL]

recPF [constructor, in PropcL]

recPI [constructor, in PropcL]

recPO [constructor, in PropcL]

recPV [constructor, in PropcL]

recPV' [constructor, in PropcL]

Reflexivity [definition, in PropiL]

refutation [lemma, in PropcL]

ref_gk3c [lemma, in PropcL]

ref_gk3c [lemma, in PropcL]

ref_dec [lemma, in PropcL]

ref_iff_unsat [lemma, in PropcL]

ref_ndc [lemma, in PropcL]

ref_unsat [lemma, in PropcL]

ref_sound [projection, in PropcL]

ref_neg_or [projection, in PropcL]

ref_pos_or [projection, in PropcL]

ref_neg_and [projection, in PropcL]

ref_pos_and [projection, in PropcL]

ref_neg_imp [projection, in PropcL]

ref_pos_imp [projection, in PropcL]

ref_clash [projection, in PropcL]

ref_weak [projection, in PropcL]

ref_Fal [projection, in PropcL]

ref_pred [record, in PropcL]

rem [definition, in Base]

Removal [section, in Base]

Removal.X [variable, in Base]

rem_inclr [lemma, in Base]

rem_reorder [lemma, in Base]

rem_id [lemma, in Base]

rem_fst' [lemma, in Base]

rem_fst [lemma, in Base]

rem_comm [lemma, in Base]

rem_equi [lemma, in Base]

rem_app' [lemma, in Base]

rem_app [lemma, in Base]

rem_neq [lemma, in Base]

rem_in [lemma, in Base]

rem_cons' [lemma, in Base]

rem_cons [lemma, in Base]

rem_mono [lemma, in Base]

rem_incl [lemma, in Base]

rem_not_in [lemma, in Base]

rep [definition, in Base]

rep [definition, in Base]

rep_dupfree [lemma, in Base]

rep_idempotent [lemma, in Base]

rep_injective [lemma, in Base]

rep_eq [lemma, in Base]

rep_eq' [lemma, in Base]

rep_mono [lemma, in Base]

rep_equi [lemma, in Base]

rep_in [lemma, in Base]

rep_incl [lemma, in Base]

rep_power [lemma, in Base]

rep_dupfree [lemma, in Base]

rep_idempotent [lemma, in Base]

rep_injective [lemma, in Base]

rep_eq [lemma, in Base]

rep_eq' [lemma, in Base]

rep_mono [lemma, in Base]

rep_equi [lemma, in Base]

rep_in [lemma, in Base]

rep_incl [lemma, in Base]

rep_power [lemma, in Base]

RL [section, in PropcL]

RL.Rho [variable, in PropcL]

RL.rho [variable, in PropcL]

## S

sat [definition, in PropcL]satis [definition, in PropcL]

satis_pos [lemma, in PropcL]

satis_weak [lemma, in PropcL]

satis_in [lemma, in PropcL]

satis_iff [lemma, in PropcL]

satis_neg_or [lemma, in PropcL]

satis_pos_or [lemma, in PropcL]

satis_neg_and [lemma, in PropcL]

satis_pos_and [lemma, in PropcL]

satis_neg_imp [lemma, in PropcL]

satis_pos_imp [lemma, in PropcL]

satis_eval [lemma, in PropcL]

satis_dec [instance, in PropcL]

satis' [definition, in PropcL]

sat_weak [lemma, in PropcL]

scl [definition, in PropiL]

scl_closed [lemma, in PropiL]

scl_incl [lemma, in PropiL]

scl_incl' [lemma, in PropiL]

scl' [definition, in PropiL]

scl'_closed [lemma, in PropiL]

scl'_in [lemma, in PropiL]

sform [inductive, in PropiL]

sform_eq_dec [instance, in PropiL]

sf_closed_cons [lemma, in PropiL]

sf_closed_app [lemma, in PropiL]

sf_closed [definition, in PropiL]

size [definition, in PropiL]

sizeF [definition, in PropiL]

size_recursion [lemma, in Base]

solved [definition, in PropcL]

solved_ref [lemma, in PropcL]

solved_neg_var [lemma, in PropcL]

solved_pos_var [lemma, in PropcL]

solved_nil [lemma, in PropcL]

solved_sat' [lemma, in PropcL]

solved_sat [lemma, in PropcL]

solved_phi [lemma, in PropcL]

ssL [definition, in PropiL]

ssL [section, in PropiL]

ssLb [definition, in PropiL]

ssL_nd_ndc [section, in PropcL]

ssL_idempotent [lemma, in PropiL]

ssL_app [lemma, in PropiL]

ssL_mono [lemma, in PropiL]

ssL_in [lemma, in PropiL]

ssL_correct [lemma, in PropiL]

ssL' [definition, in PropiL]

ssL'_in_ssL2 [lemma, in PropiL]

ssL'_in_ssL [lemma, in PropiL]

ssL'_correct [lemma, in PropiL]

ssL'_in [lemma, in PropiL]

ssL'_self [lemma, in PropiL]

ss_closed_app [lemma, in PropiL]

ss_closed'_mono [lemma, in PropiL]

ss_closed [definition, in PropiL]

ss_closed' [definition, in PropiL]

step [definition, in PropiL]

stepc [definition, in PropcL]

stepc_dec [instance, in PropcL]

step_dec [instance, in PropiL]

subst [definition, in PropiL]

Substitution [definition, in PropiL]

svar [definition, in PropcL]

s2b [definition, in PropiL]

## T

tab [inductive, in PropiL]tabAN [constructor, in PropiL]

tabAP [constructor, in PropiL]

tabC [constructor, in PropiL]

tabCS [lemma, in PropiL]

tabF [constructor, in PropiL]

tabIN [constructor, in PropiL]

tabIP [constructor, in PropiL]

tabLW [lemma, in PropiL]

tabON [constructor, in PropiL]

tabOP [constructor, in PropiL]

tabRW [lemma, in PropiL]

tabW [lemma, in PropiL]

tab_nd [lemma, in PropiL]

tab_ndG [lemma, in PropiL]

tab_gen [lemma, in PropiL]

tab_genG [lemma, in PropiL]

True_dec [instance, in Base]

## U

U [definition, in PropiL]Uc [definition, in PropcL]

Uc_sfc [definition, in PropcL]

undup [definition, in Base]

Undup [section, in Base]

undup [definition, in Base]

Undup [section, in Base]

undup_idempotent [lemma, in Base]

undup_id [lemma, in Base]

undup_equi [lemma, in Base]

undup_incl [lemma, in Base]

undup_id_equi [lemma, in Base]

undup_idempotent [lemma, in Base]

undup_id [lemma, in Base]

undup_equi [lemma, in Base]

undup_incl [lemma, in Base]

undup_id_equi [lemma, in Base]

Undup.X [variable, in Base]

Undup.X [variable, in Base]

uns [definition, in PropiL]

uns_neg [lemma, in PropcL]

uns_neg [lemma, in PropcL]

uns_pos [lemma, in PropiL]

U_sfc [definition, in PropiL]

## V

valid [definition, in PropcL]valid_unsat [lemma, in PropcL]

Var [constructor, in PropiL]

var [definition, in PropiL]

## other

_ === _ [notation, in Base]_ <<= _ [notation, in Base]

_ el _ [notation, in Base]

eq_dec _ [notation, in Base]

+ _ [notation, in PropiL]

- _ [notation, in PropiL]

| _ | [notation, in Base]

# Notation Index

## other

_ === _ [in Base]_ <<= _ [in Base]

_ el _ [in Base]

eq_dec _ [in Base]

+ _ [in PropiL]

- _ [in PropiL]

| _ | [in Base]

# Module Index

## F

FCI [in Base]FCI [in Base]

# Variable Index

## C

Cardinality.X [in Base]## D

Decidability_GK3c.B0 [in PropcL]Decidability_GK3c.A0 [in PropcL]

Decidability.A0 [in PropiL]

Decidability.s0 [in PropiL]

Dupfree.X [in Base]

Dupfree.X [in Base]

## E

EntailmentRelationProperties.E [in PropiL]EntailmentRelationProperties.F [in PropiL]

Equi.X [in Base]

## F

FCI.FCI.step [in Base]FCI.FCI.step [in Base]

FCI.FCI.V [in Base]

FCI.FCI.V [in Base]

FCI.FCI.X [in Base]

FCI.FCI.X [in Base]

FilterComm.p [in Base]

FilterComm.q [in Base]

FilterComm.X [in Base]

FilterLemmas_pq.q [in Base]

FilterLemmas_pq.p [in Base]

FilterLemmas_pq.X [in Base]

FilterLemmas.p [in Base]

FilterLemmas.X [in Base]

## I

Inclusion.X [in Base]Iteration.f [in Base]

Iteration.X [in Base]

## M

Membership.X [in Base]## P

PowerRep.X [in Base]PowerRep.X [in Base]

## R

Removal.X [in Base]RL.Rho [in PropcL]

RL.rho [in PropcL]

## U

Undup.X [in Base]Undup.X [in Base]

# Library Index

## B

Base## P

PropcLPropiL

# Lemma Index

## B

bent_iff_unsat [in PropcL]## C

card_or [in Base]card_lt [in Base]

card_equi [in Base]

card_ex [in Base]

card_0 [in Base]

card_cons_rem [in Base]

card_eq [in Base]

card_le [in Base]

card_not_in_rem [in Base]

card_in_rem [in Base]

cent_solved_sat [in PropcL]

cent_sat [in PropcL]

cent_weak [in PropcL]

## D

dec_prop_iff [in Base]dec_DM_impl [in Base]

dec_DM_and [in Base]

dec_DN [in Base]

disjoint_app [in Base]

disjoint_cons [in Base]

disjoint_nil' [in Base]

disjoint_nil [in Base]

disjoint_incl [in Base]

disjoint_symm [in Base]

disjoint_forall [in Base]

DM_exists [in Base]

DM_or [in Base]

dupfree_in_power [in Base]

dupfree_power [in Base]

dupfree_undup [in Base]

dupfree_card [in Base]

dupfree_dec [in Base]

dupfree_filter [in Base]

dupfree_map [in Base]

dupfree_app [in Base]

dupfree_cons [in Base]

dupfree_in_power [in Base]

dupfree_power [in Base]

dupfree_undup [in Base]

dupfree_card [in Base]

dupfree_dec [in Base]

dupfree_filter [in Base]

dupfree_map [in Base]

dupfree_app [in Base]

dupfree_cons [in Base]

## E

EntailRelAllProps_ext [in PropiL]equi_rotate [in Base]

equi_shift [in Base]

equi_swap [in Base]

equi_dup [in Base]

equi_push [in Base]

## F

FCI.closure [in Base]FCI.closure [in Base]

FCI.fp [in Base]

FCI.fp [in Base]

FCI.incl [in Base]

FCI.incl [in Base]

FCI.ind [in Base]

FCI.ind [in Base]

FCI.it_incl [in Base]

FCI.it_incl [in Base]

FCI.pick [in Base]

FCI.pick [in Base]

filter_comm [in Base]

filter_and [in Base]

filter_pq_eq [in Base]

filter_pq_mono [in Base]

filter_fst' [in Base]

filter_fst [in Base]

filter_app [in Base]

filter_id [in Base]

filter_mono [in Base]

filter_incl [in Base]

## G

genA [in PropiL]genCW [in PropiL]

genW [in PropiL]

gen_DN [in PropiL]

gen_DN' [in PropiL]

gen_lambda [in PropiL]

gen_iff_tab [in PropiL]

gen_tab [in PropiL]

gen_iff_nd [in PropiL]

gen_nd [in PropiL]

gen_NoNVar [in PropiL]

gen_NoVar [in PropiL]

gen_EntailRelation [in PropiL]

gen_subst [in PropiL]

gen_or [in PropiL]

gen_and_both [in PropiL]

gen_and [in PropiL]

gen_fal [in PropiL]

gen_imp [in PropiL]

gen_cons [in PropiL]

gen_NoFal [in PropiL]

gen_cut [in PropiL]

gen_GCut [in PropiL]

gen_mono [in PropiL]

gk3cA [in PropcL]

gk3cCutE [in PropcL]

gk3cCut_iff_ndc [in PropcL]

gk3cDNL [in PropcL]

gk3cDNL_iff [in PropcL]

gk3cDNL_inv [in PropcL]

gk3cDNL_invCut [in PropcL]

gk3cDNR [in PropcL]

gk3cDNR_iff [in PropcL]

gk3cDNR_inv [in PropcL]

gk3cDNR_invCut [in PropcL]

gk3cE [in PropcL]

gk3cFL [in PropcL]

gk3cFL_iff [in PropcL]

gk3cFL_inv [in PropcL]

gk3cFL_invCut [in PropcL]

gk3cFR [in PropcL]

gk3cFR_iff [in PropcL]

gk3cFR_inv [in PropcL]

gk3cFR_invCut [in PropcL]

gk3cLC [in PropcL]

gk3cLW [in PropcL]

gk3cRC [in PropcL]

gk3cRW [in PropcL]

gk3cTF [in PropcL]

gk3cTF' [in PropcL]

gk3cW [in PropcL]

gk3c_iff_sem [in PropcL]

gk3c_dec_ref [in PropcL]

gk3c_refute [in PropcL]

gk3c_bent [in PropcL]

gk3c_bentG [in PropcL]

gk3c_dec [in PropcL]

gk3c_iff_sem [in PropcL]

gk3c_dec_ref [in PropcL]

gk3c_refute [in PropcL]

gk3c_bent [in PropcL]

gk3c_bentG [in PropcL]

gk3c_dec [in PropcL]

gk3c_lambdac [in PropcL]

gk3c_tab_NegImpFree [in PropcL]

gk3c_tab_NegImpFreeG [in PropcL]

gk3c_tab_ImpFreeG [in PropcL]

gk3c_iff_ndc [in PropcL]

gk3c_Cut [in PropcL]

gk3c_GCut [in PropcL]

gk3c_GCut_Fal [in PropcL]

gk3c_GCut_Var [in PropcL]

gk3c_ndc [in PropcL]

gk3c_ndcG [in PropcL]

gk3c_NV [in PropcL]

gk3c_NV' [in PropcL]

gk3c_con [in PropcL]

gk3c_NF [in PropcL]

gk3c_NF1 [in PropcL]

gk3c_NF' [in PropcL]

gk3c_emptyR [in PropcL]

Glivenko [in PropcL]

Glivenko_refute [in PropcL]

## H

hilAK [in PropiL]hilAS [in PropiL]

hilcAK [in PropcL]

hilcAK [in PropcL]

hilcAS [in PropcL]

hilcAS [in PropcL]

hilcD [in PropcL]

hilcD [in PropcL]

hilcI [in PropcL]

hilcI [in PropcL]

hilc_iff_ndc [in PropcL]

hilc_ndc [in PropcL]

hilc_iff_ndc [in PropcL]

hilc_ndc [in PropcL]

hilD [in PropiL]

hilI [in PropiL]

hil_iff_nd [in PropiL]

hil_nd [in PropiL]

## I

incl_app_left [in Base]incl_lrcons [in Base]

incl_rcons [in Base]

incl_sing [in Base]

incl_lcons [in Base]

incl_shift [in Base]

incl_nil_eq [in Base]

incl_map [in Base]

incl_nil [in Base]

in_rem_iff [in Base]

in_filter_iff [in Base]

in_cons_neq [in Base]

in_sing [in Base]

it_fp [in Base]

it_ind [in Base]

## L

lambdac_gk3c [in PropcL]lambdac_gk3c [in PropcL]

lambdac_ind [in PropcL]

lambdac_closure [in PropcL]

lambda_gen [in PropiL]

lambda_ind [in PropiL]

lambda_closure [in PropiL]

list_cc [in Base]

list_exists_not_incl [in Base]

list_exists_DM [in Base]

list_sigma_forall [in Base]

list_cycle [in Base]

## N

ndcE [in PropcL]ndcW [in PropcL]

ndCW [in PropiL]

ndcW1 [in PropcL]

ndc_hilc [in PropcL]

ndc_dec_gk3c [in PropcL]

ndc_hilc [in PropcL]

ndc_dec_gk3c [in PropcL]

ndc_gk3c [in PropcL]

ndc_gk3cCut [in PropcL]

ndc_iff_sem [in PropcL]

ndc_dec_bent [in PropcL]

ndc_EntailRelation [in PropcL]

ndc_cons [in PropcL]

ndc_bent [in PropcL]

ndc_refute [in PropcL]

ndc_subst [in PropcL]

ndc_or [in PropcL]

ndc_and [in PropcL]

ndc_fal [in PropcL]

ndc_imp [in PropcL]

ndc_cut [in PropcL]

ndc_mono [in PropcL]

ndc_refl [in PropcL]

ndDN [in PropcL]

ndW [in PropiL]

nd_ndc_NegImpFree [in PropcL]

nd_ndc_ImpFree [in PropcL]

nd_embeds_ndc [in PropcL]

nd_ndc [in PropcL]

nd_dec [in PropiL]

nd_OrARcut [in PropiL]

nd_OrCut [in PropiL]

nd_hil [in PropiL]

nd_onesided [in PropiL]

nd_EntailRelation [in PropiL]

nd_cons [in PropiL]

nd_NoFal [in PropiL]

nd_gen [in PropiL]

nd_subst [in PropiL]

nd_or [in PropiL]

nd_and [in PropiL]

nd_fal [in PropiL]

nd_imp [in PropiL]

nd_cut [in PropiL]

nd_mono [in PropiL]

nd_refl [in PropiL]

neg_incl [in PropcL]

neg_in [in PropcL]

not_in_cons [in Base]

## O

OrAR_mono_nd [in PropiL]OrAR_mono [in PropiL]

## P

power_extensional [in Base]power_nil [in Base]

power_incl [in Base]

power_extensional [in Base]

power_nil [in Base]

power_incl [in Base]

## R

refutation [in PropcL]ref_gk3c [in PropcL]

ref_gk3c [in PropcL]

ref_dec [in PropcL]

ref_iff_unsat [in PropcL]

ref_ndc [in PropcL]

ref_unsat [in PropcL]

rem_inclr [in Base]

rem_reorder [in Base]

rem_id [in Base]

rem_fst' [in Base]

rem_fst [in Base]

rem_comm [in Base]

rem_equi [in Base]

rem_app' [in Base]

rem_app [in Base]

rem_neq [in Base]

rem_in [in Base]

rem_cons' [in Base]

rem_cons [in Base]

rem_mono [in Base]

rem_incl [in Base]

rem_not_in [in Base]

rep_dupfree [in Base]

rep_idempotent [in Base]

rep_injective [in Base]

rep_eq [in Base]

rep_eq' [in Base]

rep_mono [in Base]

rep_equi [in Base]

rep_in [in Base]

rep_incl [in Base]

rep_power [in Base]

rep_dupfree [in Base]

rep_idempotent [in Base]

rep_injective [in Base]

rep_eq [in Base]

rep_eq' [in Base]

rep_mono [in Base]

rep_equi [in Base]

rep_in [in Base]

rep_incl [in Base]

rep_power [in Base]

## S

satis_pos [in PropcL]satis_weak [in PropcL]

satis_in [in PropcL]

satis_iff [in PropcL]

satis_neg_or [in PropcL]

satis_pos_or [in PropcL]

satis_neg_and [in PropcL]

satis_pos_and [in PropcL]

satis_neg_imp [in PropcL]

satis_pos_imp [in PropcL]

satis_eval [in PropcL]

sat_weak [in PropcL]

scl_closed [in PropiL]

scl_incl [in PropiL]

scl_incl' [in PropiL]

scl'_closed [in PropiL]

scl'_in [in PropiL]

sf_closed_cons [in PropiL]

sf_closed_app [in PropiL]

size_recursion [in Base]

solved_ref [in PropcL]

solved_neg_var [in PropcL]

solved_pos_var [in PropcL]

solved_nil [in PropcL]

solved_sat' [in PropcL]

solved_sat [in PropcL]

solved_phi [in PropcL]

ssL_idempotent [in PropiL]

ssL_app [in PropiL]

ssL_mono [in PropiL]

ssL_in [in PropiL]

ssL_correct [in PropiL]

ssL'_in_ssL2 [in PropiL]

ssL'_in_ssL [in PropiL]

ssL'_correct [in PropiL]

ssL'_in [in PropiL]

ssL'_self [in PropiL]

ss_closed_app [in PropiL]

ss_closed'_mono [in PropiL]

## T

tabCS [in PropiL]tabLW [in PropiL]

tabRW [in PropiL]

tabW [in PropiL]

tab_nd [in PropiL]

tab_ndG [in PropiL]

tab_gen [in PropiL]

tab_genG [in PropiL]

## U

undup_idempotent [in Base]undup_id [in Base]

undup_equi [in Base]

undup_incl [in Base]

undup_id_equi [in Base]

undup_idempotent [in Base]

undup_id [in Base]

undup_equi [in Base]

undup_incl [in Base]

undup_id_equi [in Base]

uns_neg [in PropcL]

uns_neg [in PropcL]

uns_pos [in PropiL]

## V

valid_unsat [in PropcL]# Constructor Index

## A

And [in PropiL]## D

dupfreeC [in Base]dupfreeC [in Base]

dupfreeN [in Base]

dupfreeN [in Base]

## F

Fal [in PropiL]## G

genAL [in PropiL]genAR [in PropiL]

genF [in PropiL]

genIL [in PropiL]

genIR [in PropiL]

genOL [in PropiL]

genOR1 [in PropiL]

genOR2 [in PropiL]

genV [in PropiL]

gk3cAL [in PropcL]

gk3cAR [in PropcL]

gk3cC [in PropcL]

gk3cF [in PropcL]

gk3cIL [in PropcL]

gk3cIR [in PropcL]

gk3cOL [in PropcL]

gk3cOR [in PropcL]

## H

hilA [in PropiL]hilAI [in PropiL]

hilAL [in PropiL]

hilAR [in PropiL]

hilcA [in PropcL]

hilcA [in PropcL]

hilcAI [in PropcL]

hilcAI [in PropcL]

hilcAL [in PropcL]

hilcAL [in PropcL]

hilcAR [in PropcL]

hilcAR [in PropcL]

hilcDN [in PropcL]

hilcDN [in PropcL]

hilcK [in PropcL]

hilcK [in PropcL]

hilcMP [in PropcL]

hilcMP [in PropcL]

hilcOE [in PropcL]

hilcOE [in PropcL]

hilcOL [in PropcL]

hilcOL [in PropcL]

hilcOR [in PropcL]

hilcOR [in PropcL]

hilcS [in PropcL]

hilcS [in PropcL]

hilE [in PropiL]

hilK [in PropiL]

hilMP [in PropiL]

hilOE [in PropiL]

hilOL [in PropiL]

hilOR [in PropiL]

hilS [in PropiL]

## I

Imp [in PropiL]## N

ndA [in PropiL]ndAE [in PropiL]

ndAI [in PropiL]

ndcA [in PropcL]

ndcAE [in PropcL]

ndcAI [in PropcL]

ndcC [in PropcL]

ndcIE [in PropcL]

ndcII [in PropcL]

ndcOE [in PropcL]

ndcOIL [in PropcL]

ndcOIR [in PropcL]

ndE [in PropiL]

ndIE [in PropiL]

ndII [in PropiL]

ndOE [in PropiL]

ndOIL [in PropiL]

ndOIR [in PropiL]

Neg [in PropiL]

## O

Or [in PropiL]## P

Pos [in PropiL]## R

recNA [in PropcL]recNF [in PropcL]

recNI [in PropcL]

recNil [in PropcL]

recNO [in PropcL]

recNV [in PropcL]

recNV' [in PropcL]

recPA [in PropcL]

recPF [in PropcL]

recPI [in PropcL]

recPO [in PropcL]

recPV [in PropcL]

recPV' [in PropcL]

## T

tabAN [in PropiL]tabAP [in PropiL]

tabC [in PropiL]

tabF [in PropiL]

tabIN [in PropiL]

tabIP [in PropiL]

tabON [in PropiL]

tabOP [in PropiL]

## V

Var [in PropiL]# Inductive Index

## D

dupfree [in Base]dupfree [in Base]

## F

form [in PropiL]## G

gen [in PropiL]gk3c [in PropcL]

## H

hil [in PropiL]hilc [in PropcL]

hilc [in PropcL]

## N

nd [in PropiL]ndc [in PropcL]

## R

rec [in PropcL]## S

sform [in PropiL]## T

tab [in PropiL]# Projection Index

## R

ref_sound [in PropcL]ref_neg_or [in PropcL]

ref_pos_or [in PropcL]

ref_neg_and [in PropcL]

ref_pos_and [in PropcL]

ref_neg_imp [in PropcL]

ref_pos_imp [in PropcL]

ref_clash [in PropcL]

ref_weak [in PropcL]

ref_Fal [in PropcL]

# Instance Index

## A

and_dec [in Base]app_equi_proper [in Base]

app_incl_proper [in Base]

## B

bool_eq_dec [in Base]## C

card_equi_proper [in Base]cons_equi_proper [in Base]

cons_incl_proper [in Base]

## E

equi_Equivalence [in Base]## F

False_dec [in Base]form_eq_dec [in PropiL]

## G

goalc_eq_dec [in PropcL]goal_eq_dec [in PropiL]

## I

iff_dec [in Base]impl_dec [in Base]

incl_equi_proper [in Base]

incl_preorder [in Base]

in_equi_proper [in Base]

in_incl_proper [in Base]

## L

list_exists_dec [in Base]list_forall_dec [in Base]

list_in_dec [in Base]

list_eq_dec [in Base]

## N

nat_le_dec [in Base]nat_eq_dec [in Base]

not_dec [in Base]

## O

or_dec [in Base]## S

satis_dec [in PropcL]sform_eq_dec [in PropiL]

stepc_dec [in PropcL]

step_dec [in PropiL]

## T

True_dec [in Base]# Section Index

## C

Cardinality [in Base]## D

Decidability [in PropiL]Decidability_GK3c [in PropcL]

Dupfree [in Base]

Dupfree [in Base]

## E

EntailmentRelationProperties [in PropiL]Equi [in Base]

## F

FCI.FCI [in Base]FCI.FCI [in Base]

FilterComm [in Base]

FilterLemmas [in Base]

FilterLemmas_pq [in Base]

## G

gk3c_Cut [in PropcL]## I

Inclusion [in Base]Iteration [in Base]

## M

Membership [in Base]## P

PowerRep [in Base]PowerRep [in Base]

## R

Removal [in Base]RL [in PropcL]

## S

ssL [in PropiL]ssL_nd_ndc [in PropcL]

## U

Undup [in Base]Undup [in Base]

# Definition Index

## A

AndFree [in PropiL]assn [in PropcL]

## B

bent [in PropcL]b2s [in PropiL]

## C

card [in Base]cent [in PropcL]

CharAnd [in PropiL]

CharFal [in PropiL]

CharImp [in PropiL]

CharOr [in PropiL]

clause [in PropiL]

Consistency [in PropiL]

context [in PropiL]

Cut [in PropiL]

c2f [in PropiL]

## D

dec [in Base]decider [in PropcL]

decision [in Base]

depth [in PropiL]

disjoint [in Base]

DNF [in PropcL]

dupfree_inv [in Base]

dupfree_inv [in Base]

## E

EntailRelAllProps [in PropiL]Equi [in PropiL]

equi [in Base]

eval [in PropcL]

## F

FalFree [in PropiL]FCI.C [in Base]

FCI.C [in Base]

FCI.F [in Base]

FCI.F [in Base]

filter [in Base]

FK [in PropiL]

FP [in Base]

FS [in PropiL]

## G

Gamma [in PropiL]Gammac [in PropcL]

gk3cCut [in PropcL]

gk3c_Peirce_Cut [in PropcL]

goal [in PropiL]

goalc [in PropcL]

## I

ImpFree [in PropiL]ImpFreeA [in PropcL]

inclp [in Base]

it [in Base]

## L

Lambda [in PropiL]Lambdac [in PropcL]

## M

Monotonicity [in PropiL]## N

neg [in PropcL]negative [in PropiL]

Not [in PropiL]

## O

OrAR [in PropiL]OrFree [in PropiL]

## P

phi [in PropcL]positive [in PropiL]

power [in Base]

power [in Base]

provider [in PropcL]

## R

Reflexivity [in PropiL]rem [in Base]

rep [in Base]

rep [in Base]

## S

sat [in PropcL]satis [in PropcL]

satis' [in PropcL]

scl [in PropiL]

scl' [in PropiL]

sf_closed [in PropiL]

size [in PropiL]

sizeF [in PropiL]

solved [in PropcL]

ssL [in PropiL]

ssLb [in PropiL]

ssL' [in PropiL]

ss_closed [in PropiL]

ss_closed' [in PropiL]

step [in PropiL]

stepc [in PropcL]

subst [in PropiL]

Substitution [in PropiL]

svar [in PropcL]

s2b [in PropiL]

## U

U [in PropiL]Uc [in PropcL]

Uc_sfc [in PropcL]

undup [in Base]

undup [in Base]

uns [in PropiL]

U_sfc [in PropiL]

## V

valid [in PropcL]var [in PropiL]

# Record Index

## R

ref_pred [in PropcL]Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (681 entries) |

Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7 entries) |

Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |

Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (35 entries) |

Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |

Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (363 entries) |

Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (100 entries) |

Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |

Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 entries) |

Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (31 entries) |

Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (24 entries) |

Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (92 entries) |

Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |

This page has been generated by coqdoc