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 | (647 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 | (69 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 | (4 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 | (284 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 | (60 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 | (36 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 | (10 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 | (33 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 | (28 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 | (110 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 | (4 entries) |

# Global Index

## A

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

AndIndependence_hey [lemma, in PropiLindep]

AndIndependence_hey [lemma, in PropiLindep]

and_dec [instance, in Base]

app_equi_proper [instance, in Base]

app_incl_proper [instance, in Base]

## B

Base [library]bool_eq_dec [instance, in Base]

bot [projection, in PropiLmodel]

bot [projection, in PropiLmodel]

bot1 [projection, in PropiLmodel]

bot1 [projection, in PropiLmodel]

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]

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.A0 [variable, in PropiL]

Decidability.s0 [variable, in PropiL]

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]

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]

eqH [definition, in PropiLmodel]

eqH [definition, in PropiLmodel]

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]

evalH [definition, in PropiLmodel]

evalH [definition, in PropiLmodel]

evalHf [lemma, in PropiLmodel]

evalHf [lemma, in PropiLmodel]

evalH' [definition, in PropiLmodel]

evalH' [definition, in PropiLmodel]

evalK [definition, in PropiLmodel]

evalK [definition, in PropiLmodel]

evalKA [definition, in PropiLmodel]

evalKA [definition, in PropiLmodel]

evalK_evalH_agree [lemma, in PropiLmodel]

evalK_mono [lemma, in PropiLmodel]

evalK_evalH_agree [lemma, in PropiLmodel]

evalK_mono [lemma, in PropiLmodel]

## F

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

FalIndependence_hey [lemma, in PropiLindep]

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]

FormHA [definition, in PropiLmodel]

FormHA [definition, in PropiLmodel]

FormHeytingAlgebra [section, in PropiLmodel]

FormHeytingAlgebra [section, in PropiLmodel]

FormHeytingAlgebra.bot [variable, in PropiLmodel]

FormHeytingAlgebra.bot [variable, in PropiLmodel]

FormHeytingAlgebra.H [variable, in PropiLmodel]

FormHeytingAlgebra.H [variable, in PropiLmodel]

FormHeytingAlgebra.imp [variable, in PropiLmodel]

FormHeytingAlgebra.imp [variable, in PropiLmodel]

FormHeytingAlgebra.join [variable, in PropiLmodel]

FormHeytingAlgebra.join [variable, in PropiLmodel]

FormHeytingAlgebra.meet [variable, in PropiLmodel]

FormHeytingAlgebra.meet [variable, in PropiLmodel]

FormHeytingAlgebra.R [variable, in PropiLmodel]

FormHeytingAlgebra.R [variable, in PropiLmodel]

form_eq_dec [instance, in PropiL]

FP [definition, in Base]

FS [definition, in PropiL]

## G

Gamma [definition, in PropiL]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]

genXM [lemma, in PropiLindep]

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]

goal [definition, in PropiL]

goal_eq_dec [instance, in PropiL]

## H

H [projection, in PropiLmodel]H [projection, in PropiLmodel]

HAequiv [lemma, in PropiLmodel]

HAequiv [lemma, in PropiLmodel]

HAProperty [section, in PropiLmodel]

HAProperty [section, in PropiLmodel]

HAProperty.HA [variable, in PropiLmodel]

HAProperty.HA [variable, in PropiLmodel]

Harrop [lemma, in PropiLindep]

HarropC [definition, in PropiLindep]

HarropF [definition, in PropiLindep]

HASound [section, in PropiLmodel]

HASound [section, in PropiLmodel]

HASound.HA [variable, in PropiLmodel]

HASound.HA [variable, in PropiLmodel]

HASound.interp [variable, in PropiLmodel]

HASound.interp [variable, in PropiLmodel]

HA_iff_nd [lemma, in PropiLmodel]

HA_nd [lemma, in PropiLmodel]

HA_iff_nd [lemma, in PropiLmodel]

HA_nd [lemma, in PropiLmodel]

hent [definition, in PropiLmodel]

hent [definition, in PropiLmodel]

hent_imp [lemma, in PropiLmodel]

hent_imp [lemma, in PropiLmodel]

HeytingAlgebra [record, in PropiLmodel]

HeytingAlgebra [record, in PropiLmodel]

HeytingHMK1 [section, in PropiLindep]

HeytingHMK2 [section, in PropiLindep]

HeytingHMK3 [section, in PropiLindep]

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]

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]

HMK1 [inductive, in PropiLindep]

HMK1a [constructor, in PropiLindep]

HMK1bot [constructor, in PropiLindep]

HMK1HA [definition, in PropiLindep]

HMK1imp [definition, in PropiLindep]

HMK1join [definition, in PropiLindep]

HMK1meet [definition, in PropiLindep]

HMK1R [definition, in PropiLindep]

HMK1Rref [lemma, in PropiLindep]

HMK1Rtra [lemma, in PropiLindep]

HMK1top [constructor, in PropiLindep]

HMK2 [inductive, in PropiLindep]

HMK2a [constructor, in PropiLindep]

HMK2ab [constructor, in PropiLindep]

HMK2b [constructor, in PropiLindep]

HMK2bot [constructor, in PropiLindep]

HMK2HA [definition, in PropiLindep]

HMK2imp [definition, in PropiLindep]

HMK2join [definition, in PropiLindep]

HMK2meet [definition, in PropiLindep]

HMK2R [definition, in PropiLindep]

HMK2Rref [lemma, in PropiLindep]

HMK2Rtra [lemma, in PropiLindep]

HMK2top [constructor, in PropiLindep]

HMK3 [definition, in PropiLindep]

HMK3HA [definition, in PropiLindep]

HMK3imp [definition, in PropiLindep]

HMK3join [definition, in PropiLindep]

HMK3meet [definition, in PropiLindep]

HMK3R [definition, in PropiLindep]

HMK3Rref [lemma, in PropiLindep]

HMK3Rtra [lemma, in PropiLindep]

## I

iff_dec [instance, in Base]imp [projection, in PropiLmodel]

imp [projection, in PropiLmodel]

Imp [constructor, in PropiL]

ImpFree [definition, in PropiL]

ImpIndependence_hey [lemma, in PropiLindep]

impl_dec [instance, in Base]

imp1 [projection, in PropiLmodel]

imp1 [projection, in PropiLmodel]

imp2 [lemma, in PropiLmodel]

imp2 [lemma, in PropiLmodel]

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]

