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 (876 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 (108 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 (5 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 (381 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 (53 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 (42 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 (8 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 (49 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 (43 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 (173 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 (5 entries)

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]


B

base [definition, in PropiLFmodel]
Base [library]
baseKD [definition, in PropiLFmodel]
baseKD_complete [lemma, in PropiLFmodel]
baseKD_sound [lemma, in PropiLFmodel]
baseKD_in [lemma, in PropiLFmodel]
baseVars [definition, in PropiLFmodel]
baseVars_in [lemma, in PropiLFmodel]
baseVars_incl [lemma, in PropiLFmodel]
Binter [definition, in PropiLFmodel]
Binter_sound [lemma, in PropiLFmodel]
bool_eq_dec [instance, in Base]
bot [projection, in PropiLmodel]
bot [projection, in PropiLmodel]
bot1 [projection, in PropiLmodel]
bot1 [projection, in PropiLmodel]
Bunion [definition, in PropiLFmodel]
Bunion_sound [lemma, in PropiLFmodel]
b2s [definition, in PropiL]


C

CanonicalDemo [section, in PropiLFmodel2]
CanonicalDemo.sscU [variable, in PropiLFmodel2]
CanonicalDemo.U [variable, in PropiLFmodel2]
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]
CD [definition, in PropiLFmodel2]
CD_demo [lemma, in PropiLFmodel2]
CharAnd [definition, in PropiL]
CharFal [definition, in PropiL]
CharImp [definition, in PropiL]
CharOr [definition, in PropiL]
clause [definition, in PropiL]
clauseCD [definition, in PropiLFmodel2]
compactCD_restore [definition, in PropiLFmodel2]
compactCD_restore [definition, in PropiLFmodel2]
compactDemo [definition, in PropiLFmodel2]
compactDemo [definition, in PropiLFmodel2]
compact_restore_demo [lemma, in PropiLFmodel2]
compact_CD_equi [lemma, in PropiLFmodel2]
compact_sound [lemma, in PropiLFmodel2]
compact_cons [lemma, in PropiLFmodel2]
compact_CD [definition, in PropiLFmodel2]
compact_restore_demo [lemma, in PropiLFmodel2]
compact_CD_equi [lemma, in PropiLFmodel2]
compact_sound [lemma, in PropiLFmodel2]
compact_cons [lemma, in PropiLFmodel2]
compact_CD [definition, in PropiLFmodel2]
cons [definition, in PropiLFmodel]
Cons [definition, in PropiLFmodel2]
Consistency [definition, in PropiL]
consW [lemma, in PropiLFmodel]
cons_dec [instance, in PropiLFmodel]
cons_equi_proper [instance, in Base]
cons_incl_proper [instance, in Base]
Cons_mono [lemma, in PropiLFmodel2]
Cons_dec [instance, in PropiLFmodel2]
context [definition, in PropiL]
CounterModels [section, in PropiLFmodel]
CounterModels.K1 [variable, in PropiLFmodel]
CounterModels.K2 [variable, in PropiLFmodel]
CounterModels.K3 [variable, in PropiLFmodel]
CounterModels.K4 [variable, in PropiLFmodel]
Cut [definition, in PropiL]
CVars [definition, in PropiLFmodel]
CVars_correct [lemma, in PropiLFmodel]
c2f [definition, in PropiL]
C2PC [definition, in PropiLFmodel]


D

dec [definition, in Base]
Decidability [section, in PropiL]
Decidability.A0 [variable, in PropiL]
Decidability.s0 [variable, in PropiL]
decision [definition, in Base]
dec_ucsPred [lemma, in PropiLFmodel]
dec_prop_iff [lemma, in Base]
dec_DM_impl [lemma, in Base]
dec_DM_and [lemma, in Base]
dec_DN [lemma, in Base]
Demo [definition, in PropiLFmodel]
Demo [section, in PropiLFmodel]
DemoFiniteKripke [section, in PropiLFmodel2]
DemoKBase [section, in PropiLFmodel]
DemoSat [lemma, in PropiLFmodel2]
DemoSatisAll [lemma, in PropiLFmodel2]
Demo_equi [lemma, in PropiLFmodel]
demo_extension [lemma, in PropiLFmodel2]
depth [definition, in PropiL]
dequi [definition, in PropiLFmodel]
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]
dsub [definition, in PropiLFmodel]
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]
D2FKM [definition, in PropiLFmodel2]


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]
eq_decW [projection, in PropiLFmodel]
evalFK [definition, in PropiLFmodel]
evalFK_OrAR [lemma, in PropiLFmodel]
evalFK_mono [lemma, in PropiLFmodel]
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]
evalTK [definition, in PropiLFmodel]
evalTK' [definition, in PropiLFmodel]
extension [lemma, in PropiLFmodel2]


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_idempotent [lemma, in PropiLFmodel]
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]
filter_equi [lemma, in PropiLFmodel2]
FImp [definition, in PropiLFmodel]
FImpList [definition, in PropiLFmodel]
FImpList_in [lemma, in PropiLFmodel]
FImpList_ind [lemma, in PropiLFmodel]
FImpList_closure [lemma, in PropiLFmodel]
FImp_in4 [lemma, in PropiLFmodel]
FImp_in3 [lemma, in PropiLFmodel]
FImp_in2 [lemma, in PropiLFmodel]
FImp_in1 [lemma, in PropiLFmodel]
FImp_greatest [lemma, in PropiLFmodel]
FImp_Heyting [lemma, in PropiLFmodel]
FiniteClosure [section, in PropiLFmodel]
FiniteClosure.F [variable, in PropiLFmodel]
FiniteClosure.FE [variable, in PropiLFmodel]
FiniteClosure.FS [variable, in PropiLFmodel]
FiniteClosure.UCSFilter [variable, in PropiLFmodel]
FiniteKripke [section, in PropiLFmodel]
FiniteKripkeModel [record, in PropiLFmodel]
FiniteKripke.FKM [variable, in PropiLFmodel]
FiniteKripke.interp [variable, in PropiLFmodel]
FiniteKripke.pW [variable, in PropiLFmodel]
FiniteKripke.W [variable, in PropiLFmodel]
FiniteKripke.WR [variable, in PropiLFmodel]
FiniteKripke.WRref [variable, in PropiLFmodel]
FiniteKripke.WRtra [variable, in PropiLFmodel]
FK [definition, in PropiL]
FKImp [definition, in PropiLFmodel]
FKImp_in [lemma, in PropiLFmodel]
FKImp_ind [lemma, in PropiLFmodel]
FKImp_closure [lemma, in PropiLFmodel]
FK2K [definition, in PropiLFmodel]
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]
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]
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]
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]
Hintikka [definition, in PropiLFmodel]
Hintikka_dec [instance, in PropiLFmodel]
Hintikka_equi [lemma, in PropiLFmodel]


