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 | (362 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 | (5 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 | (1 entry) |

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 | (40 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 | (148 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 | (30 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 | (7 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 | (25 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 | (20 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 | (26 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 | (55 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 | (2 entries) |

# Global Index

## A

andlist [definition, in PropL]andlistEq [lemma, in PropL]

and_dec [instance, in Base]

app_equi_proper [instance, in Base]

app_incl_proper [instance, in Base]

assn [definition, in PropL]

## B

Base [library]bool_eq_dec [instance, in Base]

bot [projection, in HeytingAndKripke]

bot1 [projection, in HeytingAndKripke]

bsc [definition, in PropL]

## 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]

CharFal [definition, in PropL]

CharImp [definition, in PropL]

Consistency [definition, in PropL]

cons_equi_proper [instance, in Base]

cons_incl_proper [instance, in Base]

context [definition, in PropL]

Cut [definition, in PropL]

## D

dec [definition, in Base]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]

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]

Dupfree [section, in Base]

dupfree [inductive, in Base]

dupfreeC [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.X [variable, in Base]

## E

EntailRelAllProps [definition, in PropL]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]

evalH [definition, in HeytingAndKripke]

evalH_evalK_agree [lemma, in HeytingAndKripke]

evalH' [definition, in HeytingAndKripke]

evalK [definition, in HeytingAndKripke]

evalK_evalH_agree [lemma, in HeytingAndKripke]

evalK' [definition, in HeytingAndKripke]

## F

F [section, in PropL]Fal [constructor, in PropL]

False_dec [instance, in Base]

FCI [module, in Base]

FCI.C [definition, in Base]

FCI.closure [lemma, in Base]

FCI.F [definition, in Base]

FCI.FCI [section, in Base]

FCI.FCI.step [variable, in Base]

FCI.FCI.V [variable, in Base]

FCI.FCI.X [variable, in Base]

FCI.fp [lemma, in Base]

FCI.incl [lemma, in Base]

FCI.ind [lemma, in Base]

FCI.it_incl [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 PropL]

form [inductive, in PropL]

form_eq_dec [instance, in PropL]

FP [definition, in Base]

FS [definition, in PropL]

F.E [variable, in PropL]

F.F [variable, in PropL]

## G

Glivenko [lemma, in PropL]Glivenko_refute [lemma, in PropL]

## H

H [projection, in HeytingAndKripke]Ha5 [inductive, in HeytingAndKripke]

Ha5a [constructor, in HeytingAndKripke]

Ha5ab [constructor, in HeytingAndKripke]

Ha5b [constructor, in HeytingAndKripke]

Ha5bot [constructor, in HeytingAndKripke]

Ha5HA [definition, in HeytingAndKripke]

Ha5imp [definition, in HeytingAndKripke]

Ha5interp [definition, in HeytingAndKripke]

Ha5join [definition, in HeytingAndKripke]

Ha5meet [definition, in HeytingAndKripke]

Ha5R [definition, in HeytingAndKripke]

Ha5Rref [lemma, in HeytingAndKripke]

Ha5Rtra [lemma, in HeytingAndKripke]

Ha5top [constructor, in HeytingAndKripke]

Hb5 [inductive, in HeytingAndKripke]

Hb5a [constructor, in HeytingAndKripke]

Hb5ab [constructor, in HeytingAndKripke]

Hb5b [constructor, in HeytingAndKripke]

Hb5bot [constructor, in HeytingAndKripke]

Hb5HA [definition, in HeytingAndKripke]

Hb5imp [definition, in HeytingAndKripke]

Hb5interp [definition, in HeytingAndKripke]

Hb5join [definition, in HeytingAndKripke]

Hb5meet [definition, in HeytingAndKripke]

Hb5R [definition, in HeytingAndKripke]

Hb5Rref [lemma, in HeytingAndKripke]

Hb5Rtra [lemma, in HeytingAndKripke]

Hb5top [constructor, in HeytingAndKripke]

HeytingAlgebra [section, in HeytingAndKripke]

HeytingAlgebra [record, in HeytingAndKripke]

HeytingAlgebraOfKripkeModel [definition, in HeytingAndKripke]

HeytingAlgebraToKripkeModel [section, in HeytingAndKripke]

HeytingAlgebraToKripkeModel.A [variable, in HeytingAndKripke]

HeytingAlgebraToKripkeModel.interp [variable, in HeytingAndKripke]

HeytingAlgebraToKripkeModel.xm [variable, in HeytingAndKripke]

HeytingAlgebra.HA [variable, in HeytingAndKripke]

HeytingAlgebra.interp [variable, in HeytingAndKripke]

HeytingAndKripke [library]

HeytingHa5 [section, in HeytingAndKripke]

HeytingHa5.Ha5eval [variable, in HeytingAndKripke]

HeytingHb5 [section, in HeytingAndKripke]

HeytingHb5.Hb5eval [variable, in HeytingAndKripke]

HeytingInterpOfKripkeModel [definition, in HeytingAndKripke]

hil [inductive, in PropL]

hilA [constructor, in PropL]

hilAK [lemma, in PropL]

hilAS [lemma, in PropL]

hilD [lemma, in PropL]

hilE [constructor, in PropL]

hilI [lemma, in PropL]

hilK [constructor, in PropL]

hilMP [constructor, in PropL]

hilS [constructor, in PropL]

hil_iff_nd [lemma, in PropL]

hil_nd [lemma, in PropL]

## I

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

imp [projection, in HeytingAndKripke]

impl_dec [instance, in Base]

imp1 [projection, in HeytingAndKripke]

imp2 [projection, in HeytingAndKripke]

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]

## J

join [projection, in HeytingAndKripke]join1 [projection, in HeytingAndKripke]

join2 [projection, in HeytingAndKripke]

join3 [projection, in HeytingAndKripke]

## K

KripkeModel [section, in HeytingAndKripke]KripkeModel [record, in HeytingAndKripke]

KripkeModelOfHeytingAlgebra [definition, in HeytingAndKripke]

KripkeModelToHeytingAlgebra [section, in HeytingAndKripke]

KripkeModelToHeytingAlgebra.bot [variable, in HeytingAndKripke]

KripkeModelToHeytingAlgebra.Cl [variable, in HeytingAndKripke]

KripkeModelToHeytingAlgebra.H [variable, in HeytingAndKripke]

KripkeModelToHeytingAlgebra.imp [variable, in HeytingAndKripke]

KripkeModelToHeytingAlgebra.join [variable, in HeytingAndKripke]

KripkeModelToHeytingAlgebra.M [variable, in HeytingAndKripke]

KripkeModelToHeytingAlgebra.meet [variable, in HeytingAndKripke]

KripkeModelToHeytingAlgebra.R [variable, in HeytingAndKripke]

KripkeModelToHeytingAlgebra.top [variable, in HeytingAndKripke]

KripkeModel.M [variable, in HeytingAndKripke]

## L

label [projection, in HeytingAndKripke]label_mon [projection, in HeytingAndKripke]

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

meet [projection, in HeytingAndKripke]meet1 [projection, in HeytingAndKripke]

meet2 [projection, in HeytingAndKripke]

meet3 [projection, in HeytingAndKripke]

Membership [section, in Base]

Membership.X [variable, in Base]

mkHeytingAlgebra [constructor, in HeytingAndKripke]

mkKripkeModel [constructor, in HeytingAndKripke]

monotone [lemma, in HeytingAndKripke]

monotone_ctx [lemma, in HeytingAndKripke]

Monotonicity [definition, in PropL]

## N

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

nd [inductive, in PropL]

ndA [constructor, in PropL]

ndapp [lemma, in PropL]

ndapp1 [lemma, in PropL]

ndapp2 [lemma, in PropL]

ndapp3 [lemma, in PropL]

ndc [inductive, in PropL]

ndcA [constructor, in PropL]

ndcC [constructor, in PropL]

ndcE [lemma, in PropL]

ndcIE [constructor, in PropL]

ndcII [constructor, in PropL]

ndcW [lemma, in PropL]

ndc_refute [lemma, in PropL]

ndc_weak [lemma, in PropL]

ndDN [lemma, in PropL]

ndE [constructor, in PropL]

ndIE [constructor, in PropL]

ndIE_weak [lemma, in PropL]

ndII [constructor, in PropL]

ndW [lemma, in PropL]

nd_hil [lemma, in PropL]

nd_embeds_ndc [lemma, in PropL]

nd_ndc [lemma, in PropL]

nd_subst [lemma, in PropL]

nd_con [lemma, in PropL]

nd_bool_sound [lemma, in PropL]

nd_weak [lemma, in PropL]

nd_soundK [lemma, in HeytingAndKripke]

nd_soundH [lemma, in HeytingAndKripke]

Not [definition, in PropL]

not_in_cons [lemma, in Base]

not_dec [instance, in Base]

## O

or_dec [instance, in Base]## P

power [definition, in Base]PowerRep [section, in Base]

PowerRep.X [variable, in Base]

power_extensional [lemma, in Base]

power_nil [lemma, in Base]

power_incl [lemma, in Base]

ProperFilter [definition, in HeytingAndKripke]

PropL [library]

## R

R [projection, in HeytingAndKripke]Reflexivity [definition, in PropL]

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_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]

Rref [projection, in HeytingAndKripke]

Rtra [projection, in HeytingAndKripke]

## S

satis [definition, in PropL]satis_dec [instance, in PropL]

size_recursion [lemma, in Base]

state [projection, in HeytingAndKripke]

step [projection, in HeytingAndKripke]

step_trans [projection, in HeytingAndKripke]

step_refl [projection, in HeytingAndKripke]

subst [definition, in PropL]

Substitution [definition, in PropL]

## T

top [projection, in HeytingAndKripke]top1 [projection, in HeytingAndKripke]

True_dec [instance, in Base]

## U

undef_a_Or_b [lemma, in HeytingAndKripke]undef_a_And_b [lemma, in HeytingAndKripke]

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.X [variable, in Base]

## V

Var [constructor, in PropL]var [definition, in PropL]

vars [definition, in PropL]

## other

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

_ el _ [notation, in Base]

eq_dec _ [notation, in Base]

| _ | [notation, in Base]

# Notation Index

## other

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

_ el _ [in Base]

eq_dec _ [in Base]

| _ | [in Base]

# Module Index

## F

FCI [in Base]# Variable Index

## C

Cardinality.X [in Base]## D

Dupfree.X [in Base]## E

Equi.X [in Base]## F

FCI.FCI.step [in Base]FCI.FCI.V [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]

F.E [in PropL]

F.F [in PropL]

## H

HeytingAlgebraToKripkeModel.A [in HeytingAndKripke]HeytingAlgebraToKripkeModel.interp [in HeytingAndKripke]

HeytingAlgebraToKripkeModel.xm [in HeytingAndKripke]

HeytingAlgebra.HA [in HeytingAndKripke]

HeytingAlgebra.interp [in HeytingAndKripke]

HeytingHa5.Ha5eval [in HeytingAndKripke]

HeytingHb5.Hb5eval [in HeytingAndKripke]

## I

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

Iteration.X [in Base]

## K

KripkeModelToHeytingAlgebra.bot [in HeytingAndKripke]KripkeModelToHeytingAlgebra.Cl [in HeytingAndKripke]

KripkeModelToHeytingAlgebra.H [in HeytingAndKripke]

KripkeModelToHeytingAlgebra.imp [in HeytingAndKripke]

KripkeModelToHeytingAlgebra.join [in HeytingAndKripke]

KripkeModelToHeytingAlgebra.M [in HeytingAndKripke]

KripkeModelToHeytingAlgebra.meet [in HeytingAndKripke]

KripkeModelToHeytingAlgebra.R [in HeytingAndKripke]

KripkeModelToHeytingAlgebra.top [in HeytingAndKripke]

KripkeModel.M [in HeytingAndKripke]

## M

Membership.X [in Base]## P

PowerRep.X [in Base]## R

Removal.X [in Base]## U

Undup.X [in Base]# Library Index

## B

Base## H

HeytingAndKripke## P

PropL# Lemma Index

## A

andlistEq [in PropL]## 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]

## 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]

## E

equi_rotate [in Base]equi_shift [in Base]

equi_swap [in Base]

equi_dup [in Base]

equi_push [in Base]

evalH_evalK_agree [in HeytingAndKripke]

evalK_evalH_agree [in HeytingAndKripke]

## F

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

FCI.incl [in Base]

FCI.ind [in Base]

FCI.it_incl [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

Glivenko [in PropL]Glivenko_refute [in PropL]

## H

Ha5Rref [in HeytingAndKripke]Ha5Rtra [in HeytingAndKripke]

Hb5Rref [in HeytingAndKripke]

Hb5Rtra [in HeytingAndKripke]

hilAK [in PropL]

hilAS [in PropL]

hilD [in PropL]

hilI [in PropL]

hil_iff_nd [in PropL]

hil_nd [in PropL]

## 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

list_cc [in Base]list_exists_not_incl [in Base]

list_exists_DM [in Base]

list_sigma_forall [in Base]

list_cycle [in Base]

## M

monotone [in HeytingAndKripke]monotone_ctx [in HeytingAndKripke]

## N

ndapp [in PropL]ndapp1 [in PropL]

ndapp2 [in PropL]

ndapp3 [in PropL]

ndcE [in PropL]

ndcW [in PropL]

ndc_refute [in PropL]

ndc_weak [in PropL]

ndDN [in PropL]

ndIE_weak [in PropL]

ndW [in PropL]

nd_hil [in PropL]

nd_embeds_ndc [in PropL]

nd_ndc [in PropL]

nd_subst [in PropL]

nd_con [in PropL]

nd_bool_sound [in PropL]

nd_weak [in PropL]

nd_soundK [in HeytingAndKripke]

nd_soundH [in HeytingAndKripke]

not_in_cons [in Base]

## P

power_extensional [in Base]power_nil [in Base]

power_incl [in Base]

## R

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]

## S

size_recursion [in Base]## U

undef_a_Or_b [in HeytingAndKripke]undef_a_And_b [in HeytingAndKripke]

undup_idempotent [in Base]

undup_id [in Base]

undup_equi [in Base]

undup_incl [in Base]

undup_id_equi [in Base]

# Constructor Index

## D

dupfreeC [in Base]dupfreeN [in Base]

## F

Fal [in PropL]## H

Ha5a [in HeytingAndKripke]Ha5ab [in HeytingAndKripke]

Ha5b [in HeytingAndKripke]

Ha5bot [in HeytingAndKripke]

Ha5top [in HeytingAndKripke]

Hb5a [in HeytingAndKripke]

Hb5ab [in HeytingAndKripke]

Hb5b [in HeytingAndKripke]

Hb5bot [in HeytingAndKripke]

Hb5top [in HeytingAndKripke]

hilA [in PropL]

hilE [in PropL]

hilK [in PropL]

hilMP [in PropL]

hilS [in PropL]

## I

Imp [in PropL]## M

mkHeytingAlgebra [in HeytingAndKripke]mkKripkeModel [in HeytingAndKripke]

## N

ndA [in PropL]ndcA [in PropL]

ndcC [in PropL]

ndcIE [in PropL]

ndcII [in PropL]

ndE [in PropL]

ndIE [in PropL]

ndII [in PropL]

## V

Var [in PropL]# Inductive Index

## D

dupfree [in Base]## F

form [in PropL]## H

Ha5 [in HeytingAndKripke]Hb5 [in HeytingAndKripke]

hil [in PropL]

## N

nd [in PropL]ndc [in PropL]

# Projection Index

## B

bot [in HeytingAndKripke]bot1 [in HeytingAndKripke]

## H

H [in HeytingAndKripke]## I

imp [in HeytingAndKripke]imp1 [in HeytingAndKripke]

imp2 [in HeytingAndKripke]

## J

join [in HeytingAndKripke]join1 [in HeytingAndKripke]

join2 [in HeytingAndKripke]

join3 [in HeytingAndKripke]

## L

label [in HeytingAndKripke]label_mon [in HeytingAndKripke]

## M

meet [in HeytingAndKripke]meet1 [in HeytingAndKripke]

meet2 [in HeytingAndKripke]

meet3 [in HeytingAndKripke]

## R

R [in HeytingAndKripke]Rref [in HeytingAndKripke]

Rtra [in HeytingAndKripke]

## S

state [in HeytingAndKripke]step [in HeytingAndKripke]

step_trans [in HeytingAndKripke]

step_refl [in HeytingAndKripke]

## T

top [in HeytingAndKripke]top1 [in HeytingAndKripke]

# Section Index

## C

Cardinality [in Base]## D

Dupfree [in Base]## E

Equi [in Base]## F

F [in PropL]FCI.FCI [in Base]

FilterComm [in Base]

FilterLemmas [in Base]

FilterLemmas_pq [in Base]

## H

HeytingAlgebra [in HeytingAndKripke]HeytingAlgebraToKripkeModel [in HeytingAndKripke]

HeytingHa5 [in HeytingAndKripke]

HeytingHb5 [in HeytingAndKripke]

## I

Inclusion [in Base]Iteration [in Base]

## K

KripkeModel [in HeytingAndKripke]KripkeModelToHeytingAlgebra [in HeytingAndKripke]

## M

Membership [in Base]## P

PowerRep [in Base]## R

Removal [in Base]## U

Undup [in Base]# 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 PropL]

## 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 PropL]## T

True_dec [in Base]# Definition Index

## A

andlist [in PropL]assn [in PropL]

## B

bsc [in PropL]## C

card [in Base]CharFal [in PropL]

CharImp [in PropL]

Consistency [in PropL]

context [in PropL]

Cut [in PropL]

## D

dec [in Base]decision [in Base]

disjoint [in Base]

dupfree_inv [in Base]

## E

EntailRelAllProps [in PropL]equi [in Base]

evalH [in HeytingAndKripke]

evalH' [in HeytingAndKripke]

evalK [in HeytingAndKripke]

evalK' [in HeytingAndKripke]

## F

FCI.C [in Base]FCI.F [in Base]

filter [in Base]

FK [in PropL]

FP [in Base]

FS [in PropL]

## H

Ha5HA [in HeytingAndKripke]Ha5imp [in HeytingAndKripke]

Ha5interp [in HeytingAndKripke]

Ha5join [in HeytingAndKripke]

Ha5meet [in HeytingAndKripke]

Ha5R [in HeytingAndKripke]

Hb5HA [in HeytingAndKripke]

Hb5imp [in HeytingAndKripke]

Hb5interp [in HeytingAndKripke]

Hb5join [in HeytingAndKripke]

Hb5meet [in HeytingAndKripke]

Hb5R [in HeytingAndKripke]

HeytingAlgebraOfKripkeModel [in HeytingAndKripke]

HeytingInterpOfKripkeModel [in HeytingAndKripke]

## I

inclp [in Base]it [in Base]

## K

KripkeModelOfHeytingAlgebra [in HeytingAndKripke]## M

Monotonicity [in PropL]## N

Not [in PropL]## P

power [in Base]ProperFilter [in HeytingAndKripke]

## R

Reflexivity [in PropL]rem [in Base]

rep [in Base]

## S

satis [in PropL]subst [in PropL]

Substitution [in PropL]

## U

undup [in Base]## V

var [in PropL]vars [in PropL]

# Record Index

## H

HeytingAlgebra [in HeytingAndKripke]## K

KripkeModel [in HeytingAndKripke]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 | (362 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 | (5 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 | (1 entry) |

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 | (40 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 | (148 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 | (30 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 | (7 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 | (25 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 | (20 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 | (26 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 | (55 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 | (2 entries) |

This page has been generated by coqdoc