interp [projection, in PropiLmodel]

interp [projection, in PropiLmodel]

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 PropiLmodel]join [projection, in PropiLmodel]

join_com [lemma, in PropiLmodel]

join_com [lemma, in PropiLmodel]

join1 [projection, in PropiLmodel]

join1 [projection, in PropiLmodel]

join2 [lemma, in PropiLmodel]

join2 [lemma, in PropiLmodel]

join3 [lemma, in PropiLmodel]

join3 [lemma, in PropiLmodel]

## K

KripkeModel [record, in PropiLmodel]KripkeModel [record, in PropiLmodel]

KripkeSemantics [section, in PropiLmodel]

KripkeSemantics [section, in PropiLmodel]

KripkeSemantics.KM [variable, in PropiLmodel]

KripkeSemantics.KM [variable, in PropiLmodel]

Kripke2Heyting [section, in PropiLmodel]

Kripke2Heyting [section, in PropiLmodel]

Kripke2Heyting.bot [variable, in PropiLmodel]

Kripke2Heyting.bot [variable, in PropiLmodel]

Kripke2Heyting.H [variable, in PropiLmodel]

Kripke2Heyting.H [variable, in PropiLmodel]

Kripke2Heyting.imp [variable, in PropiLmodel]

Kripke2Heyting.imp [variable, in PropiLmodel]

Kripke2Heyting.join [variable, in PropiLmodel]

Kripke2Heyting.join [variable, in PropiLmodel]

Kripke2Heyting.KM [variable, in PropiLmodel]

Kripke2Heyting.KM [variable, in PropiLmodel]

Kripke2Heyting.meet [variable, in PropiLmodel]

Kripke2Heyting.meet [variable, in PropiLmodel]

Kripke2Heyting.R [variable, in PropiLmodel]