I

iff_dec [instance, in Base]
imp [projection, in PropiLmodel]
imp [projection, in PropiLmodel]
Imp [constructor, in PropiL]
ImpFree [definition, in PropiL]
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]
inter [definition, in PropiLFmodel]
interp [projection, in PropiLmodel]
interp [projection, in PropiLmodel]
interp [projection, in PropiLFmodel]
interpTK [definition, in PropiLFmodel]
inter_sub [lemma, in PropiLFmodel]
inter_sound [lemma, in PropiLFmodel]
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]
in_map_informative [lemma, in PropiLFmodel2]
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]
kripke_nd [lemma, in PropiLFmodel2]
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]
K_Peirce [definition, in PropiLFmodel]
K_DN [definition, in PropiLFmodel]
K_XM [definition, in PropiLFmodel]
K_neg [definition, in PropiLFmodel]
K_orxy [definition, in PropiLFmodel]
K_var [definition, in PropiLFmodel]
K_Fal [definition, in PropiLFmodel]
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]
lfpTab [definition, in PropiLFmodel]
lfpTab_ind [lemma, in PropiLFmodel]
lfpTab_closure [lemma, in PropiLFmodel]
lfp_tab [lemma, in PropiLFmodel]
ListOperation [section, in PropiLFmodel]
ListOperation.X [variable, in PropiLFmodel]
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

maxCons_PartialOrder [lemma, in PropiLFmodel2]
maxCons_ParOrd [lemma, in PropiLFmodel2]
maxCons_equi [lemma, in PropiLFmodel2]
maxCons_incl [lemma, in PropiLFmodel2]
maxCons_equi_Fal [lemma, in PropiLFmodel2]
maxCons_PartialOrder [lemma, in PropiLFmodel2]
maxCons_ParOrd [lemma, in PropiLFmodel2]
maxCons_equi [lemma, in PropiLFmodel2]
maxCons_incl [lemma, in PropiLFmodel2]
maxCons_equi_Fal [lemma, in PropiLFmodel2]
maxCons_equi_vars [lemma, in PropiLFmodel2]
maxCons_XM [lemma, in PropiLFmodel2]
maxext [definition, in PropiLFmodel2]
maxExtension [lemma, in PropiLFmodel2]
maxext_samebase [lemma, in PropiLFmodel2]
maxext_samebase [lemma, in PropiLFmodel2]
maxext_nomore [lemma, in PropiLFmodel2]
MaximalExtension [section, in PropiLFmodel2]
MaximalExtension.p [variable, in PropiLFmodel2]
MaximalExtension.p_mono [variable, in PropiLFmodel2]
MaximalExtension.U [variable, in PropiLFmodel2]
MaximalExtension.X [variable, in PropiLFmodel2]
MaximalIdentity [section, in PropiLFmodel2]
MaximalIdentity.sclU [variable, in PropiLFmodel2]
MaximalIdentity.SFL [variable, in PropiLFmodel2]
MaximalIdentity.SFL [variable, in PropiLFmodel2]
MaximalIdentity.U [variable, in PropiLFmodel2]
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]
mkFiniteKripkeModel [constructor, in PropiLFmodel]
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]
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_soundKM [lemma, in PropiLmodel]
nd_soundHA [lemma, in PropiLmodel]
nd_soundKM [lemma, in PropiLmodel]
nd_soundHA [lemma, in PropiLmodel]
nd_soundFK [lemma, in PropiLFmodel]
nd_soundTK [lemma, in PropiLFmodel]
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]
negative_dec [instance, in PropiLFmodel]
negImp [definition, in PropiLFmodel2]
negImp [definition, in PropiLFmodel2]
negImp_dec [instance, in PropiLFmodel2]
negImp_dec [instance, in PropiLFmodel2]
negtrip_empty [lemma, in PropiLFmodel]
negtrip_in [lemma, in PropiLFmodel]
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

