Global Index

other

(647 entries)

Notation Index

other

(7 entries)

Module Index

other

(2 entries)

Variable Index

other

(69 entries)

Library Index

other

(4 entries)

Lemma Index

other

(284 entries)

Constructor Index

other

(60 entries)

Projection Index

other

(36 entries)

Inductive Index

other

(10 entries)

Section Index

other

(33 entries)

Instance Index

other

(28 entries)

Definition Index

other

(110 entries)

Record Index

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

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

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]