Kripke2Heyting.R [variable, in PropiLmodel]

Kripke2Heyting.UC [variable, in PropiLmodel]

Kripke2Heyting.UC [variable, in PropiLmodel]

Kripke2Heyting.UCS [variable, in PropiLmodel]

Kripke2Heyting.UCS [variable, in PropiLmodel]

K2H [definition, in PropiLmodel]

K2H [definition, in PropiLmodel]

K2Hinterp [definition, in PropiLmodel]

K2Hinterp [definition, in PropiLmodel]

## L

Lambda [definition, in PropiL]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]

ltr [definition, in PropiLmodel]

ltr [definition, in PropiLmodel]

ltr_CharImp [lemma, in PropiLmodel]

ltr_CharImp [lemma, in PropiLmodel]

## M

meet [projection, in PropiLmodel]meet [projection, in PropiLmodel]

meet_com [lemma, in PropiLmodel]

meet_com [lemma, in PropiLmodel]

meet1 [projection, in PropiLmodel]

meet1 [projection, in PropiLmodel]

meet2 [lemma, in PropiLmodel]

meet2 [lemma, in PropiLmodel]

meet3 [lemma, in PropiLmodel]

meet3 [lemma, in PropiLmodel]

Membership [section, in Base]

Membership.X [variable, in Base]

mkHeytingAlgebra [constructor, in PropiLmodel]

mkHeytingAlgebra [constructor, in PropiLmodel]

mkKripkeModel [constructor, in PropiLmodel]

mkKripkeModel [constructor, in PropiLmodel]

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]

ndCW [lemma, in PropiL]

ndDeMorgan_hey [lemma, in PropiLindep]

ndDeMorgan_hey [lemma, in PropiLindep]

ndDN_hey [lemma, in PropiLindep]

ndDN_hey [lemma, in PropiLindep]

ndDN'_hey [lemma, in PropiLindep]

ndDN'_hey [lemma, in PropiLindep]

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]

ndXM_hey [lemma, in PropiLindep]

ndXM_hey [lemma, in PropiLindep]

nd_soundKM [lemma, in PropiLmodel]

nd_soundHA [lemma, in PropiLmodel]

nd_soundKM [lemma, in PropiLmodel]

nd_soundHA [lemma, in PropiLmodel]

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 [constructor, in PropiL]

negative [definition, in PropiL]

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]

OrFree_Harrop [lemma, in PropiLindep]

OrIndependence [lemma, in PropiLindep]

OrIndependence_hey [lemma, in PropiLindep]

or_dec [instance, in Base]

## P

persist [projection, in PropiLmodel]persist [projection, in PropiLmodel]

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]

PropiL [library]

PropiLindep [library]

PropiLmodel [library]

## R

R [projection, in PropiLmodel]R [projection, in PropiLmodel]

Reflexivity [definition, in PropiL]

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]

Rref [projection, in PropiLmodel]

Rref [projection, in PropiLmodel]

Rtra [projection, in PropiLmodel]

Rtra [projection, in PropiLmodel]

## S

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]

ssL [definition, in PropiL]

ssL [section, in PropiL]

ssLb [definition, in PropiL]

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]

step_dec [instance, in PropiL]

subst [definition, in PropiL]

Substitution [definition, in PropiL]

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]

top [definition, in PropiLmodel]

top [definition, in PropiLmodel]

top1 [lemma, in PropiLmodel]

top1 [lemma, in PropiLmodel]

True_dec [instance, in Base]

## U

U [definition, in PropiL]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_pos [lemma, in PropiL]

U_sfc [definition, in PropiL]

## V

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

Vf [definition, in PropiLmodel]

Vf [definition, in PropiLmodel]

## W

W [projection, in PropiLmodel]W [projection, in PropiLmodel]

WR [projection, in PropiLmodel]

WR [projection, in PropiLmodel]

WRref [projection, in PropiLmodel]

WRref [projection, in PropiLmodel]

WRtra [projection, in PropiLmodel]

WRtra [projection, in PropiLmodel]

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

FormHeytingAlgebra.bot [in PropiLmodel]