PContext [definition, in PropiLFmodel]
PContextRelation [section, in PropiLFmodel]
PContextRelation.pRC [variable, in PropiLFmodel]
PContextRelation.pRC_dec [variable, in PropiLFmodel]
PC2C [definition, in PropiLFmodel]
PC2C_pushpos [lemma, in PropiLFmodel]
PC2C_pushneg [lemma, in PropiLFmodel]
PC2C_neg [lemma, in PropiLFmodel]
PC2C_pos [lemma, in PropiLFmodel]
persist [projection, in PropiLmodel]
persist [projection, in PropiLmodel]
persist [projection, in PropiLFmodel]
pos [definition, in PropiLFmodel]
Pos [constructor, in PropiL]
positive [definition, in PropiL]
positive_dec [instance, in PropiLFmodel]
postrip_in [lemma, in PropiLFmodel]
posVar [definition, in PropiLFmodel2]
posVars [definition, in PropiLFmodel2]
posVar_dec [instance, in PropiLFmodel2]
pos_in [lemma, in PropiLFmodel2]
pos_in [lemma, in PropiLFmodel2]
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_once [lemma, in PropiLFmodel]
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]
prod_eq_dec [instance, in PropiLFmodel]
PropiL [library]
PropiLFmodel [library]
PropiLFmodel2 [library]
PropiLmodel [library]
pVar_nImp_dec [instance, in PropiLFmodel2]
pVar_nImp [definition, in PropiLFmodel2]
pVar_nImp_dec [instance, in PropiLFmodel2]
pVar_nImp [definition, in PropiLFmodel2]


Q

qmax [definition, in PropiLFmodel2]
qmax_Uequi [lemma, in PropiLFmodel2]
qmax_Uequi [lemma, in PropiLFmodel2]
qmax_maxext [lemma, in PropiLFmodel2]
qmax_exists [lemma, in PropiLFmodel2]
qmax_or [lemma, in PropiLFmodel2]


R

R [projection, in PropiLmodel]
R [projection, in PropiLmodel]
RC [definition, in PropiLFmodel]
RCinterp [definition, in PropiLFmodel]
RCList [definition, in PropiLFmodel]
RC_dec [instance, in PropiLFmodel]
Reflexivity [definition, in PropiL]
RelationToList [section, in PropiLFmodel]
RelationToList.R [variable, in PropiLFmodel]
RelationToList.S [variable, in PropiLFmodel]
RelationToList.SS [variable, in PropiLFmodel]
RelationToList.X [variable, in PropiLFmodel]
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_evalTK' [lemma, in PropiLFmodel]
rep_evalTK [lemma, in PropiLFmodel]
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]
RList [definition, in PropiLFmodel]
RList_in [lemma, in PropiLFmodel]
RList_ind [lemma, in PropiLFmodel]
RList_closure [lemma, in PropiLFmodel]
Rref [projection, in PropiLmodel]
Rref [projection, in PropiLmodel]
RTC [definition, in PropiLFmodel]
RTC_RCList [lemma, in PropiLFmodel]
RTC_iff [lemma, in PropiLFmodel]
RTC_in [lemma, in PropiLFmodel]
RTC_transitive [lemma, in PropiLFmodel]
RTC_reflexive [lemma, in PropiLFmodel]
RTC_ind [lemma, in PropiLFmodel]
RTC_closure [lemma, in PropiLFmodel]
Rtra [projection, in PropiLmodel]
Rtra [projection, in PropiLmodel]


S

