| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (681 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (35 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (363 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (100 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (31 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (24 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (92 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
Global Index
A
And [constructor, in PropiL]AndFree [definition, in PropiL]
and_dec [instance, in Base]
app_equi_proper [instance, in Base]
app_incl_proper [instance, in Base]
assn [definition, in PropcL]
B
Base [library]bent [definition, in PropcL]
bent_iff_unsat [lemma, in PropcL]
bool_eq_dec [instance, in Base]
b2s [definition, in PropiL]
C
card [definition, in Base]Cardinality [section, in Base]
Cardinality.X [variable, in Base]
card_equi_proper [instance, in Base]
card_or [lemma, in Base]
card_lt [lemma, in Base]
card_equi [lemma, in Base]
card_ex [lemma, in Base]
card_0 [lemma, in Base]
card_cons_rem [lemma, in Base]
card_eq [lemma, in Base]
card_le [lemma, in Base]
card_not_in_rem [lemma, in Base]
card_in_rem [lemma, in Base]
cent [definition, in PropcL]
cent_solved_sat [lemma, in PropcL]
cent_sat [lemma, in PropcL]
cent_weak [lemma, in PropcL]
CharAnd [definition, in PropiL]
CharFal [definition, in PropiL]
CharImp [definition, in PropiL]
CharOr [definition, in PropiL]
clause [definition, in PropiL]
Consistency [definition, in PropiL]
cons_equi_proper [instance, in Base]
cons_incl_proper [instance, in Base]
context [definition, in PropiL]
Cut [definition, in PropiL]
c2f [definition, in PropiL]
D
dec [definition, in Base]Decidability [section, in PropiL]
Decidability_GK3c.B0 [variable, in PropcL]
Decidability_GK3c.A0 [variable, in PropcL]
Decidability_GK3c [section, in PropcL]
Decidability.A0 [variable, in PropiL]
Decidability.s0 [variable, in PropiL]
decider [definition, in PropcL]
decision [definition, in Base]
dec_prop_iff [lemma, in Base]
dec_DM_impl [lemma, in Base]
dec_DM_and [lemma, in Base]
dec_DN [lemma, in Base]
depth [definition, in PropiL]
disjoint [definition, in Base]
disjoint_app [lemma, in Base]
disjoint_cons [lemma, in Base]
disjoint_nil' [lemma, in Base]
disjoint_nil [lemma, in Base]
disjoint_incl [lemma, in Base]
disjoint_symm [lemma, in Base]
disjoint_forall [lemma, in Base]
DM_exists [lemma, in Base]
DM_or [lemma, in Base]
DNF [definition, in PropcL]
Dupfree [section, in Base]
dupfree [inductive, in Base]
Dupfree [section, in Base]
dupfree [inductive, in Base]
dupfreeC [constructor, in Base]
dupfreeC [constructor, in Base]
dupfreeN [constructor, in Base]
dupfreeN [constructor, in Base]
dupfree_inv [definition, in Base]
dupfree_in_power [lemma, in Base]
dupfree_power [lemma, in Base]
dupfree_undup [lemma, in Base]
dupfree_card [lemma, in Base]
dupfree_dec [lemma, in Base]
dupfree_filter [lemma, in Base]
dupfree_map [lemma, in Base]
dupfree_app [lemma, in Base]
dupfree_cons [lemma, in Base]
dupfree_inv [definition, in Base]
dupfree_in_power [lemma, in Base]
dupfree_power [lemma, in Base]
dupfree_undup [lemma, in Base]
dupfree_card [lemma, in Base]
dupfree_dec [lemma, in Base]
dupfree_filter [lemma, in Base]
dupfree_map [lemma, in Base]
dupfree_app [lemma, in Base]
dupfree_cons [lemma, in Base]
Dupfree.X [variable, in Base]
Dupfree.X [variable, in Base]
E
EntailmentRelationProperties [section, in PropiL]EntailmentRelationProperties.E [variable, in PropiL]
EntailmentRelationProperties.F [variable, in PropiL]
EntailRelAllProps [definition, in PropiL]
EntailRelAllProps_ext [lemma, in PropiL]
Equi [definition, in PropiL]
Equi [section, in Base]
equi [definition, in Base]
equi_rotate [lemma, in Base]
equi_shift [lemma, in Base]
equi_swap [lemma, in Base]
equi_dup [lemma, in Base]
equi_push [lemma, in Base]
equi_Equivalence [instance, in Base]
Equi.X [variable, in Base]
eval [definition, in PropcL]
F
Fal [constructor, in PropiL]FalFree [definition, in PropiL]
False_dec [instance, in Base]
FCI [module, in Base]
FCI [module, in Base]
FCI.C [definition, in Base]
FCI.C [definition, in Base]
FCI.closure [lemma, in Base]
FCI.closure [lemma, in Base]
FCI.F [definition, in Base]
FCI.F [definition, in Base]
FCI.FCI [section, in Base]
FCI.FCI [section, in Base]
FCI.FCI.step [variable, in Base]
FCI.FCI.step [variable, in Base]
FCI.FCI.V [variable, in Base]
FCI.FCI.V [variable, in Base]
FCI.FCI.X [variable, in Base]
FCI.FCI.X [variable, in Base]
FCI.fp [lemma, in Base]
FCI.fp [lemma, in Base]
FCI.incl [lemma, in Base]
FCI.incl [lemma, in Base]
FCI.ind [lemma, in Base]
FCI.ind [lemma, in Base]
FCI.it_incl [lemma, in Base]
FCI.it_incl [lemma, in Base]
FCI.pick [lemma, in Base]
FCI.pick [lemma, in Base]
filter [definition, in Base]
FilterComm [section, in Base]
FilterComm.p [variable, in Base]
FilterComm.q [variable, in Base]
FilterComm.X [variable, in Base]
FilterLemmas [section, in Base]
FilterLemmas_pq.q [variable, in Base]
FilterLemmas_pq.p [variable, in Base]
FilterLemmas_pq.X [variable, in Base]
FilterLemmas_pq [section, in Base]
FilterLemmas.p [variable, in Base]
FilterLemmas.X [variable, in Base]
filter_comm [lemma, in Base]
filter_and [lemma, in Base]
filter_pq_eq [lemma, in Base]
filter_pq_mono [lemma, in Base]
filter_fst' [lemma, in Base]
filter_fst [lemma, in Base]
filter_app [lemma, in Base]
filter_id [lemma, in Base]
filter_mono [lemma, in Base]
filter_incl [lemma, in Base]
FK [definition, in PropiL]
form [inductive, in PropiL]
form_eq_dec [instance, in PropiL]
FP [definition, in Base]
FS [definition, in PropiL]
G
Gamma [definition, in PropiL]Gammac [definition, in PropcL]
gen [inductive, in PropiL]
genA [lemma, in PropiL]
genAL [constructor, in PropiL]
genAR [constructor, in PropiL]
genCW [lemma, in PropiL]
genF [constructor, in PropiL]
genIL [constructor, in PropiL]
genIR [constructor, in PropiL]
genOL [constructor, in PropiL]
genOR1 [constructor, in PropiL]
genOR2 [constructor, in PropiL]
genV [constructor, in PropiL]
genW [lemma, in PropiL]
gen_DN [lemma, in PropiL]
gen_DN' [lemma, in PropiL]
gen_lambda [lemma, in PropiL]
gen_iff_tab [lemma, in PropiL]
gen_tab [lemma, in PropiL]
gen_iff_nd [lemma, in PropiL]
gen_nd [lemma, in PropiL]
gen_NoNVar [lemma, in PropiL]
gen_NoVar [lemma, in PropiL]
gen_EntailRelation [lemma, in PropiL]
gen_subst [lemma, in PropiL]
gen_or [lemma, in PropiL]
gen_and_both [lemma, in PropiL]
gen_and [lemma, in PropiL]
gen_fal [lemma, in PropiL]
gen_imp [lemma, in PropiL]
gen_cons [lemma, in PropiL]
gen_NoFal [lemma, in PropiL]
gen_cut [lemma, in PropiL]
gen_GCut [lemma, in PropiL]
gen_mono [lemma, in PropiL]
gk3c [inductive, in PropcL]
gk3cA [lemma, in PropcL]
gk3cAL [constructor, in PropcL]
gk3cAR [constructor, in PropcL]
gk3cC [constructor, in PropcL]
gk3cCut [definition, in PropcL]
gk3cCutE [lemma, in PropcL]
gk3cCut_iff_ndc [lemma, in PropcL]
gk3cDNL [lemma, in PropcL]
gk3cDNL_iff [lemma, in PropcL]
gk3cDNL_inv [lemma, in PropcL]
gk3cDNL_invCut [lemma, in PropcL]
gk3cDNR [lemma, in PropcL]
gk3cDNR_iff [lemma, in PropcL]
gk3cDNR_inv [lemma, in PropcL]
gk3cDNR_invCut [lemma, in PropcL]
gk3cE [lemma, in PropcL]
gk3cF [constructor, in PropcL]
gk3cFL [lemma, in PropcL]
gk3cFL_iff [lemma, in PropcL]
gk3cFL_inv [lemma, in PropcL]
gk3cFL_invCut [lemma, in PropcL]
gk3cFR [lemma, in PropcL]
gk3cFR_iff [lemma, in PropcL]
gk3cFR_inv [lemma, in PropcL]
gk3cFR_invCut [lemma, in PropcL]
gk3cIL [constructor, in PropcL]
gk3cIR [constructor, in PropcL]
gk3cLC [lemma, in PropcL]
gk3cLW [lemma, in PropcL]
gk3cOL [constructor, in PropcL]
gk3cOR [constructor, in PropcL]
gk3cRC [lemma, in PropcL]
gk3cRW [lemma, in PropcL]
gk3cTF [lemma, in PropcL]
gk3cTF' [lemma, in PropcL]
gk3cW [lemma, in PropcL]
gk3c_iff_sem [lemma, in PropcL]
gk3c_dec_ref [lemma, in PropcL]
gk3c_refute [lemma, in PropcL]
gk3c_bent [lemma, in PropcL]
gk3c_bentG [lemma, in PropcL]
gk3c_dec [lemma, in PropcL]
gk3c_iff_sem [lemma, in PropcL]
gk3c_dec_ref [lemma, in PropcL]
gk3c_refute [lemma, in PropcL]
gk3c_bent [lemma, in PropcL]
gk3c_bentG [lemma, in PropcL]
gk3c_dec [lemma, in PropcL]
gk3c_lambdac [lemma, in PropcL]
gk3c_tab_NegImpFree [lemma, in PropcL]
gk3c_tab_NegImpFreeG [lemma, in PropcL]
gk3c_tab_ImpFreeG [lemma, in PropcL]
gk3c_iff_ndc [lemma, in PropcL]
gk3c_Cut [lemma, in PropcL]
gk3c_GCut [lemma, in PropcL]
gk3c_GCut_Fal [lemma, in PropcL]
gk3c_GCut_Var [lemma, in PropcL]
gk3c_Peirce_Cut [definition, in PropcL]
gk3c_Cut [section, in PropcL]
gk3c_ndc [lemma, in PropcL]
gk3c_ndcG [lemma, in PropcL]
gk3c_NV [lemma, in PropcL]
gk3c_NV' [lemma, in PropcL]
gk3c_con [lemma, in PropcL]
gk3c_NF [lemma, in PropcL]
gk3c_NF1 [lemma, in PropcL]
gk3c_NF' [lemma, in PropcL]
gk3c_emptyR [lemma, in PropcL]
Glivenko [lemma, in PropcL]
Glivenko_refute [lemma, in PropcL]
goal [definition, in PropiL]
goalc [definition, in PropcL]
goalc_eq_dec [instance, in PropcL]
goal_eq_dec [instance, in PropiL]
H
hil [inductive, in PropiL]hilA [constructor, in PropiL]
hilAI [constructor, in PropiL]
hilAK [lemma, in PropiL]
hilAL [constructor, in PropiL]
hilAR [constructor, in PropiL]
hilAS [lemma, in PropiL]
hilc [inductive, in PropcL]
hilc [inductive, in PropcL]
hilcA [constructor, in PropcL]
hilcA [constructor, in PropcL]
hilcAI [constructor, in PropcL]
hilcAI [constructor, in PropcL]
hilcAK [lemma, in PropcL]
hilcAK [lemma, in PropcL]
hilcAL [constructor, in PropcL]
hilcAL [constructor, in PropcL]
hilcAR [constructor, in PropcL]
hilcAR [constructor, in PropcL]
hilcAS [lemma, in PropcL]
hilcAS [lemma, in PropcL]
hilcD [lemma, in PropcL]
hilcD [lemma, in PropcL]
hilcDN [constructor, in PropcL]
hilcDN [constructor, in PropcL]
hilcI [lemma, in PropcL]
hilcI [lemma, in PropcL]
hilcK [constructor, in PropcL]
hilcK [constructor, in PropcL]
hilcMP [constructor, in PropcL]
hilcMP [constructor, in PropcL]
hilcOE [constructor, in PropcL]
hilcOE [constructor, in PropcL]
hilcOL [constructor, in PropcL]
hilcOL [constructor, in PropcL]
hilcOR [constructor, in PropcL]
hilcOR [constructor, in PropcL]
hilcS [constructor, in PropcL]
hilcS [constructor, in PropcL]
hilc_iff_ndc [lemma, in PropcL]
hilc_ndc [lemma, in PropcL]
hilc_iff_ndc [lemma, in PropcL]
hilc_ndc [lemma, in PropcL]
hilD [lemma, in PropiL]
hilE [constructor, in PropiL]
hilI [lemma, in PropiL]
hilK [constructor, in PropiL]
hilMP [constructor, in PropiL]
hilOE [constructor, in PropiL]
hilOL [constructor, in PropiL]
hilOR [constructor, in PropiL]
hilS [constructor, in PropiL]
hil_iff_nd [lemma, in PropiL]
hil_nd [lemma, in PropiL]
I
iff_dec [instance, in Base]Imp [constructor, in PropiL]
ImpFree [definition, in PropiL]
ImpFreeA [definition, in PropcL]
impl_dec [instance, in Base]
inclp [definition, in Base]
Inclusion [section, in Base]
Inclusion.X [variable, in Base]
incl_equi_proper [instance, in Base]
incl_preorder [instance, in Base]
incl_app_left [lemma, in Base]
incl_lrcons [lemma, in Base]
incl_rcons [lemma, in Base]
incl_sing [lemma, in Base]
incl_lcons [lemma, in Base]
incl_shift [lemma, in Base]
incl_nil_eq [lemma, in Base]
incl_map [lemma, in Base]
incl_nil [lemma, in Base]
in_rem_iff [lemma, in Base]
in_filter_iff [lemma, in Base]
in_equi_proper [instance, in Base]
in_incl_proper [instance, in Base]
in_cons_neq [lemma, in Base]
in_sing [lemma, in Base]
it [definition, in Base]
Iteration [section, in Base]
Iteration.f [variable, in Base]
Iteration.X [variable, in Base]
it_fp [lemma, in Base]
it_ind [lemma, in Base]
L
Lambda [definition, in PropiL]Lambdac [definition, in PropcL]
lambdac_gk3c [lemma, in PropcL]
lambdac_gk3c [lemma, in PropcL]
lambdac_ind [lemma, in PropcL]
lambdac_closure [lemma, in PropcL]
lambda_gen [lemma, in PropiL]
lambda_ind [lemma, in PropiL]
lambda_closure [lemma, in PropiL]
list_cc [lemma, in Base]
list_exists_not_incl [lemma, in Base]
list_exists_DM [lemma, in Base]
list_exists_dec [instance, in Base]
list_forall_dec [instance, in Base]
list_sigma_forall [lemma, in Base]
list_in_dec [instance, in Base]
list_eq_dec [instance, in Base]
list_cycle [lemma, in Base]
M
Membership [section, in Base]Membership.X [variable, in Base]
Monotonicity [definition, in PropiL]
N
nat_le_dec [instance, in Base]nat_eq_dec [instance, in Base]
nd [inductive, in PropiL]
ndA [constructor, in PropiL]
ndAE [constructor, in PropiL]
ndAI [constructor, in PropiL]
ndc [inductive, in PropcL]
ndcA [constructor, in PropcL]
ndcAE [constructor, in PropcL]
ndcAI [constructor, in PropcL]
ndcC [constructor, in PropcL]
ndcE [lemma, in PropcL]
ndcIE [constructor, in PropcL]
ndcII [constructor, in PropcL]
ndcOE [constructor, in PropcL]
ndcOIL [constructor, in PropcL]
ndcOIR [constructor, in PropcL]
ndcW [lemma, in PropcL]
ndCW [lemma, in PropiL]
ndcW1 [lemma, in PropcL]
ndc_hilc [lemma, in PropcL]
ndc_dec_gk3c [lemma, in PropcL]
ndc_hilc [lemma, in PropcL]
ndc_dec_gk3c [lemma, in PropcL]
ndc_gk3c [lemma, in PropcL]
ndc_gk3cCut [lemma, in PropcL]
ndc_iff_sem [lemma, in PropcL]
ndc_dec_bent [lemma, in PropcL]
ndc_EntailRelation [lemma, in PropcL]
ndc_cons [lemma, in PropcL]
ndc_bent [lemma, in PropcL]
ndc_refute [lemma, in PropcL]
ndc_subst [lemma, in PropcL]
ndc_or [lemma, in PropcL]
ndc_and [lemma, in PropcL]
ndc_fal [lemma, in PropcL]
ndc_imp [lemma, in PropcL]
ndc_cut [lemma, in PropcL]
ndc_mono [lemma, in PropcL]
ndc_refl [lemma, in PropcL]
ndDN [lemma, in PropcL]
ndE [constructor, in PropiL]
ndIE [constructor, in PropiL]
ndII [constructor, in PropiL]
ndOE [constructor, in PropiL]
ndOIL [constructor, in PropiL]
ndOIR [constructor, in PropiL]
ndW [lemma, in PropiL]
nd_ndc_NegImpFree [lemma, in PropcL]
nd_ndc_ImpFree [lemma, in PropcL]
nd_embeds_ndc [lemma, in PropcL]
nd_ndc [lemma, in PropcL]
nd_dec [lemma, in PropiL]
nd_OrARcut [lemma, in PropiL]
nd_OrCut [lemma, in PropiL]
nd_hil [lemma, in PropiL]
nd_onesided [lemma, in PropiL]
nd_EntailRelation [lemma, in PropiL]
nd_cons [lemma, in PropiL]
nd_NoFal [lemma, in PropiL]
nd_gen [lemma, in PropiL]
nd_subst [lemma, in PropiL]
nd_or [lemma, in PropiL]
nd_and [lemma, in PropiL]
nd_fal [lemma, in PropiL]
nd_imp [lemma, in PropiL]
nd_cut [lemma, in PropiL]
nd_mono [lemma, in PropiL]
nd_refl [lemma, in PropiL]
neg [definition, in PropcL]
Neg [constructor, in PropiL]
negative [definition, in PropiL]
neg_incl [lemma, in PropcL]
neg_in [lemma, in PropcL]
Not [definition, in PropiL]
not_in_cons [lemma, in Base]
not_dec [instance, in Base]
O
Or [constructor, in PropiL]OrAR [definition, in PropiL]
OrAR_mono_nd [lemma, in PropiL]
OrAR_mono [lemma, in PropiL]
OrFree [definition, in PropiL]
or_dec [instance, in Base]
P
phi [definition, in PropcL]Pos [constructor, in PropiL]
positive [definition, in PropiL]
power [definition, in Base]
power [definition, in Base]
PowerRep [section, in Base]
PowerRep [section, in Base]
PowerRep.X [variable, in Base]
PowerRep.X [variable, in Base]
power_extensional [lemma, in Base]
power_nil [lemma, in Base]
power_incl [lemma, in Base]
power_extensional [lemma, in Base]
power_nil [lemma, in Base]
power_incl [lemma, in Base]
PropcL [library]
PropiL [library]
provider [definition, in PropcL]
R
rec [inductive, in PropcL]recNA [constructor, in PropcL]
recNF [constructor, in PropcL]
recNI [constructor, in PropcL]
recNil [constructor, in PropcL]
recNO [constructor, in PropcL]
recNV [constructor, in PropcL]
recNV' [constructor, in PropcL]
recPA [constructor, in PropcL]
recPF [constructor, in PropcL]
recPI [constructor, in PropcL]
recPO [constructor, in PropcL]
recPV [constructor, in PropcL]
recPV' [constructor, in PropcL]
Reflexivity [definition, in PropiL]
refutation [lemma, in PropcL]
ref_gk3c [lemma, in PropcL]
ref_gk3c [lemma, in PropcL]
ref_dec [lemma, in PropcL]
ref_iff_unsat [lemma, in PropcL]
ref_ndc [lemma, in PropcL]
ref_unsat [lemma, in PropcL]
ref_sound [projection, in PropcL]
ref_neg_or [projection, in PropcL]
ref_pos_or [projection, in PropcL]
ref_neg_and [projection, in PropcL]
ref_pos_and [projection, in PropcL]
ref_neg_imp [projection, in PropcL]
ref_pos_imp [projection, in PropcL]
ref_clash [projection, in PropcL]
ref_weak [projection, in PropcL]
ref_Fal [projection, in PropcL]
ref_pred [record, in PropcL]
rem [definition, in Base]
Removal [section, in Base]
Removal.X [variable, in Base]
rem_inclr [lemma, in Base]
rem_reorder [lemma, in Base]
rem_id [lemma, in Base]
rem_fst' [lemma, in Base]
rem_fst [lemma, in Base]
rem_comm [lemma, in Base]
rem_equi [lemma, in Base]
rem_app' [lemma, in Base]
rem_app [lemma, in Base]
rem_neq [lemma, in Base]
rem_in [lemma, in Base]
rem_cons' [lemma, in Base]
rem_cons [lemma, in Base]
rem_mono [lemma, in Base]
rem_incl [lemma, in Base]
rem_not_in [lemma, in Base]
rep [definition, in Base]
rep [definition, in Base]
rep_dupfree [lemma, in Base]
rep_idempotent [lemma, in Base]
rep_injective [lemma, in Base]
rep_eq [lemma, in Base]
rep_eq' [lemma, in Base]
rep_mono [lemma, in Base]
rep_equi [lemma, in Base]
rep_in [lemma, in Base]
rep_incl [lemma, in Base]
rep_power [lemma, in Base]
rep_dupfree [lemma, in Base]
rep_idempotent [lemma, in Base]
rep_injective [lemma, in Base]
rep_eq [lemma, in Base]
rep_eq' [lemma, in Base]
rep_mono [lemma, in Base]
rep_equi [lemma, in Base]
rep_in [lemma, in Base]
rep_incl [lemma, in Base]
rep_power [lemma, in Base]
RL [section, in PropcL]
RL.Rho [variable, in PropcL]
RL.rho [variable, in PropcL]
S
sat [definition, in PropcL]satis [definition, in PropcL]
satis_pos [lemma, in PropcL]
satis_weak [lemma, in PropcL]
satis_in [lemma, in PropcL]
satis_iff [lemma, in PropcL]
satis_neg_or [lemma, in PropcL]
satis_pos_or [lemma, in PropcL]
satis_neg_and [lemma, in PropcL]
satis_pos_and [lemma, in PropcL]
satis_neg_imp [lemma, in PropcL]
satis_pos_imp [lemma, in PropcL]
satis_eval [lemma, in PropcL]
satis_dec [instance, in PropcL]
satis' [definition, in PropcL]
sat_weak [lemma, in PropcL]
scl [definition, in PropiL]
scl_closed [lemma, in PropiL]
scl_incl [lemma, in PropiL]
scl_incl' [lemma, in PropiL]
scl' [definition, in PropiL]
scl'_closed [lemma, in PropiL]
scl'_in [lemma, in PropiL]
sform [inductive, in PropiL]
sform_eq_dec [instance, in PropiL]
sf_closed_cons [lemma, in PropiL]
sf_closed_app [lemma, in PropiL]
sf_closed [definition, in PropiL]
size [definition, in PropiL]
sizeF [definition, in PropiL]
size_recursion [lemma, in Base]
solved [definition, in PropcL]
solved_ref [lemma, in PropcL]
solved_neg_var [lemma, in PropcL]
solved_pos_var [lemma, in PropcL]
solved_nil [lemma, in PropcL]
solved_sat' [lemma, in PropcL]
solved_sat [lemma, in PropcL]
solved_phi [lemma, in PropcL]
ssL [definition, in PropiL]
ssL [section, in PropiL]
ssLb [definition, in PropiL]
ssL_nd_ndc [section, in PropcL]
ssL_idempotent [lemma, in PropiL]
ssL_app [lemma, in PropiL]
ssL_mono [lemma, in PropiL]
ssL_in [lemma, in PropiL]
ssL_correct [lemma, in PropiL]
ssL' [definition, in PropiL]
ssL'_in_ssL2 [lemma, in PropiL]
ssL'_in_ssL [lemma, in PropiL]
ssL'_correct [lemma, in PropiL]
ssL'_in [lemma, in PropiL]
ssL'_self [lemma, in PropiL]
ss_closed_app [lemma, in PropiL]
ss_closed'_mono [lemma, in PropiL]
ss_closed [definition, in PropiL]
ss_closed' [definition, in PropiL]
step [definition, in PropiL]
stepc [definition, in PropcL]
stepc_dec [instance, in PropcL]
step_dec [instance, in PropiL]
subst [definition, in PropiL]
Substitution [definition, in PropiL]
svar [definition, in PropcL]
s2b [definition, in PropiL]
T
tab [inductive, in PropiL]tabAN [constructor, in PropiL]
tabAP [constructor, in PropiL]
tabC [constructor, in PropiL]
tabCS [lemma, in PropiL]
tabF [constructor, in PropiL]
tabIN [constructor, in PropiL]
tabIP [constructor, in PropiL]
tabLW [lemma, in PropiL]
tabON [constructor, in PropiL]
tabOP [constructor, in PropiL]
tabRW [lemma, in PropiL]
tabW [lemma, in PropiL]
tab_nd [lemma, in PropiL]
tab_ndG [lemma, in PropiL]
tab_gen [lemma, in PropiL]
tab_genG [lemma, in PropiL]
True_dec [instance, in Base]
U
U [definition, in PropiL]Uc [definition, in PropcL]
Uc_sfc [definition, in PropcL]
undup [definition, in Base]
Undup [section, in Base]
undup [definition, in Base]
Undup [section, in Base]
undup_idempotent [lemma, in Base]
undup_id [lemma, in Base]
undup_equi [lemma, in Base]
undup_incl [lemma, in Base]
undup_id_equi [lemma, in Base]
undup_idempotent [lemma, in Base]
undup_id [lemma, in Base]
undup_equi [lemma, in Base]
undup_incl [lemma, in Base]
undup_id_equi [lemma, in Base]
Undup.X [variable, in Base]
Undup.X [variable, in Base]
uns [definition, in PropiL]
uns_neg [lemma, in PropcL]
uns_neg [lemma, in PropcL]
uns_pos [lemma, in PropiL]
U_sfc [definition, in PropiL]
V
valid [definition, in PropcL]valid_unsat [lemma, in PropcL]
Var [constructor, in PropiL]
var [definition, in PropiL]
other
_ === _ [notation, in Base]_ <<= _ [notation, in Base]
_ el _ [notation, in Base]
eq_dec _ [notation, in Base]
+ _ [notation, in PropiL]
- _ [notation, in PropiL]
| _ | [notation, in Base]
Notation Index
other
_ === _ [in Base]_ <<= _ [in Base]
_ el _ [in Base]
eq_dec _ [in Base]
+ _ [in PropiL]
- _ [in PropiL]
| _ | [in Base]
Module Index
F
FCI [in Base]FCI [in Base]
Variable Index
C
Cardinality.X [in Base]D
Decidability_GK3c.B0 [in PropcL]Decidability_GK3c.A0 [in PropcL]
Decidability.A0 [in PropiL]
Decidability.s0 [in PropiL]
Dupfree.X [in Base]
Dupfree.X [in Base]
E
EntailmentRelationProperties.E [in PropiL]EntailmentRelationProperties.F [in PropiL]
Equi.X [in Base]
F
FCI.FCI.step [in Base]FCI.FCI.step [in Base]
FCI.FCI.V [in Base]
FCI.FCI.V [in Base]
FCI.FCI.X [in Base]
FCI.FCI.X [in Base]
FilterComm.p [in Base]
FilterComm.q [in Base]
FilterComm.X [in Base]
FilterLemmas_pq.q [in Base]
FilterLemmas_pq.p [in Base]
FilterLemmas_pq.X [in Base]
FilterLemmas.p [in Base]
FilterLemmas.X [in Base]
I
Inclusion.X [in Base]Iteration.f [in Base]
Iteration.X [in Base]
M
Membership.X [in Base]P
PowerRep.X [in Base]PowerRep.X [in Base]
R
Removal.X [in Base]RL.Rho [in PropcL]
RL.rho [in PropcL]
U
Undup.X [in Base]Undup.X [in Base]
Library Index
B
BaseP
PropcLPropiL
Lemma Index
B
bent_iff_unsat [in PropcL]C
card_or [in Base]card_lt [in Base]
card_equi [in Base]
card_ex [in Base]
card_0 [in Base]
card_cons_rem [in Base]
card_eq [in Base]
card_le [in Base]
card_not_in_rem [in Base]
card_in_rem [in Base]
cent_solved_sat [in PropcL]
cent_sat [in PropcL]
cent_weak [in PropcL]
D
dec_prop_iff [in Base]dec_DM_impl [in Base]
dec_DM_and [in Base]
dec_DN [in Base]
disjoint_app [in Base]
disjoint_cons [in Base]
disjoint_nil' [in Base]
disjoint_nil [in Base]
disjoint_incl [in Base]
disjoint_symm [in Base]
disjoint_forall [in Base]
DM_exists [in Base]
DM_or [in Base]
dupfree_in_power [in Base]
dupfree_power [in Base]
dupfree_undup [in Base]
dupfree_card [in Base]
dupfree_dec [in Base]
dupfree_filter [in Base]
dupfree_map [in Base]
dupfree_app [in Base]
dupfree_cons [in Base]
dupfree_in_power [in Base]
dupfree_power [in Base]
dupfree_undup [in Base]
dupfree_card [in Base]
dupfree_dec [in Base]
dupfree_filter [in Base]
dupfree_map [in Base]
dupfree_app [in Base]
dupfree_cons [in Base]
E
EntailRelAllProps_ext [in PropiL]equi_rotate [in Base]
equi_shift [in Base]
equi_swap [in Base]
equi_dup [in Base]
equi_push [in Base]
F
FCI.closure [in Base]FCI.closure [in Base]
FCI.fp [in Base]
FCI.fp [in Base]
FCI.incl [in Base]
FCI.incl [in Base]
FCI.ind [in Base]
FCI.ind [in Base]
FCI.it_incl [in Base]
FCI.it_incl [in Base]
FCI.pick [in Base]
FCI.pick [in Base]
filter_comm [in Base]
filter_and [in Base]
filter_pq_eq [in Base]
filter_pq_mono [in Base]
filter_fst' [in Base]
filter_fst [in Base]
filter_app [in Base]
filter_id [in Base]
filter_mono [in Base]
filter_incl [in Base]
G
genA [in PropiL]genCW [in PropiL]
genW [in PropiL]
gen_DN [in PropiL]
gen_DN' [in PropiL]
gen_lambda [in PropiL]
gen_iff_tab [in PropiL]
gen_tab [in PropiL]
gen_iff_nd [in PropiL]
gen_nd [in PropiL]
gen_NoNVar [in PropiL]
gen_NoVar [in PropiL]
gen_EntailRelation [in PropiL]
gen_subst [in PropiL]
gen_or [in PropiL]
gen_and_both [in PropiL]
gen_and [in PropiL]
gen_fal [in PropiL]
gen_imp [in PropiL]
gen_cons [in PropiL]
gen_NoFal [in PropiL]
gen_cut [in PropiL]
gen_GCut [in PropiL]
gen_mono [in PropiL]
gk3cA [in PropcL]
gk3cCutE [in PropcL]
gk3cCut_iff_ndc [in PropcL]
gk3cDNL [in PropcL]
gk3cDNL_iff [in PropcL]
gk3cDNL_inv [in PropcL]
gk3cDNL_invCut [in PropcL]
gk3cDNR [in PropcL]
gk3cDNR_iff [in PropcL]
gk3cDNR_inv [in PropcL]
gk3cDNR_invCut [in PropcL]
gk3cE [in PropcL]
gk3cFL [in PropcL]
gk3cFL_iff [in PropcL]
gk3cFL_inv [in PropcL]
gk3cFL_invCut [in PropcL]
gk3cFR [in PropcL]
gk3cFR_iff [in PropcL]
gk3cFR_inv [in PropcL]
gk3cFR_invCut [in PropcL]
gk3cLC [in PropcL]
gk3cLW [in PropcL]
gk3cRC [in PropcL]
gk3cRW [in PropcL]
gk3cTF [in PropcL]
gk3cTF' [in PropcL]
gk3cW [in PropcL]
gk3c_iff_sem [in PropcL]
gk3c_dec_ref [in PropcL]
gk3c_refute [in PropcL]
gk3c_bent [in PropcL]
gk3c_bentG [in PropcL]
gk3c_dec [in PropcL]
gk3c_iff_sem [in PropcL]
gk3c_dec_ref [in PropcL]
gk3c_refute [in PropcL]
gk3c_bent [in PropcL]
gk3c_bentG [in PropcL]
gk3c_dec [in PropcL]
gk3c_lambdac [in PropcL]
gk3c_tab_NegImpFree [in PropcL]
gk3c_tab_NegImpFreeG [in PropcL]
gk3c_tab_ImpFreeG [in PropcL]
gk3c_iff_ndc [in PropcL]
gk3c_Cut [in PropcL]
gk3c_GCut [in PropcL]
gk3c_GCut_Fal [in PropcL]
gk3c_GCut_Var [in PropcL]
gk3c_ndc [in PropcL]
gk3c_ndcG [in PropcL]
gk3c_NV [in PropcL]
gk3c_NV' [in PropcL]
gk3c_con [in PropcL]
gk3c_NF [in PropcL]
gk3c_NF1 [in PropcL]
gk3c_NF' [in PropcL]
gk3c_emptyR [in PropcL]
Glivenko [in PropcL]
Glivenko_refute [in PropcL]
H
hilAK [in PropiL]hilAS [in PropiL]
hilcAK [in PropcL]
hilcAK [in PropcL]
hilcAS [in PropcL]
hilcAS [in PropcL]
hilcD [in PropcL]
hilcD [in PropcL]
hilcI [in PropcL]
hilcI [in PropcL]
hilc_iff_ndc [in PropcL]
hilc_ndc [in PropcL]
hilc_iff_ndc [in PropcL]
hilc_ndc [in PropcL]
hilD [in PropiL]
hilI [in PropiL]
hil_iff_nd [in PropiL]
hil_nd [in PropiL]
I
incl_app_left [in Base]incl_lrcons [in Base]
incl_rcons [in Base]
incl_sing [in Base]
incl_lcons [in Base]
incl_shift [in Base]
incl_nil_eq [in Base]
incl_map [in Base]
incl_nil [in Base]
in_rem_iff [in Base]
in_filter_iff [in Base]
in_cons_neq [in Base]
in_sing [in Base]
it_fp [in Base]
it_ind [in Base]
L
lambdac_gk3c [in PropcL]lambdac_gk3c [in PropcL]
lambdac_ind [in PropcL]
lambdac_closure [in PropcL]
lambda_gen [in PropiL]
lambda_ind [in PropiL]
lambda_closure [in PropiL]
list_cc [in Base]
list_exists_not_incl [in Base]
list_exists_DM [in Base]
list_sigma_forall [in Base]
list_cycle [in Base]
N
ndcE [in PropcL]ndcW [in PropcL]
ndCW [in PropiL]
ndcW1 [in PropcL]
ndc_hilc [in PropcL]
ndc_dec_gk3c [in PropcL]
ndc_hilc [in PropcL]
ndc_dec_gk3c [in PropcL]
ndc_gk3c [in PropcL]
ndc_gk3cCut [in PropcL]
ndc_iff_sem [in PropcL]
ndc_dec_bent [in PropcL]
ndc_EntailRelation [in PropcL]
ndc_cons [in PropcL]
ndc_bent [in PropcL]
ndc_refute [in PropcL]
ndc_subst [in PropcL]
ndc_or [in PropcL]
ndc_and [in PropcL]
ndc_fal [in PropcL]
ndc_imp [in PropcL]
ndc_cut [in PropcL]
ndc_mono [in PropcL]
ndc_refl [in PropcL]
ndDN [in PropcL]
ndW [in PropiL]
nd_ndc_NegImpFree [in PropcL]
nd_ndc_ImpFree [in PropcL]
nd_embeds_ndc [in PropcL]
nd_ndc [in PropcL]
nd_dec [in PropiL]
nd_OrARcut [in PropiL]
nd_OrCut [in PropiL]
nd_hil [in PropiL]
nd_onesided [in PropiL]
nd_EntailRelation [in PropiL]
nd_cons [in PropiL]
nd_NoFal [in PropiL]
nd_gen [in PropiL]
nd_subst [in PropiL]
nd_or [in PropiL]
nd_and [in PropiL]
nd_fal [in PropiL]
nd_imp [in PropiL]
nd_cut [in PropiL]
nd_mono [in PropiL]
nd_refl [in PropiL]
neg_incl [in PropcL]
neg_in [in PropcL]
not_in_cons [in Base]
O
OrAR_mono_nd [in PropiL]OrAR_mono [in PropiL]
P
power_extensional [in Base]power_nil [in Base]
power_incl [in Base]
power_extensional [in Base]
power_nil [in Base]
power_incl [in Base]
R
refutation [in PropcL]ref_gk3c [in PropcL]
ref_gk3c [in PropcL]
ref_dec [in PropcL]
ref_iff_unsat [in PropcL]
ref_ndc [in PropcL]
ref_unsat [in PropcL]
rem_inclr [in Base]
rem_reorder [in Base]
rem_id [in Base]
rem_fst' [in Base]
rem_fst [in Base]
rem_comm [in Base]
rem_equi [in Base]
rem_app' [in Base]
rem_app [in Base]
rem_neq [in Base]
rem_in [in Base]
rem_cons' [in Base]
rem_cons [in Base]
rem_mono [in Base]
rem_incl [in Base]
rem_not_in [in Base]
rep_dupfree [in Base]
rep_idempotent [in Base]
rep_injective [in Base]
rep_eq [in Base]
rep_eq' [in Base]
rep_mono [in Base]
rep_equi [in Base]
rep_in [in Base]
rep_incl [in Base]
rep_power [in Base]
rep_dupfree [in Base]
rep_idempotent [in Base]
rep_injective [in Base]
rep_eq [in Base]
rep_eq' [in Base]
rep_mono [in Base]
rep_equi [in Base]
rep_in [in Base]
rep_incl [in Base]
rep_power [in Base]
S
satis_pos [in PropcL]satis_weak [in PropcL]
satis_in [in PropcL]
satis_iff [in PropcL]
satis_neg_or [in PropcL]
satis_pos_or [in PropcL]
satis_neg_and [in PropcL]
satis_pos_and [in PropcL]
satis_neg_imp [in PropcL]
satis_pos_imp [in PropcL]
satis_eval [in PropcL]
sat_weak [in PropcL]
scl_closed [in PropiL]
scl_incl [in PropiL]
scl_incl' [in PropiL]
scl'_closed [in PropiL]
scl'_in [in PropiL]
sf_closed_cons [in PropiL]
sf_closed_app [in PropiL]
size_recursion [in Base]
solved_ref [in PropcL]
solved_neg_var [in PropcL]
solved_pos_var [in PropcL]
solved_nil [in PropcL]
solved_sat' [in PropcL]
solved_sat [in PropcL]
solved_phi [in PropcL]
ssL_idempotent [in PropiL]
ssL_app [in PropiL]
ssL_mono [in PropiL]
ssL_in [in PropiL]
ssL_correct [in PropiL]
ssL'_in_ssL2 [in PropiL]
ssL'_in_ssL [in PropiL]
ssL'_correct [in PropiL]
ssL'_in [in PropiL]
ssL'_self [in PropiL]
ss_closed_app [in PropiL]
ss_closed'_mono [in PropiL]
T
tabCS [in PropiL]tabLW [in PropiL]
tabRW [in PropiL]
tabW [in PropiL]
tab_nd [in PropiL]
tab_ndG [in PropiL]
tab_gen [in PropiL]
tab_genG [in PropiL]
U
undup_idempotent [in Base]undup_id [in Base]
undup_equi [in Base]
undup_incl [in Base]
undup_id_equi [in Base]
undup_idempotent [in Base]
undup_id [in Base]
undup_equi [in Base]
undup_incl [in Base]
undup_id_equi [in Base]
uns_neg [in PropcL]
uns_neg [in PropcL]
uns_pos [in PropiL]
V
valid_unsat [in PropcL]Constructor Index
A
And [in PropiL]D
dupfreeC [in Base]dupfreeC [in Base]
dupfreeN [in Base]
dupfreeN [in Base]
F
Fal [in PropiL]G
genAL [in PropiL]genAR [in PropiL]
genF [in PropiL]
genIL [in PropiL]
genIR [in PropiL]
genOL [in PropiL]
genOR1 [in PropiL]
genOR2 [in PropiL]
genV [in PropiL]
gk3cAL [in PropcL]
gk3cAR [in PropcL]
gk3cC [in PropcL]
gk3cF [in PropcL]
gk3cIL [in PropcL]
gk3cIR [in PropcL]
gk3cOL [in PropcL]
gk3cOR [in PropcL]
H
hilA [in PropiL]hilAI [in PropiL]
hilAL [in PropiL]
hilAR [in PropiL]
hilcA [in PropcL]
hilcA [in PropcL]
hilcAI [in PropcL]
hilcAI [in PropcL]
hilcAL [in PropcL]
hilcAL [in PropcL]
hilcAR [in PropcL]
hilcAR [in PropcL]
hilcDN [in PropcL]
hilcDN [in PropcL]
hilcK [in PropcL]
hilcK [in PropcL]
hilcMP [in PropcL]
hilcMP [in PropcL]
hilcOE [in PropcL]
hilcOE [in PropcL]
hilcOL [in PropcL]
hilcOL [in PropcL]
hilcOR [in PropcL]
hilcOR [in PropcL]
hilcS [in PropcL]
hilcS [in PropcL]
hilE [in PropiL]
hilK [in PropiL]
hilMP [in PropiL]
hilOE [in PropiL]
hilOL [in PropiL]
hilOR [in PropiL]
hilS [in PropiL]
I
Imp [in PropiL]N
ndA [in PropiL]ndAE [in PropiL]
ndAI [in PropiL]
ndcA [in PropcL]
ndcAE [in PropcL]
ndcAI [in PropcL]
ndcC [in PropcL]
ndcIE [in PropcL]
ndcII [in PropcL]
ndcOE [in PropcL]
ndcOIL [in PropcL]
ndcOIR [in PropcL]
ndE [in PropiL]
ndIE [in PropiL]
ndII [in PropiL]
ndOE [in PropiL]
ndOIL [in PropiL]
ndOIR [in PropiL]
Neg [in PropiL]
O
Or [in PropiL]P
Pos [in PropiL]R
recNA [in PropcL]recNF [in PropcL]
recNI [in PropcL]
recNil [in PropcL]
recNO [in PropcL]
recNV [in PropcL]
recNV' [in PropcL]
recPA [in PropcL]
recPF [in PropcL]
recPI [in PropcL]
recPO [in PropcL]
recPV [in PropcL]
recPV' [in PropcL]
T
tabAN [in PropiL]tabAP [in PropiL]
tabC [in PropiL]
tabF [in PropiL]
tabIN [in PropiL]
tabIP [in PropiL]
tabON [in PropiL]
tabOP [in PropiL]
V
Var [in PropiL]Inductive Index
D
dupfree [in Base]dupfree [in Base]
F
form [in PropiL]G
gen [in PropiL]gk3c [in PropcL]
H
hil [in PropiL]hilc [in PropcL]
hilc [in PropcL]
N
nd [in PropiL]ndc [in PropcL]
R
rec [in PropcL]S
sform [in PropiL]T
tab [in PropiL]Projection Index
R
ref_sound [in PropcL]ref_neg_or [in PropcL]
ref_pos_or [in PropcL]
ref_neg_and [in PropcL]
ref_pos_and [in PropcL]
ref_neg_imp [in PropcL]
ref_pos_imp [in PropcL]
ref_clash [in PropcL]
ref_weak [in PropcL]
ref_Fal [in PropcL]
Instance Index
A
and_dec [in Base]app_equi_proper [in Base]
app_incl_proper [in Base]
B
bool_eq_dec [in Base]C
card_equi_proper [in Base]cons_equi_proper [in Base]
cons_incl_proper [in Base]
E
equi_Equivalence [in Base]F
False_dec [in Base]form_eq_dec [in PropiL]
G
goalc_eq_dec [in PropcL]goal_eq_dec [in PropiL]
I
iff_dec [in Base]impl_dec [in Base]
incl_equi_proper [in Base]
incl_preorder [in Base]
in_equi_proper [in Base]
in_incl_proper [in Base]
L
list_exists_dec [in Base]list_forall_dec [in Base]
list_in_dec [in Base]
list_eq_dec [in Base]
N
nat_le_dec [in Base]nat_eq_dec [in Base]
not_dec [in Base]
O
or_dec [in Base]S
satis_dec [in PropcL]sform_eq_dec [in PropiL]
stepc_dec [in PropcL]
step_dec [in PropiL]
T
True_dec [in Base]Section Index
C
Cardinality [in Base]D
Decidability [in PropiL]Decidability_GK3c [in PropcL]
Dupfree [in Base]
Dupfree [in Base]
E
EntailmentRelationProperties [in PropiL]Equi [in Base]
F
FCI.FCI [in Base]FCI.FCI [in Base]
FilterComm [in Base]
FilterLemmas [in Base]
FilterLemmas_pq [in Base]
G
gk3c_Cut [in PropcL]I
Inclusion [in Base]Iteration [in Base]
M
Membership [in Base]P
PowerRep [in Base]PowerRep [in Base]
R
Removal [in Base]RL [in PropcL]
S
ssL [in PropiL]ssL_nd_ndc [in PropcL]
U
Undup [in Base]Undup [in Base]
Definition Index
A
AndFree [in PropiL]assn [in PropcL]
B
bent [in PropcL]b2s [in PropiL]
C
card [in Base]cent [in PropcL]
CharAnd [in PropiL]
CharFal [in PropiL]
CharImp [in PropiL]
CharOr [in PropiL]
clause [in PropiL]
Consistency [in PropiL]
context [in PropiL]
Cut [in PropiL]
c2f [in PropiL]
D
dec [in Base]decider [in PropcL]
decision [in Base]
depth [in PropiL]
disjoint [in Base]
DNF [in PropcL]
dupfree_inv [in Base]
dupfree_inv [in Base]
E
EntailRelAllProps [in PropiL]Equi [in PropiL]
equi [in Base]
eval [in PropcL]
F
FalFree [in PropiL]FCI.C [in Base]
FCI.C [in Base]
FCI.F [in Base]
FCI.F [in Base]
filter [in Base]
FK [in PropiL]
FP [in Base]
FS [in PropiL]
G
Gamma [in PropiL]Gammac [in PropcL]
gk3cCut [in PropcL]
gk3c_Peirce_Cut [in PropcL]
goal [in PropiL]
goalc [in PropcL]
I
ImpFree [in PropiL]ImpFreeA [in PropcL]
inclp [in Base]
it [in Base]
L
Lambda [in PropiL]Lambdac [in PropcL]
M
Monotonicity [in PropiL]N
neg [in PropcL]negative [in PropiL]
Not [in PropiL]
O
OrAR [in PropiL]OrFree [in PropiL]
P
phi [in PropcL]positive [in PropiL]
power [in Base]
power [in Base]
provider [in PropcL]
R
Reflexivity [in PropiL]rem [in Base]
rep [in Base]
rep [in Base]
S
sat [in PropcL]satis [in PropcL]
satis' [in PropcL]
scl [in PropiL]
scl' [in PropiL]
sf_closed [in PropiL]
size [in PropiL]
sizeF [in PropiL]
solved [in PropcL]
ssL [in PropiL]
ssLb [in PropiL]
ssL' [in PropiL]
ss_closed [in PropiL]
ss_closed' [in PropiL]
step [in PropiL]
stepc [in PropcL]
subst [in PropiL]
Substitution [in PropiL]
svar [in PropcL]
s2b [in PropiL]
U
U [in PropiL]Uc [in PropcL]
Uc_sfc [in PropcL]
undup [in Base]
undup [in Base]
uns [in PropiL]
U_sfc [in PropiL]
V
valid [in PropcL]var [in PropiL]
Record Index
R
ref_pred [in PropcL]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (681 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (35 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (363 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (100 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (31 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (24 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (92 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
This page has been generated by coqdoc