Global Index

other

(221 entries)

Notation Index

other

(2 entries)

Library Index

other

(5 entries)

Lemma Index

other

(99 entries)

Axiom Index

other

(16 entries)

Constructor Index

other

(47 entries)

Inductive Index

other

(13 entries)

Instance Index

other

(4 entries)

Abbreviation Index

other

(8 entries)

Definition Index

other

(27 entries)

Global Index

A

A [axiom, in td1_sol]
Absurd [constructor, in prop]
addnSm [lemma, in td2_sol]
addn0 [lemma, in td2_sol]
addSnm [lemma, in td2_sol]
add_ass [lemma, in td2_sol]
add_com [lemma, in td2_sol]
add0n [lemma, in td2_sol]
allSN [definition, in stlc]
allSN_acc [lemma, in stlc]
allSN0 [lemma, in stlc]
AndEL [constructor, in prop]
AndER [constructor, in prop]
AndI [constructor, in prop]
App [constructor, in stlc]
app [definition, in lists_sol]
app_length [lemma, in lists_sol]
app_ass [lemma, in lists_sol]
Arr [constructor, in stlc]
assn [inductive, in prop]
Ax [constructor, in prop]

B

B [axiom, in td1_sol]
Base [constructor, in stlc]

C

C [axiom, in td1_sol]
calc [lemma, in td2_sol]
comp [definition, in lists_sol]
comp_corr [lemma, in lists_sol]
cons [constructor, in lists_sol]
correctness [lemma, in prop]
CR [definition, in stlc]
CR_ren [lemma, in stlc]
CR_ren_apps [lemma, in stlc]
CR_stepI [lemma, in stlc]
CR_step [lemma, in stlc]
CR_step_r [lemma, in stlc]
CR_var [lemma, in stlc]
CR_SN [lemma, in stlc]
CR_SN_r [lemma, in stlc]

D

D [axiom, in td1_sol]
demo2 [lemma, in td1_sol]
demo3 [lemma, in td1_sol]
demo4 [lemma, in td1_sol]
demo5 [lemma, in td1_sol]
div2 [lemma, in td2_sol]
dn [inductive, in prop]

E

eq_dec [lemma, in td2_sol]
ex [lemma, in lists_sol]
ex0 [lemma, in td1_sol]
ex1 [lemma, in td1_sol]
ex10 [lemma, in td1_sol]
ex11 [lemma, in td1_sol]
ex2 [lemma, in td1_sol]
ex3 [lemma, in td1_sol]
ex4 [lemma, in td1_sol]
ex5 [lemma, in td1_sol]
ex6 [lemma, in td1_sol]
ex7 [lemma, in td1_sol]
ex8 [lemma, in td1_sol]
ex9 [lemma, in td1_sol]

F

FalseE [constructor, in prop]
foo [lemma, in td1_sol]
foo [lemma, in td1_sol]
foo [lemma, in td1_sol]
foo [lemma, in td1_sol]
foo [lemma, in td1_sol]
foo [lemma, in td1_sol]

I

Ids_term [instance, in stlc]
ifassn [inductive, in prop]
ifassn_correct [lemma, in prop]
ifassn_of_assn [definition, in prop]
ifsem [definition, in prop]
ImpE [constructor, in prop]
ImpI [constructor, in prop]
ins [definition, in lists_sol]
ins_permutt [lemma, in lists_sol]
ins_sorted_aux [lemma, in lists_sol]
ins_permut [lemma, in lists_sol]
ins_ex [lemma, in lists_sol]
is_tautology_complete [lemma, in prop]
is_tautology_correct [lemma, in prop]
is_tautology [definition, in prop]

L

Lam [constructor, in stlc]
Leaf [constructor, in lists_sol]
length [definition, in lists_sol]
list [inductive, in lists_sol]
lists_sol [library]
loop [definition, in stlc]
lower [definition, in lists_sol]
lower_trans [lemma, in lists_sol]
l1 [lemma, in td1_sol]

N

neutral [definition, in stlc]
nifassn [inductive, in prop]
nifassn_tauto_complete [lemma, in prop]
nifassn_tauto_r_complete [lemma, in prop]
nifassn_tauto_correct [lemma, in prop]
nifassn_tauto_r_correct [lemma, in prop]
nifassn_tauto [definition, in prop]
nifassn_tauto_r [definition, in prop]
nifsem [definition, in prop]
nil [constructor, in lists_sol]
Node [constructor, in lists_sol]
norm [definition, in prop]
normif [definition, in prop]
normif_correct [lemma, in prop]
norm_correct [lemma, in prop]