satC [definition, in PropiLFmodel2]
satisD [definition, in PropiLFmodel]
satisDFK [definition, in PropiLFmodel2]
satisFK [definition, in PropiLFmodel]
satisFK' [definition, in PropiLFmodel]
scl [definition, in PropiL]
sclNeg_in [lemma, in PropiLFmodel2]
sclPos_in [lemma, in PropiLFmodel2]
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]
sfs [definition, in PropiLFmodel2]
sf_closed_cons [lemma, in PropiL]
sf_closed_app [lemma, in PropiL]
sf_closed [definition, in PropiL]
sigma_forall_list [lemma, in PropiLFmodel2]
size [definition, in PropiL]
sizeF [definition, in PropiL]
size_recursion [lemma, in Base]
ssc_scl [lemma, in PropiLFmodel2]
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]
state [definition, in PropiLFmodel]
step [definition, in PropiL]
stepFKImp [definition, in PropiLFmodel]
stepImp [definition, in PropiLFmodel]
stepRList [definition, in PropiLFmodel]
stepRList_dec [instance, in PropiLFmodel]
stepRTC [definition, in PropiLFmodel]
stepRTC_dec [instance, in PropiLFmodel]
stepTab [definition, in PropiLFmodel]
stepTab_mono [lemma, in PropiLFmodel]
stepTab_dec [instance, in PropiLFmodel]
stepTab' [definition, in PropiLFmodel]
stepUC [definition, in PropiLFmodel]
step_dec [instance, in PropiL]
subC [lemma, in PropiLFmodel]
SubClause [section, in PropiLFmodel]
subPC [definition, in PropiLFmodel]
subPos [definition, in PropiLFmodel2]
subPos [definition, in PropiLFmodel2]
subst [definition, in PropiL]
Substitution [definition, in PropiL]
sup [definition, in PropiLFmodel]
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]
TableauxConsistency [section, in PropiLFmodel]
TableauxDecidability [section, in PropiLFmodel]
TableauxDecidability.sscU [variable, in PropiLFmodel]
TableauxDecidability.U [variable, in PropiLFmodel]
tabLW [lemma, in PropiL]
TabND [section, in PropiLFmodel2]
tabON [constructor, in PropiL]
tabOP [constructor, in PropiL]
tabRW [lemma, in PropiL]
tabW [lemma, in PropiL]
tab_dec [lemma, in PropiLFmodel]
tab_dec' [lemma, in PropiLFmodel]
tab_lfp [lemma, in PropiLFmodel]
tab_nd [lemma, in PropiL]
tab_ndG [lemma, in PropiL]
tab_gen [lemma, in PropiL]
tab_genG [lemma, in PropiL]
tab_iff_ndG [lemma, in PropiLFmodel2]
tab_iff_nd [lemma, in PropiLFmodel2]
tab_nd_sat [lemma, in PropiLFmodel2]
TK [definition, in PropiLFmodel]
top [definition, in PropiLmodel]
top [definition, in PropiLmodel]
top1 [lemma, in PropiLmodel]
top1 [lemma, in PropiLmodel]
trip [definition, in PropiLFmodel]
True_dec [instance, in Base]
truthVal [definition, in PropiLFmodel]
TruthValues [section, in PropiLFmodel]
TruthValues.Implication [section, in PropiLFmodel]
TruthValues.K [variable, in PropiLFmodel]
TruthValues.Kdupfree [variable, in PropiLFmodel]
truthVal_evalTK' [lemma, in PropiLFmodel]
truthVal_evalTK [lemma, in PropiLFmodel]
truthVal_FImp [lemma, in PropiLFmodel]
truthVal_Binter [lemma, in PropiLFmodel]
truthVal_Bunion [lemma, in PropiLFmodel]
truthVal_inter [lemma, in PropiLFmodel]
truthVal_union [lemma, in PropiLFmodel]


U

U [definition, in PropiL]
UCS [definition, in PropiLFmodel]
UCSE [definition, in PropiLFmodel]
UCSE_sound [lemma, in PropiLFmodel]
ucsPred [definition, in PropiLFmodel]
UCS_sub [lemma, in PropiLFmodel]
UCS_in [lemma, in PropiLFmodel]
UCS_ind [lemma, in PropiLFmodel]
UCS_closure [lemma, in PropiLFmodel]
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]
union [definition, in PropiLFmodel]
union_sub [lemma, in PropiLFmodel]
union_sound [lemma, in PropiLFmodel]
uns [definition, in PropiL]
uns_pos [lemma, in PropiL]
upset [definition, in PropiLFmodel]
UpwardClosure [section, in PropiLFmodel]
UpwardClosure.R [variable, in PropiLFmodel]
UpwardClosure.U [variable, in PropiLFmodel]
UpwardClosure.X [variable, in PropiLFmodel]
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]
WE [projection, in PropiLFmodel]
WF [projection, in PropiLFmodel]
WR [projection, in PropiLmodel]
WR [projection, in PropiLmodel]
WRref [projection, in PropiLmodel]
WRref [projection, in PropiLmodel]
WRtra [projection, in PropiLmodel]
WRtra [projection, in PropiLmodel]
WS [projection, in PropiLFmodel]


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