FormHeytingAlgebra.bot [in PropiLmodel]

FormHeytingAlgebra.H [in PropiLmodel]

FormHeytingAlgebra.H [in PropiLmodel]

FormHeytingAlgebra.imp [in PropiLmodel]

FormHeytingAlgebra.imp [in PropiLmodel]

FormHeytingAlgebra.join [in PropiLmodel]

FormHeytingAlgebra.join [in PropiLmodel]

FormHeytingAlgebra.meet [in PropiLmodel]

FormHeytingAlgebra.meet [in PropiLmodel]

FormHeytingAlgebra.R [in PropiLmodel]

FormHeytingAlgebra.R [in PropiLmodel]

## H

HAProperty.HA [in PropiLmodel]HAProperty.HA [in PropiLmodel]

HASound.HA [in PropiLmodel]

HASound.HA [in PropiLmodel]

HASound.interp [in PropiLmodel]

HASound.interp [in PropiLmodel]

## I

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

Iteration.X [in Base]

## K

KripkeSemantics.KM [in PropiLmodel]KripkeSemantics.KM [in PropiLmodel]

Kripke2Heyting.bot [in PropiLmodel]

Kripke2Heyting.bot [in PropiLmodel]

Kripke2Heyting.H [in PropiLmodel]

Kripke2Heyting.H [in PropiLmodel]

Kripke2Heyting.imp [in PropiLmodel]

Kripke2Heyting.imp [in PropiLmodel]

Kripke2Heyting.join [in PropiLmodel]

Kripke2Heyting.join [in PropiLmodel]

Kripke2Heyting.KM [in PropiLmodel]

Kripke2Heyting.KM [in PropiLmodel]

Kripke2Heyting.meet [in PropiLmodel]

Kripke2Heyting.meet [in PropiLmodel]

Kripke2Heyting.R [in PropiLmodel]

Kripke2Heyting.R [in PropiLmodel]

Kripke2Heyting.UC [in PropiLmodel]

Kripke2Heyting.UC [in PropiLmodel]

Kripke2Heyting.UCS [in PropiLmodel]

Kripke2Heyting.UCS [in PropiLmodel]

## M

Membership.X [in Base]## P

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

## R

Removal.X [in Base]## U

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

# Library Index

## B

Base## P

PropiLPropiLindep

PropiLmodel

# Lemma Index

## A

AndIndependence_hey [in PropiLindep]AndIndependence_hey [in PropiLindep]

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

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]

evalHf [in PropiLmodel]

evalHf [in PropiLmodel]

evalK_evalH_agree [in PropiLmodel]

evalK_mono [in PropiLmodel]

evalK_evalH_agree [in PropiLmodel]

evalK_mono [in PropiLmodel]

## F

FalIndependence_hey [in PropiLindep]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]

genXM [in PropiLindep]

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]

## H

HAequiv [in PropiLmodel]HAequiv [in PropiLmodel]

Harrop [in PropiLindep]

HA_iff_nd [in PropiLmodel]

HA_nd [in PropiLmodel]

HA_iff_nd [in PropiLmodel]

HA_nd [in PropiLmodel]

hent_imp [in PropiLmodel]

hent_imp [in PropiLmodel]

hilAK [in PropiL]

hilAS [in PropiL]

hilD [in PropiL]

hilI [in PropiL]

hil_iff_nd [in PropiL]

hil_nd [in PropiL]

HMK1Rref [in PropiLindep]

HMK1Rtra [in PropiLindep]

HMK2Rref [in PropiLindep]

HMK2Rtra [in PropiLindep]

HMK3Rref [in PropiLindep]

HMK3Rtra [in PropiLindep]

## I

ImpIndependence_hey [in PropiLindep]imp2 [in PropiLmodel]

imp2 [in PropiLmodel]

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]

## J

join_com [in PropiLmodel]join_com [in PropiLmodel]

join2 [in PropiLmodel]

join2 [in PropiLmodel]

join3 [in PropiLmodel]

join3 [in PropiLmodel]

## L

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]

ltr_CharImp [in PropiLmodel]

ltr_CharImp [in PropiLmodel]

## M

meet_com [in PropiLmodel]meet_com [in PropiLmodel]

