| 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 | (572 entries) |
| Binder 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 | (165 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 | (3 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 | (199 entries) |
| File 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) |
| 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 | (99 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 | (10 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 | (2 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 | (71 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 | (16 entries) |
Global Index
A
absorb [section, in CoMoEx.Laws]absorb_or [lemma, in CoMoEx.Laws]
absorb_and [lemma, in CoMoEx.Laws]
absorb.p [variable, in CoMoEx.Laws]
absorb.q [variable, in CoMoEx.Laws]
and_E2 [lemma, in CoMoEx.IntroElim]
and_E1 [lemma, in CoMoEx.IntroElim]
and_2.A1 [variable, in CoMoEx.IntroElim]
and_2.q [variable, in CoMoEx.IntroElim]
and_2.p [variable, in CoMoEx.IntroElim]
and_2 [section, in CoMoEx.IntroElim]
and_I [lemma, in CoMoEx.IntroElim]
and_1.A2 [variable, in CoMoEx.IntroElim]
and_1.A1 [variable, in CoMoEx.IntroElim]
and_1.q [variable, in CoMoEx.IntroElim]
and_1.p [variable, in CoMoEx.IntroElim]
and_1 [section, in CoMoEx.IntroElim]
and_assoc [lemma, in CoMoEx.Laws]
and_comm [lemma, in CoMoEx.Laws]
assoc [section, in CoMoEx.Laws]
assoc.p [variable, in CoMoEx.Laws]
assoc.q [variable, in CoMoEx.Laws]
assoc.r [variable, in CoMoEx.Laws]
A:17 [binder, in CoMoEx.Induction]
A:32 [binder, in CoMoEx.Induction]
B
bool_charac [lemma, in CoMoEx.Groups]bot_E [lemma, in CoMoEx.IntroElim]
bot_2.A1 [variable, in CoMoEx.IntroElim]
bot_2.p [variable, in CoMoEx.IntroElim]
bot_2 [section, in CoMoEx.IntroElim]
bot_I [lemma, in CoMoEx.IntroElim]
bot_1.A2 [variable, in CoMoEx.IntroElim]
bot_1.A1 [variable, in CoMoEx.IntroElim]
bot_1.p [variable, in CoMoEx.IntroElim]
bot_1 [section, in CoMoEx.IntroElim]
C
comm [section, in CoMoEx.Laws]comm.p [variable, in CoMoEx.Laws]
comm.q [variable, in CoMoEx.Laws]
contrapos [lemma, in CoMoEx.Laws]
contrapos [section, in CoMoEx.Laws]
contrapos.p [variable, in CoMoEx.Laws]
contrapos.q [variable, in CoMoEx.Laws]
curry [lemma, in CoMoEx.Laws]
currying [section, in CoMoEx.Laws]
currying.p [variable, in CoMoEx.Laws]
currying.q [variable, in CoMoEx.Laws]
currying.r [variable, in CoMoEx.Laws]
D
de_morgan_2 [lemma, in CoMoEx.Laws]de_morgan_1 [lemma, in CoMoEx.Laws]
de_morgan.q [variable, in CoMoEx.Laws]
de_morgan.p [variable, in CoMoEx.Laws]
de_morgan [section, in CoMoEx.Laws]
distr [section, in CoMoEx.Laws]
distr_2 [lemma, in CoMoEx.Laws]
distr_1 [lemma, in CoMoEx.Laws]
distr.p [variable, in CoMoEx.Laws]
distr.q [variable, in CoMoEx.Laws]
distr.r [variable, in CoMoEx.Laws]
E
excluded_middle [lemma, in CoMoEx.Laws]Exists [file]
existsE_demo_2 [lemma, in CoMoEx.Exists]
existsE_demo.existsE_demo_2.A2 [variable, in CoMoEx.Exists]
existsE_demo.existsE_demo_2.A1 [variable, in CoMoEx.Exists]
existsE_demo.existsE_demo_2.P [variable, in CoMoEx.Exists]
existsE_demo.existsE_demo_2 [section, in CoMoEx.Exists]
existsE_demo_1 [lemma, in CoMoEx.Exists]
existsE_demo.existsE_demo_1.A1 [variable, in CoMoEx.Exists]
existsE_demo.existsE_demo_1 [section, in CoMoEx.Exists]
existsE_demo.Q [variable, in CoMoEx.Exists]
existsE_demo.T [variable, in CoMoEx.Exists]
existsE_demo [section, in CoMoEx.Exists]
existsI_demo_3 [lemma, in CoMoEx.Exists]
existsI_demo.existsI_demo_3.A1 [variable, in CoMoEx.Exists]
existsI_demo.existsI_demo_3.x [variable, in CoMoEx.Exists]
existsI_demo.existsI_demo_3.P [variable, in CoMoEx.Exists]
existsI_demo.existsI_demo_3 [section, in CoMoEx.Exists]
existsI_demo_2 [lemma, in CoMoEx.Exists]
existsI_demo.existsI_demo_2.A1 [variable, in CoMoEx.Exists]
existsI_demo.existsI_demo_2.some_t [variable, in CoMoEx.Exists]
existsI_demo.existsI_demo_2.P [variable, in CoMoEx.Exists]
existsI_demo.existsI_demo_2 [section, in CoMoEx.Exists]
existsI_demo_1 [lemma, in CoMoEx.Exists]
existsI_demo.existsI_demo_1.A1 [variable, in CoMoEx.Exists]
existsI_demo.existsI_demo_1.some_t [variable, in CoMoEx.Exists]
existsI_demo.existsI_demo_1.Q [variable, in CoMoEx.Exists]
existsI_demo.existsI_demo_1 [section, in CoMoEx.Exists]
existsI_demo.T [variable, in CoMoEx.Exists]
existsI_demo [section, in CoMoEx.Exists]
exists_comm_or_2_1 [lemma, in CoMoEx.Exists]
exists_comm_ops.exists_comm_or_2.H1 [variable, in CoMoEx.Exists]
exists_comm_ops.exists_comm_or_2 [section, in CoMoEx.Exists]
exists_comm_or_1_1 [lemma, in CoMoEx.Exists]
exists_comm_ops.exists_comm_or_1.H1 [variable, in CoMoEx.Exists]
exists_comm_ops.exists_comm_or_1 [section, in CoMoEx.Exists]
exists_comm_and_2_1 [lemma, in CoMoEx.Exists]
exists_comm_ops.exists_comm_and_2.H1 [variable, in CoMoEx.Exists]
exists_comm_ops.exists_comm_and_2 [section, in CoMoEx.Exists]
exists_comm_and_1_1 [lemma, in CoMoEx.Exists]
exists_comm_ops.exists_comm_and_1.H1 [variable, in CoMoEx.Exists]
exists_comm_ops.exists_comm_and_1 [section, in CoMoEx.Exists]
exists_comm_ops.Q [variable, in CoMoEx.Exists]
exists_comm_ops.P [variable, in CoMoEx.Exists]
exists_comm_ops.T [variable, in CoMoEx.Exists]
exists_comm_ops [section, in CoMoEx.Exists]
e:12 [binder, in CoMoEx.Groups]
e:16 [binder, in CoMoEx.Groups]
e:8 [binder, in CoMoEx.Groups]
F
Forall [file]forallE_demo_2 [lemma, in CoMoEx.Forall]
forallE_demo.forallE_demo_2.A1 [variable, in CoMoEx.Forall]
forallE_demo.forallE_demo_2.P [variable, in CoMoEx.Forall]
forallE_demo.forallE_demo_2 [section, in CoMoEx.Forall]
forallE_demo_1 [lemma, in CoMoEx.Forall]
forallE_demo.forallE_demo_1.A1 [variable, in CoMoEx.Forall]
forallE_demo.forallE_demo_1.Q [variable, in CoMoEx.Forall]
forallE_demo.forallE_demo_1 [section, in CoMoEx.Forall]
forallE_demo.some_t [variable, in CoMoEx.Forall]
forallE_demo.T [variable, in CoMoEx.Forall]
forallE_demo [section, in CoMoEx.Forall]
forallI_demo_2 [lemma, in CoMoEx.Forall]
forallI_demo.forallI_demo_2.A1 [variable, in CoMoEx.Forall]
forallI_demo.forallI_demo_2.P [variable, in CoMoEx.Forall]
forallI_demo.forallI_demo_2 [section, in CoMoEx.Forall]
forallI_demo_1 [lemma, in CoMoEx.Forall]
forallI_demo.forallI_demo_1.A1 [variable, in CoMoEx.Forall]
forallI_demo.forallI_demo_1.Q [variable, in CoMoEx.Forall]
forallI_demo.forallI_demo_1 [section, in CoMoEx.Forall]
forallI_demo.T [variable, in CoMoEx.Forall]
forallI_demo [section, in CoMoEx.Forall]
forall_ex_7_1 [lemma, in CoMoEx.Forall]
forall_ex_7.P [variable, in CoMoEx.Forall]
forall_ex_7.T [variable, in CoMoEx.Forall]
forall_ex_7 [section, in CoMoEx.Forall]
forall_ex_6_1 [lemma, in CoMoEx.Forall]
forall_ex_6.A2 [variable, in CoMoEx.Forall]
forall_ex_6.A1 [variable, in CoMoEx.Forall]
forall_ex_6.R [variable, in CoMoEx.Forall]
forall_ex_6.P [variable, in CoMoEx.Forall]
forall_ex_6.z [variable, in CoMoEx.Forall]
forall_ex_6.T [variable, in CoMoEx.Forall]
forall_ex_6 [section, in CoMoEx.Forall]
forall_ex_5_1 [lemma, in CoMoEx.Forall]
forall_ex_5.A3 [variable, in CoMoEx.Forall]
forall_ex_5.A2 [variable, in CoMoEx.Forall]
forall_ex_5.A1 [variable, in CoMoEx.Forall]
forall_ex_5.R [variable, in CoMoEx.Forall]
forall_ex_5.T [variable, in CoMoEx.Forall]
forall_ex_5 [section, in CoMoEx.Forall]
forall_ex_4_1 [lemma, in CoMoEx.Forall]
forall_ex_4.A2 [variable, in CoMoEx.Forall]
forall_ex_4.A1 [variable, in CoMoEx.Forall]
forall_ex_4.S [variable, in CoMoEx.Forall]
forall_ex_4.R [variable, in CoMoEx.Forall]
forall_ex_4.P [variable, in CoMoEx.Forall]
forall_ex_4.T [variable, in CoMoEx.Forall]
forall_ex_4 [section, in CoMoEx.Forall]
forall_ex_3_1 [lemma, in CoMoEx.Forall]
forall_ex_3.A3 [variable, in CoMoEx.Forall]
forall_ex_3.A2 [variable, in CoMoEx.Forall]
forall_ex_3.A1 [variable, in CoMoEx.Forall]
forall_ex_3.R [variable, in CoMoEx.Forall]
forall_ex_3.Q [variable, in CoMoEx.Forall]
forall_ex_3.P [variable, in CoMoEx.Forall]
forall_ex_3.T [variable, in CoMoEx.Forall]
forall_ex_3 [section, in CoMoEx.Forall]
forall_ex_2_1 [lemma, in CoMoEx.Forall]
forall_ex_2.A2 [variable, in CoMoEx.Forall]
forall_ex_2.A1 [variable, in CoMoEx.Forall]
forall_ex_2.R [variable, in CoMoEx.Forall]
forall_ex_2.Q [variable, in CoMoEx.Forall]
forall_ex_2.P [variable, in CoMoEx.Forall]
forall_ex_2.T [variable, in CoMoEx.Forall]
forall_ex_2 [section, in CoMoEx.Forall]
forall_ex_1_1 [lemma, in CoMoEx.Forall]
forall_ex_1.A1 [variable, in CoMoEx.Forall]
forall_ex_1.P [variable, in CoMoEx.Forall]
forall_ex_1.T [variable, in CoMoEx.Forall]
forall_ex_1 [section, in CoMoEx.Forall]
forall_comm_iff_2_1 [lemma, in CoMoEx.Forall]
forall_comm_ops.forall_comm_iff_2.H1 [variable, in CoMoEx.Forall]
forall_comm_ops.forall_comm_iff_2 [section, in CoMoEx.Forall]
forall_comm_iff_1_1 [lemma, in CoMoEx.Forall]
forall_comm_ops.forall_comm_iff_1.H1 [variable, in CoMoEx.Forall]
forall_comm_ops.forall_comm_iff_1 [section, in CoMoEx.Forall]
forall_comm_impl_2_1 [lemma, in CoMoEx.Forall]
forall_comm_ops.forall_comm_impl_2.H1 [variable, in CoMoEx.Forall]
forall_comm_ops.forall_comm_impl_2 [section, in CoMoEx.Forall]
forall_comm_impl_1_1 [lemma, in CoMoEx.Forall]
forall_comm_ops.forall_comm_impl_1.H1 [variable, in CoMoEx.Forall]
forall_comm_ops.forall_comm_impl_1 [section, in CoMoEx.Forall]
forall_comm_or_2_1 [lemma, in CoMoEx.Forall]
forall_comm_ops.forall_comm_or_2.H1 [variable, in CoMoEx.Forall]
forall_comm_ops.forall_comm_or_2 [section, in CoMoEx.Forall]
forall_comm_or_1_1 [lemma, in CoMoEx.Forall]
forall_comm_ops.forall_comm_or_1.H1 [variable, in CoMoEx.Forall]
forall_comm_ops.forall_comm_or_1 [section, in CoMoEx.Forall]
forall_comm_and_2_1 [lemma, in CoMoEx.Forall]
forall_comm_ops.forall_comm_and_2.H1 [variable, in CoMoEx.Forall]
forall_comm_ops.forall_comm_and_2 [section, in CoMoEx.Forall]
forall_comm_and_1_1 [lemma, in CoMoEx.Forall]
forall_comm_ops.forall_comm_and_1.H1 [variable, in CoMoEx.Forall]
forall_comm_ops.forall_comm_and_1 [section, in CoMoEx.Forall]
forall_comm_ops.Q [variable, in CoMoEx.Forall]
forall_comm_ops.P [variable, in CoMoEx.Forall]
forall_comm_ops.T [variable, in CoMoEx.Forall]
forall_comm_ops [section, in CoMoEx.Forall]
f:11 [binder, in CoMoEx.Groups]
f:2 [binder, in CoMoEx.Groups]
f:27 [binder, in CoMoEx.Induction]
f:31 [binder, in CoMoEx.Induction]
f:35 [binder, in CoMoEx.Induction]
f:47 [binder, in CoMoEx.Induction]
f:50 [binder, in CoMoEx.Induction]
f:53 [binder, in CoMoEx.Induction]
f:7 [binder, in CoMoEx.Groups]
G
Groups [file]G:1 [binder, in CoMoEx.Groups]
G:10 [binder, in CoMoEx.Groups]
G:6 [binder, in CoMoEx.Groups]
H
how_to_use_Laws_2 [definition, in CoMoEx.SomeExamples]how_to_use_Laws_1 [definition, in CoMoEx.SomeExamples]
how_to_use_Laws.p2 [variable, in CoMoEx.SomeExamples]
how_to_use_Laws.p1 [variable, in CoMoEx.SomeExamples]
how_to_use_Laws [section, in CoMoEx.SomeExamples]
I
idem [section, in CoMoEx.Laws]idem_or [lemma, in CoMoEx.Laws]
idem_and [lemma, in CoMoEx.Laws]
idem.p [variable, in CoMoEx.Laws]
iff_E_2 [lemma, in CoMoEx.IntroElim]
iff_3.A2 [variable, in CoMoEx.IntroElim]
iff_3.A1 [variable, in CoMoEx.IntroElim]
iff_3.q [variable, in CoMoEx.IntroElim]
iff_3.p [variable, in CoMoEx.IntroElim]
iff_3 [section, in CoMoEx.IntroElim]
iff_E_1 [lemma, in CoMoEx.IntroElim]
iff_2.A2 [variable, in CoMoEx.IntroElim]
iff_2.A1 [variable, in CoMoEx.IntroElim]
iff_2.q [variable, in CoMoEx.IntroElim]
iff_2.p [variable, in CoMoEx.IntroElim]
iff_2 [section, in CoMoEx.IntroElim]
iff_I [lemma, in CoMoEx.IntroElim]
iff_1.A2 [variable, in CoMoEx.IntroElim]
iff_1.A1 [variable, in CoMoEx.IntroElim]
iff_1.q [variable, in CoMoEx.IntroElim]
iff_1.p [variable, in CoMoEx.IntroElim]
iff_1 [section, in CoMoEx.IntroElim]
implsem [section, in CoMoEx.Laws]
implsem.p [variable, in CoMoEx.Laws]
implsem.q [variable, in CoMoEx.Laws]
impl_E [lemma, in CoMoEx.IntroElim]
impl_2.A2 [variable, in CoMoEx.IntroElim]
impl_2.A1 [variable, in CoMoEx.IntroElim]
impl_2.q [variable, in CoMoEx.IntroElim]
impl_2.p [variable, in CoMoEx.IntroElim]
impl_2 [section, in CoMoEx.IntroElim]
impl_I [lemma, in CoMoEx.IntroElim]
impl_1.A1 [variable, in CoMoEx.IntroElim]
impl_1.q [variable, in CoMoEx.IntroElim]
impl_1.p [variable, in CoMoEx.IntroElim]
impl_1 [section, in CoMoEx.IntroElim]
impl_trans [lemma, in CoMoEx.Laws]
impl_trans.A2 [variable, in CoMoEx.Laws]
impl_trans.A1 [variable, in CoMoEx.Laws]
impl_trans.r [variable, in CoMoEx.Laws]
impl_trans.q [variable, in CoMoEx.Laws]
impl_trans.p [variable, in CoMoEx.Laws]
impl_trans [section, in CoMoEx.Laws]
impl_with_conj [lemma, in CoMoEx.Laws]
impl_with_disj [lemma, in CoMoEx.Laws]
Induction [file]
IntroElim [file]
is_left_inv [definition, in CoMoEx.Groups]
is_left_id [definition, in CoMoEx.Groups]
is_assoc [definition, in CoMoEx.Groups]
i:13 [binder, in CoMoEx.Groups]
i:17 [binder, in CoMoEx.Groups]
K
k:28 [binder, in CoMoEx.Induction]L
Laws [file]logic_vol1.disjunctive_correctness [lemma, in CoMoEx.Induction]
logic_vol1.mini_ex.H3 [variable, in CoMoEx.Induction]
logic_vol1.mini_ex.H2 [variable, in CoMoEx.Induction]
logic_vol1.mini_ex.H1 [variable, in CoMoEx.Induction]
logic_vol1.mini_ex.k [variable, in CoMoEx.Induction]
logic_vol1.mini_ex.A [variable, in CoMoEx.Induction]
logic_vol1.mini_ex.f [variable, in CoMoEx.Induction]
logic_vol1.mini_ex [section, in CoMoEx.Induction]
logic_vol1.only_bot_atom_disj [definition, in CoMoEx.Induction]
logic_vol1.contains [definition, in CoMoEx.Induction]
logic_vol1.evaluate [definition, in CoMoEx.Induction]
logic_vol1.iff [constructor, in CoMoEx.Induction]
logic_vol1.impl [constructor, in CoMoEx.Induction]
logic_vol1.disj [constructor, in CoMoEx.Induction]
logic_vol1.conj [constructor, in CoMoEx.Induction]
logic_vol1.neg [constructor, in CoMoEx.Induction]
logic_vol1.atom [constructor, in CoMoEx.Induction]
logic_vol1.top [constructor, in CoMoEx.Induction]
logic_vol1.bot [constructor, in CoMoEx.Induction]
logic_vol1.form [inductive, in CoMoEx.Induction]
logic_vol1.atoms [definition, in CoMoEx.Induction]
logic_vol1 [module, in CoMoEx.Induction]
M
mod_tollens [lemma, in CoMoEx.Laws]m':63 [binder, in CoMoEx.Induction]
m:10 [binder, in CoMoEx.Induction]
m:12 [binder, in CoMoEx.Induction]
m:13 [binder, in CoMoEx.Induction]
m:5 [binder, in CoMoEx.Induction]
m:58 [binder, in CoMoEx.Induction]
m:65 [binder, in CoMoEx.Induction]
N
nat_exercises.know_this_one [lemma, in CoMoEx.Induction]nat_exercises.addRow [definition, in CoMoEx.Induction]
nat_exercises.mulN_assoc [lemma, in CoMoEx.Induction]
nat_exercises.addN_mulN_distr_2 [lemma, in CoMoEx.Induction]
nat_exercises.addN_mulN_distr_1 [lemma, in CoMoEx.Induction]
nat_exercises.mulN_comm [lemma, in CoMoEx.Induction]
nat_exercises.mulN_n_succ_m [lemma, in CoMoEx.Induction]
nat_exercises.mulN_zero_r [lemma, in CoMoEx.Induction]
nat_exercises.mulN [definition, in CoMoEx.Induction]
nat_exercises.addN_assoc [lemma, in CoMoEx.Induction]
nat_exercises.my_nat_iso_to_nat [lemma, in CoMoEx.Induction]
nat_exercises.bij [definition, in CoMoEx.Induction]
nat_exercises.sur [definition, in CoMoEx.Induction]
nat_exercises.inj [definition, in CoMoEx.Induction]
nat_exercises.my_nat_to_nat [definition, in CoMoEx.Induction]
nat_exercises [module, in CoMoEx.Induction]
nat_playground.addN_comm' [lemma, in CoMoEx.Induction]
nat_playground.addN_comm [lemma, in CoMoEx.Induction]
nat_playground.addN_n_succ_m [lemma, in CoMoEx.Induction]
nat_playground.addN_zero_r [lemma, in CoMoEx.Induction]
nat_playground.addN [definition, in CoMoEx.Induction]
nat_playground.succ [constructor, in CoMoEx.Induction]
nat_playground.zero [constructor, in CoMoEx.Induction]
nat_playground.my_nat [inductive, in CoMoEx.Induction]
nat_playground [module, in CoMoEx.Induction]
neg_E [lemma, in CoMoEx.IntroElim]
neg_2.A1 [variable, in CoMoEx.IntroElim]
neg_2.p [variable, in CoMoEx.IntroElim]
neg_2 [section, in CoMoEx.IntroElim]
neg_I [lemma, in CoMoEx.IntroElim]
neg_1.A1 [variable, in CoMoEx.IntroElim]
neg_1.p [variable, in CoMoEx.IntroElim]
neg_1 [section, in CoMoEx.IntroElim]
neutr [section, in CoMoEx.Laws]
neutr_or [lemma, in CoMoEx.Laws]
neutr_and [lemma, in CoMoEx.Laws]
neutr.p [variable, in CoMoEx.Laws]
n:11 [binder, in CoMoEx.Induction]
n:14 [binder, in CoMoEx.Induction]
n:3 [binder, in CoMoEx.Induction]
n:4 [binder, in CoMoEx.Induction]
n:57 [binder, in CoMoEx.Induction]
n:61 [binder, in CoMoEx.Induction]
n:62 [binder, in CoMoEx.Induction]
n:64 [binder, in CoMoEx.Induction]
n:75 [binder, in CoMoEx.Induction]
n:78 [binder, in CoMoEx.Induction]
n:8 [binder, in CoMoEx.Induction]
n:9 [binder, in CoMoEx.Induction]
O
or_E [lemma, in CoMoEx.IntroElim]or_3.A3 [variable, in CoMoEx.IntroElim]
or_3.A2 [variable, in CoMoEx.IntroElim]
or_3.A1 [variable, in CoMoEx.IntroElim]
or_3.r [variable, in CoMoEx.IntroElim]
or_3.q [variable, in CoMoEx.IntroElim]
or_3.p [variable, in CoMoEx.IntroElim]
or_3 [section, in CoMoEx.IntroElim]
or_I2 [lemma, in CoMoEx.IntroElim]
or_2.A1 [variable, in CoMoEx.IntroElim]
or_2.q [variable, in CoMoEx.IntroElim]
or_2.p [variable, in CoMoEx.IntroElim]
or_2 [section, in CoMoEx.IntroElim]
or_I1 [lemma, in CoMoEx.IntroElim]
or_1.A1 [variable, in CoMoEx.IntroElim]
or_1.q [variable, in CoMoEx.IntroElim]
or_1.p [variable, in CoMoEx.IntroElim]
or_1 [section, in CoMoEx.IntroElim]
or_assoc [lemma, in CoMoEx.Laws]
or_comm [lemma, in CoMoEx.Laws]
P
peirce [lemma, in CoMoEx.Laws]peirce_law.q [variable, in CoMoEx.Laws]
peirce_law.p [variable, in CoMoEx.Laws]
peirce_law [section, in CoMoEx.Laws]
p_and_not_p [lemma, in CoMoEx.Laws]
p_not_p.p [variable, in CoMoEx.Laws]
p_not_p [section, in CoMoEx.Laws]
S
se_7_1 [lemma, in CoMoEx.SomeExamples]se_7.p2 [variable, in CoMoEx.SomeExamples]
se_7.p1 [variable, in CoMoEx.SomeExamples]
se_7 [section, in CoMoEx.SomeExamples]
se_6_1 [lemma, in CoMoEx.SomeExamples]
se_6.A1 [variable, in CoMoEx.SomeExamples]
se_6.p2 [variable, in CoMoEx.SomeExamples]
se_6.p1 [variable, in CoMoEx.SomeExamples]
se_6 [section, in CoMoEx.SomeExamples]
se_5_1 [lemma, in CoMoEx.SomeExamples]
se_5.A1 [variable, in CoMoEx.SomeExamples]
se_5.p2 [variable, in CoMoEx.SomeExamples]
se_5.p1 [variable, in CoMoEx.SomeExamples]
se_5 [section, in CoMoEx.SomeExamples]
se_4_1 [lemma, in CoMoEx.SomeExamples]
se_4.A1 [variable, in CoMoEx.SomeExamples]
se_4.p3 [variable, in CoMoEx.SomeExamples]
se_4.p2 [variable, in CoMoEx.SomeExamples]
se_4.p1 [variable, in CoMoEx.SomeExamples]
se_4 [section, in CoMoEx.SomeExamples]
se_3_1 [lemma, in CoMoEx.SomeExamples]
se_3.A6 [variable, in CoMoEx.SomeExamples]
se_3.A5 [variable, in CoMoEx.SomeExamples]
se_3.A4 [variable, in CoMoEx.SomeExamples]
se_3.A3 [variable, in CoMoEx.SomeExamples]
se_3.A2 [variable, in CoMoEx.SomeExamples]
se_3.A1 [variable, in CoMoEx.SomeExamples]
se_3.p5 [variable, in CoMoEx.SomeExamples]
se_3.p4 [variable, in CoMoEx.SomeExamples]
se_3.p3 [variable, in CoMoEx.SomeExamples]
se_3.p2 [variable, in CoMoEx.SomeExamples]
se_3.p1 [variable, in CoMoEx.SomeExamples]
se_3 [section, in CoMoEx.SomeExamples]
se_2_3 [lemma, in CoMoEx.SomeExamples]
se_2_2 [lemma, in CoMoEx.SomeExamples]
se_2_1 [lemma, in CoMoEx.SomeExamples]
se_2.A1 [variable, in CoMoEx.SomeExamples]
se_2.p4 [variable, in CoMoEx.SomeExamples]
se_2.p3 [variable, in CoMoEx.SomeExamples]
se_2.p2 [variable, in CoMoEx.SomeExamples]
se_2.p1 [variable, in CoMoEx.SomeExamples]
se_2 [section, in CoMoEx.SomeExamples]
se_1.A2 [variable, in CoMoEx.SomeExamples]
se_1.A1 [variable, in CoMoEx.SomeExamples]
se_1.p4 [variable, in CoMoEx.SomeExamples]
se_1.p3 [variable, in CoMoEx.SomeExamples]
se_1.p2 [variable, in CoMoEx.SomeExamples]
se_1.p1 [variable, in CoMoEx.SomeExamples]
se_1 [section, in CoMoEx.SomeExamples]
SomeExamples [file]
T
trivial_iff_false [lemma, in CoMoEx.Laws]trivial_iff_true [lemma, in CoMoEx.Laws]
trivial_iff.p [variable, in CoMoEx.Laws]
trivial_iff [section, in CoMoEx.Laws]
T12 [lemma, in CoMoEx.SomeExamples]
T13 [lemma, in CoMoEx.SomeExamples]
T14 [lemma, in CoMoEx.SomeExamples]
T23 [lemma, in CoMoEx.SomeExamples]
T24 [lemma, in CoMoEx.SomeExamples]
T34 [lemma, in CoMoEx.SomeExamples]
X
xor_left_id_inv_exists [lemma, in CoMoEx.Groups]xor_assoc [lemma, in CoMoEx.Groups]
x':49 [binder, in CoMoEx.Induction]
x:100 [binder, in CoMoEx.Forall]
x:104 [binder, in CoMoEx.Forall]
x:107 [binder, in CoMoEx.Forall]
x:111 [binder, in CoMoEx.Forall]
x:114 [binder, in CoMoEx.Forall]
x:119 [binder, in CoMoEx.Forall]
x:12 [binder, in CoMoEx.Forall]
x:127 [binder, in CoMoEx.Forall]
x:129 [binder, in CoMoEx.Forall]
x:13 [binder, in CoMoEx.Exists]
x:14 [binder, in CoMoEx.Forall]
x:14 [binder, in CoMoEx.Groups]
x:15 [binder, in CoMoEx.Groups]
x:16 [binder, in CoMoEx.Forall]
x:16 [binder, in CoMoEx.Exists]
x:18 [binder, in CoMoEx.Induction]
x:19 [binder, in CoMoEx.Exists]
x:19 [binder, in CoMoEx.Induction]
x:20 [binder, in CoMoEx.Forall]
x:21 [binder, in CoMoEx.Induction]
x:22 [binder, in CoMoEx.Forall]
x:22 [binder, in CoMoEx.Exists]
x:23 [binder, in CoMoEx.Forall]
x:23 [binder, in CoMoEx.Induction]
x:24 [binder, in CoMoEx.Forall]
x:25 [binder, in CoMoEx.Induction]
x:26 [binder, in CoMoEx.Exists]
x:27 [binder, in CoMoEx.Forall]
x:28 [binder, in CoMoEx.Forall]
x:28 [binder, in CoMoEx.Exists]
x:29 [binder, in CoMoEx.Forall]
x:29 [binder, in CoMoEx.Exists]
x:3 [binder, in CoMoEx.Groups]
x:30 [binder, in CoMoEx.Exists]
x:31 [binder, in CoMoEx.Forall]
x:32 [binder, in CoMoEx.Forall]
x:33 [binder, in CoMoEx.Forall]
x:33 [binder, in CoMoEx.Exists]
x:34 [binder, in CoMoEx.Exists]
x:35 [binder, in CoMoEx.Exists]
x:36 [binder, in CoMoEx.Forall]
x:37 [binder, in CoMoEx.Forall]
x:37 [binder, in CoMoEx.Exists]
x:38 [binder, in CoMoEx.Forall]
x:38 [binder, in CoMoEx.Exists]
x:39 [binder, in CoMoEx.Exists]
x:4 [binder, in CoMoEx.Forall]
x:40 [binder, in CoMoEx.Forall]
x:41 [binder, in CoMoEx.Forall]
x:42 [binder, in CoMoEx.Forall]
x:42 [binder, in CoMoEx.Exists]
x:43 [binder, in CoMoEx.Exists]
x:44 [binder, in CoMoEx.Induction]
x:45 [binder, in CoMoEx.Forall]
x:46 [binder, in CoMoEx.Forall]
x:47 [binder, in CoMoEx.Forall]
x:48 [binder, in CoMoEx.Induction]
x:49 [binder, in CoMoEx.Forall]
x:5 [binder, in CoMoEx.Exists]
x:50 [binder, in CoMoEx.Forall]
x:51 [binder, in CoMoEx.Forall]
x:52 [binder, in CoMoEx.Induction]
x:54 [binder, in CoMoEx.Forall]
x:54 [binder, in CoMoEx.Induction]
x:55 [binder, in CoMoEx.Forall]
x:58 [binder, in CoMoEx.Forall]
x:62 [binder, in CoMoEx.Forall]
x:66 [binder, in CoMoEx.Induction]
x:67 [binder, in CoMoEx.Forall]
x:69 [binder, in CoMoEx.Induction]
x:7 [binder, in CoMoEx.Forall]
x:70 [binder, in CoMoEx.Forall]
x:72 [binder, in CoMoEx.Forall]
x:72 [binder, in CoMoEx.Induction]
x:78 [binder, in CoMoEx.Forall]
x:82 [binder, in CoMoEx.Forall]
x:84 [binder, in CoMoEx.Forall]
x:87 [binder, in CoMoEx.Forall]
x:9 [binder, in CoMoEx.Exists]
x:9 [binder, in CoMoEx.Groups]
x:93 [binder, in CoMoEx.Forall]
x:96 [binder, in CoMoEx.Forall]
Y
y:101 [binder, in CoMoEx.Forall]y:105 [binder, in CoMoEx.Forall]
y:108 [binder, in CoMoEx.Forall]
y:112 [binder, in CoMoEx.Forall]
y:120 [binder, in CoMoEx.Forall]
y:122 [binder, in CoMoEx.Forall]
y:124 [binder, in CoMoEx.Forall]
y:128 [binder, in CoMoEx.Forall]
y:130 [binder, in CoMoEx.Forall]
y:131 [binder, in CoMoEx.Forall]
y:20 [binder, in CoMoEx.Induction]
y:22 [binder, in CoMoEx.Induction]
y:24 [binder, in CoMoEx.Induction]
y:25 [binder, in CoMoEx.Forall]
y:26 [binder, in CoMoEx.Induction]
y:31 [binder, in CoMoEx.Exists]
y:34 [binder, in CoMoEx.Forall]
y:4 [binder, in CoMoEx.Groups]
y:40 [binder, in CoMoEx.Exists]
y:43 [binder, in CoMoEx.Forall]
y:51 [binder, in CoMoEx.Induction]
y:52 [binder, in CoMoEx.Forall]
y:55 [binder, in CoMoEx.Induction]
y:59 [binder, in CoMoEx.Forall]
y:61 [binder, in CoMoEx.Forall]
y:67 [binder, in CoMoEx.Induction]
y:68 [binder, in CoMoEx.Forall]
y:70 [binder, in CoMoEx.Induction]
y:73 [binder, in CoMoEx.Forall]
y:73 [binder, in CoMoEx.Induction]
y:79 [binder, in CoMoEx.Forall]
y:85 [binder, in CoMoEx.Forall]
y:88 [binder, in CoMoEx.Forall]
y:94 [binder, in CoMoEx.Forall]
y:97 [binder, in CoMoEx.Forall]
Z
z:109 [binder, in CoMoEx.Forall]z:5 [binder, in CoMoEx.Groups]
z:56 [binder, in CoMoEx.Induction]
z:68 [binder, in CoMoEx.Induction]
z:71 [binder, in CoMoEx.Induction]
z:74 [binder, in CoMoEx.Induction]
z:80 [binder, in CoMoEx.Forall]
z:98 [binder, in CoMoEx.Forall]
Binder Index
A
A:17 [in CoMoEx.Induction]A:32 [in CoMoEx.Induction]
E
e:12 [in CoMoEx.Groups]e:16 [in CoMoEx.Groups]
e:8 [in CoMoEx.Groups]
F
f:11 [in CoMoEx.Groups]f:2 [in CoMoEx.Groups]
f:27 [in CoMoEx.Induction]
f:31 [in CoMoEx.Induction]
f:35 [in CoMoEx.Induction]
f:47 [in CoMoEx.Induction]
f:50 [in CoMoEx.Induction]
f:53 [in CoMoEx.Induction]
f:7 [in CoMoEx.Groups]
G
G:1 [in CoMoEx.Groups]G:10 [in CoMoEx.Groups]
G:6 [in CoMoEx.Groups]
I
i:13 [in CoMoEx.Groups]i:17 [in CoMoEx.Groups]
K
k:28 [in CoMoEx.Induction]M
m':63 [in CoMoEx.Induction]m:10 [in CoMoEx.Induction]
m:12 [in CoMoEx.Induction]
m:13 [in CoMoEx.Induction]
m:5 [in CoMoEx.Induction]
m:58 [in CoMoEx.Induction]
m:65 [in CoMoEx.Induction]
N
n:11 [in CoMoEx.Induction]n:14 [in CoMoEx.Induction]
n:3 [in CoMoEx.Induction]
n:4 [in CoMoEx.Induction]
n:57 [in CoMoEx.Induction]
n:61 [in CoMoEx.Induction]
n:62 [in CoMoEx.Induction]
n:64 [in CoMoEx.Induction]
n:75 [in CoMoEx.Induction]
n:78 [in CoMoEx.Induction]
n:8 [in CoMoEx.Induction]
n:9 [in CoMoEx.Induction]
X
x':49 [in CoMoEx.Induction]x:100 [in CoMoEx.Forall]
x:104 [in CoMoEx.Forall]
x:107 [in CoMoEx.Forall]
x:111 [in CoMoEx.Forall]
x:114 [in CoMoEx.Forall]
x:119 [in CoMoEx.Forall]
x:12 [in CoMoEx.Forall]
x:127 [in CoMoEx.Forall]
x:129 [in CoMoEx.Forall]
x:13 [in CoMoEx.Exists]
x:14 [in CoMoEx.Forall]
x:14 [in CoMoEx.Groups]
x:15 [in CoMoEx.Groups]
x:16 [in CoMoEx.Forall]
x:16 [in CoMoEx.Exists]
x:18 [in CoMoEx.Induction]
x:19 [in CoMoEx.Exists]
x:19 [in CoMoEx.Induction]
x:20 [in CoMoEx.Forall]
x:21 [in CoMoEx.Induction]
x:22 [in CoMoEx.Forall]
x:22 [in CoMoEx.Exists]
x:23 [in CoMoEx.Forall]
x:23 [in CoMoEx.Induction]
x:24 [in CoMoEx.Forall]
x:25 [in CoMoEx.Induction]
x:26 [in CoMoEx.Exists]
x:27 [in CoMoEx.Forall]
x:28 [in CoMoEx.Forall]
x:28 [in CoMoEx.Exists]
x:29 [in CoMoEx.Forall]
x:29 [in CoMoEx.Exists]
x:3 [in CoMoEx.Groups]
x:30 [in CoMoEx.Exists]
x:31 [in CoMoEx.Forall]
x:32 [in CoMoEx.Forall]
x:33 [in CoMoEx.Forall]
x:33 [in CoMoEx.Exists]
x:34 [in CoMoEx.Exists]
x:35 [in CoMoEx.Exists]
x:36 [in CoMoEx.Forall]
x:37 [in CoMoEx.Forall]
x:37 [in CoMoEx.Exists]
x:38 [in CoMoEx.Forall]
x:38 [in CoMoEx.Exists]
x:39 [in CoMoEx.Exists]
x:4 [in CoMoEx.Forall]
x:40 [in CoMoEx.Forall]
x:41 [in CoMoEx.Forall]
x:42 [in CoMoEx.Forall]
x:42 [in CoMoEx.Exists]
x:43 [in CoMoEx.Exists]
x:44 [in CoMoEx.Induction]
x:45 [in CoMoEx.Forall]
x:46 [in CoMoEx.Forall]
x:47 [in CoMoEx.Forall]
x:48 [in CoMoEx.Induction]
x:49 [in CoMoEx.Forall]
x:5 [in CoMoEx.Exists]
x:50 [in CoMoEx.Forall]
x:51 [in CoMoEx.Forall]
x:52 [in CoMoEx.Induction]
x:54 [in CoMoEx.Forall]
x:54 [in CoMoEx.Induction]
x:55 [in CoMoEx.Forall]
x:58 [in CoMoEx.Forall]
x:62 [in CoMoEx.Forall]
x:66 [in CoMoEx.Induction]
x:67 [in CoMoEx.Forall]
x:69 [in CoMoEx.Induction]
x:7 [in CoMoEx.Forall]
x:70 [in CoMoEx.Forall]
x:72 [in CoMoEx.Forall]
x:72 [in CoMoEx.Induction]
x:78 [in CoMoEx.Forall]
x:82 [in CoMoEx.Forall]
x:84 [in CoMoEx.Forall]
x:87 [in CoMoEx.Forall]
x:9 [in CoMoEx.Exists]
x:9 [in CoMoEx.Groups]
x:93 [in CoMoEx.Forall]
x:96 [in CoMoEx.Forall]
Y
y:101 [in CoMoEx.Forall]y:105 [in CoMoEx.Forall]
y:108 [in CoMoEx.Forall]
y:112 [in CoMoEx.Forall]
y:120 [in CoMoEx.Forall]
y:122 [in CoMoEx.Forall]
y:124 [in CoMoEx.Forall]
y:128 [in CoMoEx.Forall]
y:130 [in CoMoEx.Forall]
y:131 [in CoMoEx.Forall]
y:20 [in CoMoEx.Induction]
y:22 [in CoMoEx.Induction]
y:24 [in CoMoEx.Induction]
y:25 [in CoMoEx.Forall]
y:26 [in CoMoEx.Induction]
y:31 [in CoMoEx.Exists]
y:34 [in CoMoEx.Forall]
y:4 [in CoMoEx.Groups]
y:40 [in CoMoEx.Exists]
y:43 [in CoMoEx.Forall]
y:51 [in CoMoEx.Induction]
y:52 [in CoMoEx.Forall]
y:55 [in CoMoEx.Induction]
y:59 [in CoMoEx.Forall]
y:61 [in CoMoEx.Forall]
y:67 [in CoMoEx.Induction]
y:68 [in CoMoEx.Forall]
y:70 [in CoMoEx.Induction]
y:73 [in CoMoEx.Forall]
y:73 [in CoMoEx.Induction]
y:79 [in CoMoEx.Forall]
y:85 [in CoMoEx.Forall]
y:88 [in CoMoEx.Forall]
y:94 [in CoMoEx.Forall]
y:97 [in CoMoEx.Forall]
Z
z:109 [in CoMoEx.Forall]z:5 [in CoMoEx.Groups]
z:56 [in CoMoEx.Induction]
z:68 [in CoMoEx.Induction]
z:71 [in CoMoEx.Induction]
z:74 [in CoMoEx.Induction]
z:80 [in CoMoEx.Forall]
z:98 [in CoMoEx.Forall]
Module Index
L
logic_vol1 [in CoMoEx.Induction]N
nat_exercises [in CoMoEx.Induction]nat_playground [in CoMoEx.Induction]
Variable Index
A
absorb.p [in CoMoEx.Laws]absorb.q [in CoMoEx.Laws]
and_2.A1 [in CoMoEx.IntroElim]
and_2.q [in CoMoEx.IntroElim]
and_2.p [in CoMoEx.IntroElim]
and_1.A2 [in CoMoEx.IntroElim]
and_1.A1 [in CoMoEx.IntroElim]
and_1.q [in CoMoEx.IntroElim]
and_1.p [in CoMoEx.IntroElim]
assoc.p [in CoMoEx.Laws]
assoc.q [in CoMoEx.Laws]
assoc.r [in CoMoEx.Laws]
B
bot_2.A1 [in CoMoEx.IntroElim]bot_2.p [in CoMoEx.IntroElim]
bot_1.A2 [in CoMoEx.IntroElim]
bot_1.A1 [in CoMoEx.IntroElim]
bot_1.p [in CoMoEx.IntroElim]
C
comm.p [in CoMoEx.Laws]comm.q [in CoMoEx.Laws]
contrapos.p [in CoMoEx.Laws]
contrapos.q [in CoMoEx.Laws]
currying.p [in CoMoEx.Laws]
currying.q [in CoMoEx.Laws]
currying.r [in CoMoEx.Laws]
D
de_morgan.q [in CoMoEx.Laws]de_morgan.p [in CoMoEx.Laws]
distr.p [in CoMoEx.Laws]
distr.q [in CoMoEx.Laws]
distr.r [in CoMoEx.Laws]
E
existsE_demo.existsE_demo_2.A2 [in CoMoEx.Exists]existsE_demo.existsE_demo_2.A1 [in CoMoEx.Exists]
existsE_demo.existsE_demo_2.P [in CoMoEx.Exists]
existsE_demo.existsE_demo_1.A1 [in CoMoEx.Exists]
existsE_demo.Q [in CoMoEx.Exists]
existsE_demo.T [in CoMoEx.Exists]
existsI_demo.existsI_demo_3.A1 [in CoMoEx.Exists]
existsI_demo.existsI_demo_3.x [in CoMoEx.Exists]
existsI_demo.existsI_demo_3.P [in CoMoEx.Exists]
existsI_demo.existsI_demo_2.A1 [in CoMoEx.Exists]
existsI_demo.existsI_demo_2.some_t [in CoMoEx.Exists]
existsI_demo.existsI_demo_2.P [in CoMoEx.Exists]
existsI_demo.existsI_demo_1.A1 [in CoMoEx.Exists]
existsI_demo.existsI_demo_1.some_t [in CoMoEx.Exists]
existsI_demo.existsI_demo_1.Q [in CoMoEx.Exists]
existsI_demo.T [in CoMoEx.Exists]
exists_comm_ops.exists_comm_or_2.H1 [in CoMoEx.Exists]
exists_comm_ops.exists_comm_or_1.H1 [in CoMoEx.Exists]
exists_comm_ops.exists_comm_and_2.H1 [in CoMoEx.Exists]
exists_comm_ops.exists_comm_and_1.H1 [in CoMoEx.Exists]
exists_comm_ops.Q [in CoMoEx.Exists]
exists_comm_ops.P [in CoMoEx.Exists]
exists_comm_ops.T [in CoMoEx.Exists]
F
forallE_demo.forallE_demo_2.A1 [in CoMoEx.Forall]forallE_demo.forallE_demo_2.P [in CoMoEx.Forall]
forallE_demo.forallE_demo_1.A1 [in CoMoEx.Forall]
forallE_demo.forallE_demo_1.Q [in CoMoEx.Forall]
forallE_demo.some_t [in CoMoEx.Forall]
forallE_demo.T [in CoMoEx.Forall]
forallI_demo.forallI_demo_2.A1 [in CoMoEx.Forall]
forallI_demo.forallI_demo_2.P [in CoMoEx.Forall]
forallI_demo.forallI_demo_1.A1 [in CoMoEx.Forall]
forallI_demo.forallI_demo_1.Q [in CoMoEx.Forall]
forallI_demo.T [in CoMoEx.Forall]
forall_ex_7.P [in CoMoEx.Forall]
forall_ex_7.T [in CoMoEx.Forall]
forall_ex_6.A2 [in CoMoEx.Forall]
forall_ex_6.A1 [in CoMoEx.Forall]
forall_ex_6.R [in CoMoEx.Forall]
forall_ex_6.P [in CoMoEx.Forall]
forall_ex_6.z [in CoMoEx.Forall]
forall_ex_6.T [in CoMoEx.Forall]
forall_ex_5.A3 [in CoMoEx.Forall]
forall_ex_5.A2 [in CoMoEx.Forall]
forall_ex_5.A1 [in CoMoEx.Forall]
forall_ex_5.R [in CoMoEx.Forall]
forall_ex_5.T [in CoMoEx.Forall]
forall_ex_4.A2 [in CoMoEx.Forall]
forall_ex_4.A1 [in CoMoEx.Forall]
forall_ex_4.S [in CoMoEx.Forall]
forall_ex_4.R [in CoMoEx.Forall]
forall_ex_4.P [in CoMoEx.Forall]
forall_ex_4.T [in CoMoEx.Forall]
forall_ex_3.A3 [in CoMoEx.Forall]
forall_ex_3.A2 [in CoMoEx.Forall]
forall_ex_3.A1 [in CoMoEx.Forall]
forall_ex_3.R [in CoMoEx.Forall]
forall_ex_3.Q [in CoMoEx.Forall]
forall_ex_3.P [in CoMoEx.Forall]
forall_ex_3.T [in CoMoEx.Forall]
forall_ex_2.A2 [in CoMoEx.Forall]
forall_ex_2.A1 [in CoMoEx.Forall]
forall_ex_2.R [in CoMoEx.Forall]
forall_ex_2.Q [in CoMoEx.Forall]
forall_ex_2.P [in CoMoEx.Forall]
forall_ex_2.T [in CoMoEx.Forall]
forall_ex_1.A1 [in CoMoEx.Forall]
forall_ex_1.P [in CoMoEx.Forall]
forall_ex_1.T [in CoMoEx.Forall]
forall_comm_ops.forall_comm_iff_2.H1 [in CoMoEx.Forall]
forall_comm_ops.forall_comm_iff_1.H1 [in CoMoEx.Forall]
forall_comm_ops.forall_comm_impl_2.H1 [in CoMoEx.Forall]
forall_comm_ops.forall_comm_impl_1.H1 [in CoMoEx.Forall]
forall_comm_ops.forall_comm_or_2.H1 [in CoMoEx.Forall]
forall_comm_ops.forall_comm_or_1.H1 [in CoMoEx.Forall]
forall_comm_ops.forall_comm_and_2.H1 [in CoMoEx.Forall]
forall_comm_ops.forall_comm_and_1.H1 [in CoMoEx.Forall]
forall_comm_ops.Q [in CoMoEx.Forall]
forall_comm_ops.P [in CoMoEx.Forall]
forall_comm_ops.T [in CoMoEx.Forall]
H
how_to_use_Laws.p2 [in CoMoEx.SomeExamples]how_to_use_Laws.p1 [in CoMoEx.SomeExamples]
I
idem.p [in CoMoEx.Laws]iff_3.A2 [in CoMoEx.IntroElim]
iff_3.A1 [in CoMoEx.IntroElim]
iff_3.q [in CoMoEx.IntroElim]
iff_3.p [in CoMoEx.IntroElim]
iff_2.A2 [in CoMoEx.IntroElim]
iff_2.A1 [in CoMoEx.IntroElim]
iff_2.q [in CoMoEx.IntroElim]
iff_2.p [in CoMoEx.IntroElim]
iff_1.A2 [in CoMoEx.IntroElim]
iff_1.A1 [in CoMoEx.IntroElim]
iff_1.q [in CoMoEx.IntroElim]
iff_1.p [in CoMoEx.IntroElim]
implsem.p [in CoMoEx.Laws]
implsem.q [in CoMoEx.Laws]
impl_2.A2 [in CoMoEx.IntroElim]
impl_2.A1 [in CoMoEx.IntroElim]
impl_2.q [in CoMoEx.IntroElim]
impl_2.p [in CoMoEx.IntroElim]
impl_1.A1 [in CoMoEx.IntroElim]
impl_1.q [in CoMoEx.IntroElim]
impl_1.p [in CoMoEx.IntroElim]
impl_trans.A2 [in CoMoEx.Laws]
impl_trans.A1 [in CoMoEx.Laws]
impl_trans.r [in CoMoEx.Laws]
impl_trans.q [in CoMoEx.Laws]
impl_trans.p [in CoMoEx.Laws]
L
logic_vol1.mini_ex.H3 [in CoMoEx.Induction]logic_vol1.mini_ex.H2 [in CoMoEx.Induction]
logic_vol1.mini_ex.H1 [in CoMoEx.Induction]
logic_vol1.mini_ex.k [in CoMoEx.Induction]
logic_vol1.mini_ex.A [in CoMoEx.Induction]
logic_vol1.mini_ex.f [in CoMoEx.Induction]
N
neg_2.A1 [in CoMoEx.IntroElim]neg_2.p [in CoMoEx.IntroElim]
neg_1.A1 [in CoMoEx.IntroElim]
neg_1.p [in CoMoEx.IntroElim]
neutr.p [in CoMoEx.Laws]
O
or_3.A3 [in CoMoEx.IntroElim]or_3.A2 [in CoMoEx.IntroElim]
or_3.A1 [in CoMoEx.IntroElim]
or_3.r [in CoMoEx.IntroElim]
or_3.q [in CoMoEx.IntroElim]
or_3.p [in CoMoEx.IntroElim]
or_2.A1 [in CoMoEx.IntroElim]
or_2.q [in CoMoEx.IntroElim]
or_2.p [in CoMoEx.IntroElim]
or_1.A1 [in CoMoEx.IntroElim]
or_1.q [in CoMoEx.IntroElim]
or_1.p [in CoMoEx.IntroElim]
P
peirce_law.q [in CoMoEx.Laws]peirce_law.p [in CoMoEx.Laws]
p_not_p.p [in CoMoEx.Laws]
S
se_7.p2 [in CoMoEx.SomeExamples]se_7.p1 [in CoMoEx.SomeExamples]
se_6.A1 [in CoMoEx.SomeExamples]
se_6.p2 [in CoMoEx.SomeExamples]
se_6.p1 [in CoMoEx.SomeExamples]
se_5.A1 [in CoMoEx.SomeExamples]
se_5.p2 [in CoMoEx.SomeExamples]
se_5.p1 [in CoMoEx.SomeExamples]
se_4.A1 [in CoMoEx.SomeExamples]
se_4.p3 [in CoMoEx.SomeExamples]
se_4.p2 [in CoMoEx.SomeExamples]
se_4.p1 [in CoMoEx.SomeExamples]
se_3.A6 [in CoMoEx.SomeExamples]
se_3.A5 [in CoMoEx.SomeExamples]
se_3.A4 [in CoMoEx.SomeExamples]
se_3.A3 [in CoMoEx.SomeExamples]
se_3.A2 [in CoMoEx.SomeExamples]
se_3.A1 [in CoMoEx.SomeExamples]
se_3.p5 [in CoMoEx.SomeExamples]
se_3.p4 [in CoMoEx.SomeExamples]
se_3.p3 [in CoMoEx.SomeExamples]
se_3.p2 [in CoMoEx.SomeExamples]
se_3.p1 [in CoMoEx.SomeExamples]
se_2.A1 [in CoMoEx.SomeExamples]
se_2.p4 [in CoMoEx.SomeExamples]
se_2.p3 [in CoMoEx.SomeExamples]
se_2.p2 [in CoMoEx.SomeExamples]
se_2.p1 [in CoMoEx.SomeExamples]
se_1.A2 [in CoMoEx.SomeExamples]
se_1.A1 [in CoMoEx.SomeExamples]
se_1.p4 [in CoMoEx.SomeExamples]
se_1.p3 [in CoMoEx.SomeExamples]
se_1.p2 [in CoMoEx.SomeExamples]
se_1.p1 [in CoMoEx.SomeExamples]
T
trivial_iff.p [in CoMoEx.Laws]File Index
E
ExistsF
ForallG
GroupsI
InductionIntroElim
L
LawsS
SomeExamplesLemma Index
A
absorb_or [in CoMoEx.Laws]absorb_and [in CoMoEx.Laws]
and_E2 [in CoMoEx.IntroElim]
and_E1 [in CoMoEx.IntroElim]
and_I [in CoMoEx.IntroElim]
and_assoc [in CoMoEx.Laws]
and_comm [in CoMoEx.Laws]
B
bool_charac [in CoMoEx.Groups]bot_E [in CoMoEx.IntroElim]
bot_I [in CoMoEx.IntroElim]
C
contrapos [in CoMoEx.Laws]curry [in CoMoEx.Laws]
D
de_morgan_2 [in CoMoEx.Laws]de_morgan_1 [in CoMoEx.Laws]
distr_2 [in CoMoEx.Laws]
distr_1 [in CoMoEx.Laws]
E
excluded_middle [in CoMoEx.Laws]existsE_demo_2 [in CoMoEx.Exists]
existsE_demo_1 [in CoMoEx.Exists]
existsI_demo_3 [in CoMoEx.Exists]
existsI_demo_2 [in CoMoEx.Exists]
existsI_demo_1 [in CoMoEx.Exists]
exists_comm_or_2_1 [in CoMoEx.Exists]
exists_comm_or_1_1 [in CoMoEx.Exists]
exists_comm_and_2_1 [in CoMoEx.Exists]
exists_comm_and_1_1 [in CoMoEx.Exists]
F
forallE_demo_2 [in CoMoEx.Forall]forallE_demo_1 [in CoMoEx.Forall]
forallI_demo_2 [in CoMoEx.Forall]
forallI_demo_1 [in CoMoEx.Forall]
forall_ex_7_1 [in CoMoEx.Forall]
forall_ex_6_1 [in CoMoEx.Forall]
forall_ex_5_1 [in CoMoEx.Forall]
forall_ex_4_1 [in CoMoEx.Forall]
forall_ex_3_1 [in CoMoEx.Forall]
forall_ex_2_1 [in CoMoEx.Forall]
forall_ex_1_1 [in CoMoEx.Forall]
forall_comm_iff_2_1 [in CoMoEx.Forall]
forall_comm_iff_1_1 [in CoMoEx.Forall]
forall_comm_impl_2_1 [in CoMoEx.Forall]
forall_comm_impl_1_1 [in CoMoEx.Forall]
forall_comm_or_2_1 [in CoMoEx.Forall]
forall_comm_or_1_1 [in CoMoEx.Forall]
forall_comm_and_2_1 [in CoMoEx.Forall]
forall_comm_and_1_1 [in CoMoEx.Forall]
I
idem_or [in CoMoEx.Laws]idem_and [in CoMoEx.Laws]
iff_E_2 [in CoMoEx.IntroElim]
iff_E_1 [in CoMoEx.IntroElim]
iff_I [in CoMoEx.IntroElim]
impl_E [in CoMoEx.IntroElim]
impl_I [in CoMoEx.IntroElim]
impl_trans [in CoMoEx.Laws]
impl_with_conj [in CoMoEx.Laws]
impl_with_disj [in CoMoEx.Laws]
L
logic_vol1.disjunctive_correctness [in CoMoEx.Induction]M
mod_tollens [in CoMoEx.Laws]N
nat_exercises.know_this_one [in CoMoEx.Induction]nat_exercises.mulN_assoc [in CoMoEx.Induction]
nat_exercises.addN_mulN_distr_2 [in CoMoEx.Induction]
nat_exercises.addN_mulN_distr_1 [in CoMoEx.Induction]
nat_exercises.mulN_comm [in CoMoEx.Induction]
nat_exercises.mulN_n_succ_m [in CoMoEx.Induction]
nat_exercises.mulN_zero_r [in CoMoEx.Induction]
nat_exercises.addN_assoc [in CoMoEx.Induction]
nat_exercises.my_nat_iso_to_nat [in CoMoEx.Induction]
nat_playground.addN_comm' [in CoMoEx.Induction]
nat_playground.addN_comm [in CoMoEx.Induction]
nat_playground.addN_n_succ_m [in CoMoEx.Induction]
nat_playground.addN_zero_r [in CoMoEx.Induction]
neg_E [in CoMoEx.IntroElim]
neg_I [in CoMoEx.IntroElim]
neutr_or [in CoMoEx.Laws]
neutr_and [in CoMoEx.Laws]
O
or_E [in CoMoEx.IntroElim]or_I2 [in CoMoEx.IntroElim]
or_I1 [in CoMoEx.IntroElim]
or_assoc [in CoMoEx.Laws]
or_comm [in CoMoEx.Laws]
P
peirce [in CoMoEx.Laws]p_and_not_p [in CoMoEx.Laws]
S
se_7_1 [in CoMoEx.SomeExamples]se_6_1 [in CoMoEx.SomeExamples]
se_5_1 [in CoMoEx.SomeExamples]
se_4_1 [in CoMoEx.SomeExamples]
se_3_1 [in CoMoEx.SomeExamples]
se_2_3 [in CoMoEx.SomeExamples]
se_2_2 [in CoMoEx.SomeExamples]
se_2_1 [in CoMoEx.SomeExamples]
T
trivial_iff_false [in CoMoEx.Laws]trivial_iff_true [in CoMoEx.Laws]
T12 [in CoMoEx.SomeExamples]
T13 [in CoMoEx.SomeExamples]
T14 [in CoMoEx.SomeExamples]
T23 [in CoMoEx.SomeExamples]
T24 [in CoMoEx.SomeExamples]
T34 [in CoMoEx.SomeExamples]
X
xor_left_id_inv_exists [in CoMoEx.Groups]xor_assoc [in CoMoEx.Groups]
Constructor Index
L
logic_vol1.iff [in CoMoEx.Induction]logic_vol1.impl [in CoMoEx.Induction]
logic_vol1.disj [in CoMoEx.Induction]
logic_vol1.conj [in CoMoEx.Induction]
logic_vol1.neg [in CoMoEx.Induction]
logic_vol1.atom [in CoMoEx.Induction]
logic_vol1.top [in CoMoEx.Induction]
logic_vol1.bot [in CoMoEx.Induction]
N
nat_playground.succ [in CoMoEx.Induction]nat_playground.zero [in CoMoEx.Induction]
Inductive Index
L
logic_vol1.form [in CoMoEx.Induction]N
nat_playground.my_nat [in CoMoEx.Induction]Section Index
A
absorb [in CoMoEx.Laws]and_2 [in CoMoEx.IntroElim]
and_1 [in CoMoEx.IntroElim]
assoc [in CoMoEx.Laws]
B
bot_2 [in CoMoEx.IntroElim]bot_1 [in CoMoEx.IntroElim]
C
comm [in CoMoEx.Laws]contrapos [in CoMoEx.Laws]
currying [in CoMoEx.Laws]
D
de_morgan [in CoMoEx.Laws]distr [in CoMoEx.Laws]
E
existsE_demo.existsE_demo_2 [in CoMoEx.Exists]existsE_demo.existsE_demo_1 [in CoMoEx.Exists]
existsE_demo [in CoMoEx.Exists]
existsI_demo.existsI_demo_3 [in CoMoEx.Exists]
existsI_demo.existsI_demo_2 [in CoMoEx.Exists]
existsI_demo.existsI_demo_1 [in CoMoEx.Exists]
existsI_demo [in CoMoEx.Exists]
exists_comm_ops.exists_comm_or_2 [in CoMoEx.Exists]
exists_comm_ops.exists_comm_or_1 [in CoMoEx.Exists]
exists_comm_ops.exists_comm_and_2 [in CoMoEx.Exists]
exists_comm_ops.exists_comm_and_1 [in CoMoEx.Exists]
exists_comm_ops [in CoMoEx.Exists]
F
forallE_demo.forallE_demo_2 [in CoMoEx.Forall]forallE_demo.forallE_demo_1 [in CoMoEx.Forall]
forallE_demo [in CoMoEx.Forall]
forallI_demo.forallI_demo_2 [in CoMoEx.Forall]
forallI_demo.forallI_demo_1 [in CoMoEx.Forall]
forallI_demo [in CoMoEx.Forall]
forall_ex_7 [in CoMoEx.Forall]
forall_ex_6 [in CoMoEx.Forall]
forall_ex_5 [in CoMoEx.Forall]
forall_ex_4 [in CoMoEx.Forall]
forall_ex_3 [in CoMoEx.Forall]
forall_ex_2 [in CoMoEx.Forall]
forall_ex_1 [in CoMoEx.Forall]
forall_comm_ops.forall_comm_iff_2 [in CoMoEx.Forall]
forall_comm_ops.forall_comm_iff_1 [in CoMoEx.Forall]
forall_comm_ops.forall_comm_impl_2 [in CoMoEx.Forall]
forall_comm_ops.forall_comm_impl_1 [in CoMoEx.Forall]
forall_comm_ops.forall_comm_or_2 [in CoMoEx.Forall]
forall_comm_ops.forall_comm_or_1 [in CoMoEx.Forall]
forall_comm_ops.forall_comm_and_2 [in CoMoEx.Forall]
forall_comm_ops.forall_comm_and_1 [in CoMoEx.Forall]
forall_comm_ops [in CoMoEx.Forall]
H
how_to_use_Laws [in CoMoEx.SomeExamples]I
idem [in CoMoEx.Laws]iff_3 [in CoMoEx.IntroElim]
iff_2 [in CoMoEx.IntroElim]
iff_1 [in CoMoEx.IntroElim]
implsem [in CoMoEx.Laws]
impl_2 [in CoMoEx.IntroElim]
impl_1 [in CoMoEx.IntroElim]
impl_trans [in CoMoEx.Laws]
L
logic_vol1.mini_ex [in CoMoEx.Induction]N
neg_2 [in CoMoEx.IntroElim]neg_1 [in CoMoEx.IntroElim]
neutr [in CoMoEx.Laws]
O
or_3 [in CoMoEx.IntroElim]or_2 [in CoMoEx.IntroElim]
or_1 [in CoMoEx.IntroElim]
P
peirce_law [in CoMoEx.Laws]p_not_p [in CoMoEx.Laws]
S
se_7 [in CoMoEx.SomeExamples]se_6 [in CoMoEx.SomeExamples]
se_5 [in CoMoEx.SomeExamples]
se_4 [in CoMoEx.SomeExamples]
se_3 [in CoMoEx.SomeExamples]
se_2 [in CoMoEx.SomeExamples]
se_1 [in CoMoEx.SomeExamples]
T
trivial_iff [in CoMoEx.Laws]Definition Index
H
how_to_use_Laws_2 [in CoMoEx.SomeExamples]how_to_use_Laws_1 [in CoMoEx.SomeExamples]
I
is_left_inv [in CoMoEx.Groups]is_left_id [in CoMoEx.Groups]
is_assoc [in CoMoEx.Groups]
L
logic_vol1.only_bot_atom_disj [in CoMoEx.Induction]logic_vol1.contains [in CoMoEx.Induction]
logic_vol1.evaluate [in CoMoEx.Induction]
logic_vol1.atoms [in CoMoEx.Induction]
N
nat_exercises.addRow [in CoMoEx.Induction]nat_exercises.mulN [in CoMoEx.Induction]
nat_exercises.bij [in CoMoEx.Induction]
nat_exercises.sur [in CoMoEx.Induction]
nat_exercises.inj [in CoMoEx.Induction]
nat_exercises.my_nat_to_nat [in CoMoEx.Induction]
nat_playground.addN [in CoMoEx.Induction]
| 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 | (572 entries) |
| Binder 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 | (165 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 | (3 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 | (199 entries) |
| File 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) |
| 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 | (99 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 | (10 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 | (2 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 | (71 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 | (16 entries) |
This page has been generated by coqdoc