CanonicalDemo.sscU [in PropiLFmodel2]
CanonicalDemo.U [in PropiLFmodel2]
Cardinality.X [in Base]
CounterModels.K1 [in PropiLFmodel]
CounterModels.K2 [in PropiLFmodel]
CounterModels.K3 [in PropiLFmodel]
CounterModels.K4 [in PropiLFmodel]


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]
FiniteClosure.F [in PropiLFmodel]
FiniteClosure.FE [in PropiLFmodel]
FiniteClosure.FS [in PropiLFmodel]
FiniteClosure.UCSFilter [in PropiLFmodel]
FiniteKripke.FKM [in PropiLFmodel]
FiniteKripke.interp [in PropiLFmodel]
FiniteKripke.pW [in PropiLFmodel]
FiniteKripke.W [in PropiLFmodel]
FiniteKripke.WR [in PropiLFmodel]
FiniteKripke.WRref [in PropiLFmodel]
FiniteKripke.WRtra [in PropiLFmodel]
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]


L

ListOperation.X [in PropiLFmodel]


M

MaximalExtension.p [in PropiLFmodel2]
MaximalExtension.p_mono [in PropiLFmodel2]
MaximalExtension.U [in PropiLFmodel2]
MaximalExtension.X [in PropiLFmodel2]
MaximalIdentity.sclU [in PropiLFmodel2]
MaximalIdentity.SFL [in PropiLFmodel2]
MaximalIdentity.SFL [in PropiLFmodel2]
MaximalIdentity.U [in PropiLFmodel2]
Membership.X [in Base]


P

PContextRelation.pRC [in PropiLFmodel]
PContextRelation.pRC_dec [in PropiLFmodel]
PowerRep.X [in Base]
PowerRep.X [in Base]


R

RelationToList.R [in PropiLFmodel]
RelationToList.S [in PropiLFmodel]
RelationToList.SS [in PropiLFmodel]
RelationToList.X [in PropiLFmodel]
Removal.X [in Base]


T

TableauxDecidability.sscU [in PropiLFmodel]
TableauxDecidability.U [in PropiLFmodel]
TruthValues.K [in PropiLFmodel]
TruthValues.Kdupfree [in PropiLFmodel]


U

Undup.X [in Base]
Undup.X [in Base]
UpwardClosure.R [in PropiLFmodel]
UpwardClosure.U [in PropiLFmodel]
UpwardClosure.X [in PropiLFmodel]



Library Index

B

Base


P

PropiL
PropiLFmodel
PropiLFmodel2
PropiLmodel



Lemma Index

B

baseKD_complete [in PropiLFmodel]
baseKD_sound [in PropiLFmodel]
baseKD_in [in PropiLFmodel]
baseVars_in [in PropiLFmodel]
baseVars_incl [in PropiLFmodel]
Binter_sound [in PropiLFmodel]
Bunion_sound [in PropiLFmodel]


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]
CD_demo [in PropiLFmodel2]
compact_restore_demo [in PropiLFmodel2]
compact_CD_equi [in PropiLFmodel2]
compact_sound [in PropiLFmodel2]
compact_cons [in PropiLFmodel2]
compact_restore_demo [in PropiLFmodel2]
compact_CD_equi [in PropiLFmodel2]
compact_sound [in PropiLFmodel2]
compact_cons [in PropiLFmodel2]
consW [in PropiLFmodel]
Cons_mono [in PropiLFmodel2]
CVars_correct [in PropiLFmodel]


D

dec_ucsPred [in PropiLFmodel]
dec_prop_iff [in Base]
dec_DM_impl [in Base]
dec_DM_and [in Base]
dec_DN [in Base]
DemoSat [in PropiLFmodel2]
DemoSatisAll [in PropiLFmodel2]
Demo_equi [in PropiLFmodel]
demo_extension [in PropiLFmodel2]
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]
evalFK_OrAR [in PropiLFmodel]
evalFK_mono [in PropiLFmodel]
evalHf [in PropiLmodel]
evalHf [in PropiLmodel]
evalK_evalH_agree [in PropiLmodel]
evalK_mono [in PropiLmodel]
evalK_evalH_agree [in PropiLmodel]
evalK_mono [in PropiLmodel]
extension [in PropiLFmodel2]


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_idempotent [in PropiLFmodel]
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]
filter_equi [in PropiLFmodel2]
FImpList_in [in PropiLFmodel]
FImpList_ind [in PropiLFmodel]
FImpList_closure [in PropiLFmodel]
FImp_in4 [in PropiLFmodel]
FImp_in3 [in PropiLFmodel]
FImp_in2 [in PropiLFmodel]
FImp_in1 [in PropiLFmodel]
FImp_greatest [in PropiLFmodel]
FImp_Heyting [in PropiLFmodel]
FKImp_in [in PropiLFmodel]
FKImp_ind [in PropiLFmodel]
FKImp_closure [in PropiLFmodel]


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]


H

HAequiv [in PropiLmodel]
HAequiv [in PropiLmodel]
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]
Hintikka_equi [in PropiLFmodel]


I

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]
inter_sub [in PropiLFmodel]
inter_sound [in PropiLFmodel]
in_rem_iff [in Base]
in_filter_iff [in Base]
in_cons_neq [in Base]
in_sing [in Base]
in_map_informative [in PropiLFmodel2]
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]