meet2 [in PropiLmodel]

meet2 [in PropiLmodel]

meet3 [in PropiLmodel]

meet3 [in PropiLmodel]

## N

ndCW [in PropiL]ndDeMorgan_hey [in PropiLindep]

ndDeMorgan_hey [in PropiLindep]

ndDN_hey [in PropiLindep]

ndDN_hey [in PropiLindep]

ndDN'_hey [in PropiLindep]

ndDN'_hey [in PropiLindep]

ndW [in PropiL]

ndXM_hey [in PropiLindep]

ndXM_hey [in PropiLindep]

nd_soundKM [in PropiLmodel]

nd_soundHA [in PropiLmodel]

nd_soundKM [in PropiLmodel]

nd_soundHA [in PropiLmodel]

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]

not_in_cons [in Base]

## O

OrAR_mono_nd [in PropiL]OrAR_mono [in PropiL]

OrFree_Harrop [in PropiLindep]

OrIndependence [in PropiLindep]

OrIndependence_hey [in PropiLindep]

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

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

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]

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]

top1 [in PropiLmodel]

top1 [in PropiLmodel]

## 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_pos [in PropiL]

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

## H

hilA [in PropiL]hilAI [in PropiL]

hilAL [in PropiL]

hilAR [in PropiL]

hilE [in PropiL]

hilK [in PropiL]

hilMP [in PropiL]

hilOE [in PropiL]

hilOL [in PropiL]

hilOR [in PropiL]

hilS [in PropiL]

HMK1a [in PropiLindep]

HMK1bot [in PropiLindep]

HMK1top [in PropiLindep]

HMK2a [in PropiLindep]

HMK2ab [in PropiLindep]

HMK2b [in PropiLindep]

HMK2bot [in PropiLindep]

HMK2top [in PropiLindep]

## I

Imp [in PropiL]## M

mkHeytingAlgebra [in PropiLmodel]mkHeytingAlgebra [in PropiLmodel]

mkKripkeModel [in PropiLmodel]

mkKripkeModel [in PropiLmodel]

## N

ndA [in PropiL]ndAE [in PropiL]

ndAI [in PropiL]

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

## B

bot [in PropiLmodel]bot [in PropiLmodel]

bot1 [in PropiLmodel]

bot1 [in PropiLmodel]

## H

H [in PropiLmodel]H [in PropiLmodel]

## I

imp [in PropiLmodel]imp [in PropiLmodel]

imp1 [in PropiLmodel]

imp1 [in PropiLmodel]

interp [in PropiLmodel]

interp [in PropiLmodel]

## J

join [in PropiLmodel]join [in PropiLmodel]

join1 [in PropiLmodel]

join1 [in PropiLmodel]

## M

meet [in PropiLmodel]meet [in PropiLmodel]

meet1 [in PropiLmodel]

meet1 [in PropiLmodel]

## P

persist [in PropiLmodel]persist [in PropiLmodel]

## R

R [in PropiLmodel]R [in PropiLmodel]

Rref [in PropiLmodel]

Rref [in PropiLmodel]

Rtra [in PropiLmodel]

Rtra [in PropiLmodel]

## W

W [in PropiLmodel]W [in PropiLmodel]

WR [in PropiLmodel]

WR [in PropiLmodel]

WRref [in PropiLmodel]

WRref [in PropiLmodel]

WRtra [in PropiLmodel]

WRtra [in PropiLmodel]

# Inductive Index

## D

dupfree [in Base]dupfree [in Base]

## F

form [in PropiL]## G

gen [in PropiL]## H

hil [in PropiL]HMK1 [in PropiLindep]

HMK2 [in PropiLindep]

## N

nd [in PropiL]## S

sform [in PropiL]## T

tab [in PropiL]# Section Index

## C

Cardinality [in Base]## D

Decidability [in PropiL]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]

FormHeytingAlgebra [in PropiLmodel]

FormHeytingAlgebra [in PropiLmodel]

## H

HAProperty [in PropiLmodel]HAProperty [in PropiLmodel]

HASound [in PropiLmodel]

HASound [in PropiLmodel]