O

onth [abbreviation, in stlc]
OrE [constructor, in prop]
OrIL [constructor, in prop]
OrIR [constructor, in prop]

P

P [axiom, in td1_sol]
pairSN_acc [lemma, in stlc]
PAnd [constructor, in prop]
permt [lemma, in lists_sol]
permut [axiom, in lists_sol]
permutt [definition, in lists_sol]
permut_congr [axiom, in lists_sol]
permut_step [axiom, in lists_sol]
permut_trans [axiom, in lists_sol]
permut_refl [axiom, in lists_sol]
perm_trans [axiom, in lists_sol]
perm_nil' [axiom, in lists_sol]
perm_nil [axiom, in lists_sol]
PFalse [constructor, in prop]
PIConst [constructor, in prop]
PIff [abbreviation, in prop]
PIIf [constructor, in prop]
PImp [constructor, in prop]
PIVar [constructor, in prop]
PNIConst [constructor, in prop]
PNIIf [constructor, in prop]
PNIVar [constructor, in prop]
PNot [abbreviation, in prop]
POr [constructor, in prop]
PQ [axiom, in td1_sol]
prop [library]
PTrue [abbreviation, in prop]
PVar [constructor, in prop]

Q

Q [axiom, in td1_sol]
q1 [lemma, in td1_sol]
q2 [lemma, in td1_sol]
q3 [lemma, in td1_sol]

R

red [abbreviation, in stlc]
reds [abbreviation, in stlc]
Rename_term [instance, in stlc]

S

sat [definition, in prop]
sem [definition, in prop]
sim [inductive, in stlc]
SimApp [constructor, in stlc]
SimBnd [constructor, in stlc]
SimLam [constructor, in stlc]
SimVar [constructor, in stlc]
sim_subst_0 [lemma, in stlc]
sim_subst [lemma, in stlc]
sim_renL [lemma, in stlc]
sim_renL_r [lemma, in stlc]
sim_ren_n [lemma, in stlc]
sim_ren [lemma, in stlc]
sim_weak [lemma, in stlc]
sim_trans [lemma, in stlc]
sim_sym [lemma, in stlc]
sim_refl [lemma, in stlc]
SN [abbreviation, in stlc]
SN_ren_apps [lemma, in stlc]
SN_sim [lemma, in stlc]
SN_step [lemma, in stlc]
SN_apps_var [lemma, in stlc]
SN_var [lemma, in stlc]
SN_lamI [lemma, in stlc]
SN_appIR [lemma, in stlc]
SN_appIL [lemma, in stlc]
SN_subterm [lemma, in stlc]
SN_stepI [lemma, in stlc]
sorted [definition, in lists_sol]
step [inductive, in stlc]
steps [inductive, in stlc]
step_sim [lemma, in stlc]
step_apps_varI [lemma, in stlc]
step_subterm [lemma, in stlc]
step_subst [lemma, in stlc]
Step_lam [constructor, in stlc]
Step_appR [constructor, in stlc]
Step_appL [constructor, in stlc]
Step_beta [constructor, in stlc]
Step1 [constructor, in stlc]
stlc [library]
stupid [lemma, in td1_sol]
SubAppL [constructor, in stlc]
SubAppR [constructor, in stlc]
subenv [definition, in prop]
subenv_dn [lemma, in prop]
subenv_cons [definition, in prop]
SubLam [constructor, in stlc]
SubstLemmas_term [instance, in stlc]
Subst_term [instance, in stlc]
subterm [inductive, in stlc]
SubTop [constructor, in stlc]

T

td1_sol [library]
td2_sol [library]
term [inductive, in stlc]
tinsert [definition, in lists_sol]
tree [inductive, in lists_sol]
tri [definition, in lists_sol]
tri_sorted [lemma, in lists_sol]
tri_permut [lemma, in lists_sol]
ty [inductive, in stlc]
type [inductive, in stlc]
ty_SN [lemma, in stlc]
ty_CR [lemma, in stlc]
ty_pres [lemma, in stlc]
ty_subst [lemma, in stlc]
ty_ren [lemma, in stlc]
Ty_App [constructor, in stlc]
Ty_Lam [constructor, in stlc]
Ty_Var [constructor, in stlc]