K

kripke_nd [in PropiLFmodel2]


L

lambda_gen [in PropiL]
lambda_ind [in PropiL]
lambda_closure [in PropiL]
lfpTab_ind [in PropiLFmodel]
lfpTab_closure [in PropiLFmodel]
lfp_tab [in PropiLFmodel]
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

maxCons_PartialOrder [in PropiLFmodel2]
maxCons_ParOrd [in PropiLFmodel2]
maxCons_equi [in PropiLFmodel2]
maxCons_incl [in PropiLFmodel2]
maxCons_equi_Fal [in PropiLFmodel2]
maxCons_PartialOrder [in PropiLFmodel2]
maxCons_ParOrd [in PropiLFmodel2]
maxCons_equi [in PropiLFmodel2]
maxCons_incl [in PropiLFmodel2]
maxCons_equi_Fal [in PropiLFmodel2]
maxCons_equi_vars [in PropiLFmodel2]
maxCons_XM [in PropiLFmodel2]
maxExtension [in PropiLFmodel2]
maxext_samebase [in PropiLFmodel2]
maxext_samebase [in PropiLFmodel2]
maxext_nomore [in PropiLFmodel2]
meet_com [in PropiLmodel]
meet_com [in PropiLmodel]
meet2 [in PropiLmodel]
meet2 [in PropiLmodel]
meet3 [in PropiLmodel]
meet3 [in PropiLmodel]


N

ndCW [in PropiL]
ndW [in PropiL]
nd_soundKM [in PropiLmodel]
nd_soundHA [in PropiLmodel]
nd_soundKM [in PropiLmodel]
nd_soundHA [in PropiLmodel]
nd_soundFK [in PropiLFmodel]
nd_soundTK [in PropiLFmodel]
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]
negtrip_empty [in PropiLFmodel]
negtrip_in [in PropiLFmodel]
not_in_cons [in Base]


O

OrAR_mono_nd [in PropiL]
OrAR_mono [in PropiL]


P

PC2C_pushpos [in PropiLFmodel]
PC2C_pushneg [in PropiLFmodel]
PC2C_neg [in PropiLFmodel]
PC2C_pos [in PropiLFmodel]
postrip_in [in PropiLFmodel]
pos_in [in PropiLFmodel2]
pos_in [in PropiLFmodel2]
power_once [in PropiLFmodel]
power_extensional [in Base]
power_nil [in Base]
power_incl [in Base]
power_extensional [in Base]
power_nil [in Base]
power_incl [in Base]


Q

qmax_Uequi [in PropiLFmodel2]
qmax_Uequi [in PropiLFmodel2]
qmax_maxext [in PropiLFmodel2]
qmax_exists [in PropiLFmodel2]
qmax_or [in PropiLFmodel2]


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_evalTK' [in PropiLFmodel]
rep_evalTK [in PropiLFmodel]
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]
RList_in [in PropiLFmodel]
RList_ind [in PropiLFmodel]
RList_closure [in PropiLFmodel]
RTC_RCList [in PropiLFmodel]
RTC_iff [in PropiLFmodel]
RTC_in [in PropiLFmodel]
RTC_transitive [in PropiLFmodel]
RTC_reflexive [in PropiLFmodel]
RTC_ind [in PropiLFmodel]
RTC_closure [in PropiLFmodel]


S

sclNeg_in [in PropiLFmodel2]
sclPos_in [in PropiLFmodel2]
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]
sigma_forall_list [in PropiLFmodel2]
size_recursion [in Base]
ssc_scl [in PropiLFmodel2]
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]
stepTab_mono [in PropiLFmodel]
subC [in PropiLFmodel]


T

tabCS [in PropiL]
tabLW [in PropiL]
tabRW [in PropiL]
tabW [in PropiL]
tab_dec [in PropiLFmodel]
tab_dec' [in PropiLFmodel]
tab_lfp [in PropiLFmodel]
tab_nd [in PropiL]
tab_ndG [in PropiL]
tab_gen [in PropiL]
tab_genG [in PropiL]
tab_iff_ndG [in PropiLFmodel2]
tab_iff_nd [in PropiLFmodel2]
tab_nd_sat [in PropiLFmodel2]
top1 [in PropiLmodel]
top1 [in PropiLmodel]
truthVal_evalTK' [in PropiLFmodel]
truthVal_evalTK [in PropiLFmodel]
truthVal_FImp [in PropiLFmodel]
truthVal_Binter [in PropiLFmodel]
truthVal_Bunion [in PropiLFmodel]
truthVal_inter [in PropiLFmodel]
truthVal_union [in PropiLFmodel]


U

UCSE_sound [in PropiLFmodel]
UCS_sub [in PropiLFmodel]
UCS_in [in PropiLFmodel]
UCS_ind [in PropiLFmodel]
UCS_closure [in PropiLFmodel]
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]
union_sub [in PropiLFmodel]
union_sound [in PropiLFmodel]
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]