HeytingHMK1 [in PropiLindep]

HeytingHMK2 [in PropiLindep]

HeytingHMK3 [in PropiLindep]

## I

Inclusion [in Base]Iteration [in Base]

## K

KripkeSemantics [in PropiLmodel]KripkeSemantics [in PropiLmodel]

Kripke2Heyting [in PropiLmodel]

Kripke2Heyting [in PropiLmodel]

## M

Membership [in Base]## P

PowerRep [in Base]PowerRep [in Base]

## R

Removal [in Base]## S

ssL [in PropiL]## U

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

## G

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

sform_eq_dec [in PropiL]step_dec [in PropiL]

## T

True_dec [in Base]# Definition Index

## A

AndFree [in PropiL]## B

b2s [in PropiL]## C

card [in Base]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]decision [in Base]

depth [in PropiL]

disjoint [in Base]

dupfree_inv [in Base]

dupfree_inv [in Base]

## E

EntailRelAllProps [in PropiL]eqH [in PropiLmodel]

eqH [in PropiLmodel]

Equi [in PropiL]

equi [in Base]

evalH [in PropiLmodel]

evalH [in PropiLmodel]

evalH' [in PropiLmodel]

evalH' [in PropiLmodel]

evalK [in PropiLmodel]

evalK [in PropiLmodel]

evalKA [in PropiLmodel]

evalKA [in PropiLmodel]

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

FormHA [in PropiLmodel]

FormHA [in PropiLmodel]

FP [in Base]

FS [in PropiL]

## G

Gamma [in PropiL]goal [in PropiL]

## H

HarropC [in PropiLindep]HarropF [in PropiLindep]

hent [in PropiLmodel]

hent [in PropiLmodel]

HMK1HA [in PropiLindep]

HMK1imp [in PropiLindep]

HMK1join [in PropiLindep]

HMK1meet [in PropiLindep]

HMK1R [in PropiLindep]

HMK2HA [in PropiLindep]

HMK2imp [in PropiLindep]

HMK2join [in PropiLindep]

HMK2meet [in PropiLindep]

HMK2R [in PropiLindep]

HMK3 [in PropiLindep]

HMK3HA [in PropiLindep]

HMK3imp [in PropiLindep]

HMK3join [in PropiLindep]

HMK3meet [in PropiLindep]

HMK3R [in PropiLindep]

## I

ImpFree [in PropiL]inclp [in Base]

it [in Base]

## K

K2H [in PropiLmodel]K2H [in PropiLmodel]

K2Hinterp [in PropiLmodel]

K2Hinterp [in PropiLmodel]

## L

Lambda [in PropiL]ltr [in PropiLmodel]

ltr [in PropiLmodel]

## M

Monotonicity [in PropiL]## N

negative [in PropiL]Not [in PropiL]

## O

OrAR [in PropiL]OrFree [in PropiL]

## P

positive [in PropiL]power [in Base]

power [in Base]

## R

Reflexivity [in PropiL]rem [in Base]

rep [in Base]

rep [in Base]

## S

scl [in PropiL]scl' [in PropiL]

sf_closed [in PropiL]

size [in PropiL]

sizeF [in PropiL]

ssL [in PropiL]

ssLb [in PropiL]

ssL' [in PropiL]

ss_closed [in PropiL]

ss_closed' [in PropiL]

step [in PropiL]

subst [in PropiL]

Substitution [in PropiL]

s2b [in PropiL]

## T

top [in PropiLmodel]top [in PropiLmodel]

## U

U [in PropiL]undup [in Base]

undup [in Base]

uns [in PropiL]

U_sfc [in PropiL]

## V

var [in PropiL]Vf [in PropiLmodel]

Vf [in PropiLmodel]

# Record Index

## H

HeytingAlgebra [in PropiLmodel]HeytingAlgebra [in PropiLmodel]

## K

KripkeModel [in PropiLmodel]KripkeModel [in PropiLmodel]

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 | (647 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 | (69 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 | (4 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 | (284 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 | (60 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 | (36 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 | (10 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 | (33 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 | (28 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 | (110 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 | (4 entries) |

This page has been generated by coqdoc