I

Imp [in PropiL]


M

mkFiniteKripkeModel [in PropiLFmodel]
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]


E

eq_decW [in PropiLFmodel]


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]
interp [in PropiLFmodel]


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]
persist [in PropiLFmodel]


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]
WE [in PropiLFmodel]
WF [in PropiLFmodel]
WR [in PropiLmodel]
WR [in PropiLmodel]
WRref [in PropiLmodel]
WRref [in PropiLmodel]
WRtra [in PropiLmodel]
WRtra [in PropiLmodel]
WS [in PropiLFmodel]



Inductive Index

D

dupfree [in Base]
dupfree [in Base]


F

form [in PropiL]


G

gen [in PropiL]


H

hil [in PropiL]


N

nd [in PropiL]


S

sform [in PropiL]


T

tab [in PropiL]



Section Index

C

CanonicalDemo [in PropiLFmodel2]
Cardinality [in Base]
CounterModels [in PropiLFmodel]


D

Decidability [in PropiL]
Demo [in PropiLFmodel]
DemoFiniteKripke [in PropiLFmodel2]
DemoKBase [in PropiLFmodel]
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]
FiniteClosure [in PropiLFmodel]
FiniteKripke [in PropiLFmodel]
FormHeytingAlgebra [in PropiLmodel]
FormHeytingAlgebra [in PropiLmodel]


H

HAProperty [in PropiLmodel]
HAProperty [in PropiLmodel]
HASound [in PropiLmodel]
HASound [in PropiLmodel]


I

Inclusion [in Base]
Iteration [in Base]


K

KripkeSemantics [in PropiLmodel]
KripkeSemantics [in PropiLmodel]
Kripke2Heyting [in PropiLmodel]
Kripke2Heyting [in PropiLmodel]


L

ListOperation [in PropiLFmodel]


M

MaximalExtension [in PropiLFmodel2]
MaximalIdentity [in PropiLFmodel2]
Membership [in Base]


P

PContextRelation [in PropiLFmodel]
PowerRep [in Base]
PowerRep [in Base]


R

RelationToList [in PropiLFmodel]
Removal [in Base]


S

ssL [in PropiL]
SubClause [in PropiLFmodel]


T

TableauxConsistency [in PropiLFmodel]
TableauxDecidability [in PropiLFmodel]
TabND [in PropiLFmodel2]
TruthValues [in PropiLFmodel]
TruthValues.Implication [in PropiLFmodel]


U

Undup [in Base]
Undup [in Base]
UpwardClosure [in PropiLFmodel]



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_dec [in PropiLFmodel]
cons_equi_proper [in Base]
cons_incl_proper [in Base]
Cons_dec [in PropiLFmodel2]


E

equi_Equivalence [in Base]


F

False_dec [in Base]
form_eq_dec [in PropiL]


G

goal_eq_dec [in PropiL]


H

Hintikka_dec [in PropiLFmodel]


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]
negative_dec [in PropiLFmodel]
negImp_dec [in PropiLFmodel2]
negImp_dec [in PropiLFmodel2]
not_dec [in Base]


O

or_dec [in Base]


P

positive_dec [in PropiLFmodel]
posVar_dec [in PropiLFmodel2]
prod_eq_dec [in PropiLFmodel]
pVar_nImp_dec [in PropiLFmodel2]
pVar_nImp_dec [in PropiLFmodel2]


R

RC_dec [in PropiLFmodel]


S

sform_eq_dec [in PropiL]
stepRList_dec [in PropiLFmodel]
stepRTC_dec [in PropiLFmodel]
stepTab_dec [in PropiLFmodel]
step_dec [in PropiL]


T

True_dec [in Base]



Definition Index

A

AndFree [in PropiL]


B

base [in PropiLFmodel]
baseKD [in PropiLFmodel]
baseVars [in PropiLFmodel]
Binter [in PropiLFmodel]
Bunion [in PropiLFmodel]
b2s [in PropiL]


C

card [in Base]
CD [in PropiLFmodel2]
CharAnd [in PropiL]
CharFal [in PropiL]
CharImp [in PropiL]
CharOr [in PropiL]
clause [in PropiL]
clauseCD [in PropiLFmodel2]
compactCD_restore [in PropiLFmodel2]
compactCD_restore [in PropiLFmodel2]
compactDemo [in PropiLFmodel2]
compactDemo [in PropiLFmodel2]
compact_CD [in PropiLFmodel2]
compact_CD [in PropiLFmodel2]
cons [in PropiLFmodel]
Cons [in PropiLFmodel2]
Consistency [in PropiL]
context [in PropiL]
Cut [in PropiL]
CVars [in PropiLFmodel]
c2f [in PropiL]
C2PC [in PropiLFmodel]


D

dec [in Base]
decision [in Base]
Demo [in PropiLFmodel]
depth [in PropiL]
dequi [in PropiLFmodel]
disjoint [in Base]
dsub [in PropiLFmodel]
dupfree_inv [in Base]
dupfree_inv [in Base]
D2FKM [in PropiLFmodel2]


E

EntailRelAllProps [in PropiL]
eqH [in PropiLmodel]
eqH [in PropiLmodel]
Equi [in PropiL]
equi [in Base]
evalFK [in PropiLFmodel]
evalH [in PropiLmodel]
evalH [in PropiLmodel]
evalH' [in PropiLmodel]
evalH' [in PropiLmodel]
evalK [in PropiLmodel]
evalK [in PropiLmodel]
evalKA [in PropiLmodel]
evalKA [in PropiLmodel]
evalTK [in PropiLFmodel]
evalTK' [in PropiLFmodel]


F

FalFree [in PropiL]
FCI.C [in Base]
FCI.C [in Base]
FCI.F [in Base]
FCI.F [in Base]
filter [in Base]
FImp [in PropiLFmodel]
FImpList [in PropiLFmodel]
FK [in PropiL]
FKImp [in PropiLFmodel]
FK2K [in PropiLFmodel]
FormHA [in PropiLmodel]
FormHA [in PropiLmodel]
FP [in Base]
FS [in PropiL]


G

Gamma [in PropiL]
goal [in PropiL]


H

hent [in PropiLmodel]
hent [in PropiLmodel]
Hintikka [in PropiLFmodel]


I

ImpFree [in PropiL]
inclp [in Base]
inter [in PropiLFmodel]
interpTK [in PropiLFmodel]
it [in Base]


K

K_Peirce [in PropiLFmodel]
K_DN [in PropiLFmodel]
K_XM [in PropiLFmodel]
K_neg [in PropiLFmodel]
K_orxy [in PropiLFmodel]
K_var [in PropiLFmodel]
K_Fal [in PropiLFmodel]
K2H [in PropiLmodel]
K2H [in PropiLmodel]
K2Hinterp [in PropiLmodel]
K2Hinterp [in PropiLmodel]


L

Lambda [in PropiL]
lfpTab [in PropiLFmodel]
ltr [in PropiLmodel]
ltr [in PropiLmodel]


M

maxext [in PropiLFmodel2]
Monotonicity [in PropiL]


N

negative [in PropiL]
negImp [in PropiLFmodel2]
negImp [in PropiLFmodel2]
Not [in PropiL]


O

OrAR [in PropiL]
OrFree [in PropiL]


P

PContext [in PropiLFmodel]
PC2C [in PropiLFmodel]
pos [in PropiLFmodel]
positive [in PropiL]
posVar [in PropiLFmodel2]
posVars [in PropiLFmodel2]
power [in Base]
power [in Base]
pVar_nImp [in PropiLFmodel2]
pVar_nImp [in PropiLFmodel2]


Q

qmax [in PropiLFmodel2]


R

RC [in PropiLFmodel]
RCinterp [in PropiLFmodel]
RCList [in PropiLFmodel]
Reflexivity [in PropiL]
rem [in Base]
rep [in Base]
rep [in Base]
RList [in PropiLFmodel]
RTC [in PropiLFmodel]


S

satC [in PropiLFmodel2]
satisD [in PropiLFmodel]
satisDFK [in PropiLFmodel2]
satisFK [in PropiLFmodel]
satisFK' [in PropiLFmodel]
scl [in PropiL]
scl' [in PropiL]
sfs [in PropiLFmodel2]
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]
state [in PropiLFmodel]
step [in PropiL]
stepFKImp [in PropiLFmodel]
stepImp [in PropiLFmodel]
stepRList [in PropiLFmodel]
stepRTC [in PropiLFmodel]
stepTab [in PropiLFmodel]
stepTab' [in PropiLFmodel]
stepUC [in PropiLFmodel]
subPC [in PropiLFmodel]
subPos [in PropiLFmodel2]
subPos [in PropiLFmodel2]
subst [in PropiL]
Substitution [in PropiL]
sup [in PropiLFmodel]
s2b [in PropiL]


T

TK [in PropiLFmodel]
top [in PropiLmodel]
top [in PropiLmodel]
trip [in PropiLFmodel]
truthVal [in PropiLFmodel]


U

U [in PropiL]
UCS [in PropiLFmodel]
UCSE [in PropiLFmodel]
ucsPred [in PropiLFmodel]
undup [in Base]
undup [in Base]
union [in PropiLFmodel]
uns [in PropiL]
upset [in PropiLFmodel]
U_sfc [in PropiL]


V

var [in PropiL]
Vf [in PropiLmodel]
Vf [in PropiLmodel]



Record Index

F

FiniteKripkeModel [in PropiLFmodel]


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 (876 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 (108 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 (5 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 (381 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 (53 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 (42 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 (8 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 (49 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 (43 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 (173 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 (5 entries)

This page has been generated by coqdoc