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

(994 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

(38 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

(77 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

(19 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

(446 entries)

Axiom 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

(15 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

(207 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

(12 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

(30 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

(5 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

(1 entry)

Abbreviation 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)

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

(130 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

(12 entries)

---

Global Index

A

admissible [module, in DCOIOmega.admissible]
admissible [library]
admissible.cfacts [module, in DCOIOmega.admissible]
admissible.ifacts [module, in DCOIOmega.admissible]
admissible.preservation [module, in DCOIOmega.admissible]
admissible.solver [module, in DCOIOmega.admissible]
admissible.tcfacts [module, in DCOIOmega.admissible]
admissible.T_Proj2_Alt [lemma, in DCOIOmega.admissible]
admissible.T_Proj2 [lemma, in DCOIOmega.admissible]
admissible.T_Proj2_leq [lemma, in DCOIOmega.admissible]
admissible.T_Proj1 [lemma, in DCOIOmega.admissible]
admissible.T_Unbox [lemma, in DCOIOmega.admissible]
admissible.T_Box [lemma, in DCOIOmega.admissible]
admissible.T_T [lemma, in DCOIOmega.admissible]
admissible.T_Down_Alt [lemma, in DCOIOmega.admissible]
All [library]
ap [definition, in DCOIOmega.Autosubst2.unscoped]
apc [definition, in DCOIOmega.Autosubst2.unscoped]
axioms [library]

C

cod [definition, in DCOIOmega.Autosubst2.axioms]
cod_comp [definition, in DCOIOmega.Autosubst2.axioms]
cod_ext [definition, in DCOIOmega.Autosubst2.axioms]
cod_id [definition, in DCOIOmega.Autosubst2.axioms]
cod_map [definition, in DCOIOmega.Autosubst2.axioms]
consistency [module, in DCOIOmega.consistency]
consistency [library]
consistency.consistency [lemma, in DCOIOmega.consistency]
consistency.ne_contra [lemma, in DCOIOmega.consistency]
consistency.preservation [module, in DCOIOmega.consistency]
consistency.soundness [module, in DCOIOmega.consistency]
conv [library]
conv_facts.conv_par_star2 [lemma, in DCOIOmega.conv]
conv_facts.iconv_par_star2 [lemma, in DCOIOmega.conv]
conv_facts.iconv_par_star [lemma, in DCOIOmega.conv]
conv_facts.iconv_conv [lemma, in DCOIOmega.conv]
conv_facts.conv_renaming [lemma, in DCOIOmega.conv]
conv_facts.iconv_renaming [lemma, in DCOIOmega.conv]
conv_facts.iconv_iok_downgrade [lemma, in DCOIOmega.conv]
conv_facts.conv_eq_inj [lemma, in DCOIOmega.conv]
conv_facts.conv_sig_inj [lemma, in DCOIOmega.conv]
conv_facts.conv_pi_inj [lemma, in DCOIOmega.conv]
conv_facts.iconv_sig_inj [lemma, in DCOIOmega.conv]
conv_facts.iconv_pi_inj [lemma, in DCOIOmega.conv]
conv_facts.conv_univ_inj [lemma, in DCOIOmega.conv]
conv_facts.ieq_conv [lemma, in DCOIOmega.conv]
conv_facts.conv_subst [lemma, in DCOIOmega.conv]
conv_facts.iconv_subst [lemma, in DCOIOmega.conv]
conv_facts.conv_trans [lemma, in DCOIOmega.conv]
conv_facts.iconv_trans [lemma, in DCOIOmega.conv]
conv_facts.iconv_trans_heterogeneous_leq' [lemma, in DCOIOmega.conv]
conv_facts.iconv_trans_heterogeneous_leq [lemma, in DCOIOmega.conv]
conv_facts.iconv_trans_heterogeneous [lemma, in DCOIOmega.conv]
conv_facts.ieq_trans_heterogeneous_leq' [lemma, in DCOIOmega.conv]
conv_facts.ieq_trans_heterogeneous_leq [lemma, in DCOIOmega.conv]
conv_facts.ieq_trans_heterogeneous [lemma, in DCOIOmega.conv]
conv_facts.iconv_par2 [lemma, in DCOIOmega.conv]
conv_facts.conv_par [lemma, in DCOIOmega.conv]
conv_facts.iconv_par [lemma, in DCOIOmega.conv]
conv_facts.conv_rpar [lemma, in DCOIOmega.conv]
conv_facts.iconv_rpar [lemma, in DCOIOmega.conv]
conv_facts.conv_sym [lemma, in DCOIOmega.conv]
conv_facts.iconv_sym [lemma, in DCOIOmega.conv]
conv_facts.conv_refl [lemma, in DCOIOmega.conv]
conv_facts.simulation_star [lemma, in DCOIOmega.conv]
conv_facts.simulation [lemma, in DCOIOmega.conv]
conv_facts.iok_preservation_star [lemma, in DCOIOmega.conv]
conv_facts.iok_preservation [lemma, in DCOIOmega.conv]
conv_facts.ieq_iconv [lemma, in DCOIOmega.conv]
conv_facts.ifacts [module, in DCOIOmega.conv]
conv_facts.pfacts [module, in DCOIOmega.conv]
conv_facts [module, in DCOIOmega.conv]
conv_sig.conv [definition, in DCOIOmega.conv]
conv_sig.iconv [definition, in DCOIOmega.conv]
conv_sig [module, in DCOIOmega.conv]
conv_dec_bot.conv_dec [lemma, in DCOIOmega.iconv_dec]
conv_dec_bot.conv_convb [lemma, in DCOIOmega.iconv_dec]
conv_dec_bot.convb_conv [lemma, in DCOIOmega.iconv_dec]
conv_dec_bot.convb [definition, in DCOIOmega.iconv_dec]
conv_dec_bot.compute_level_downgrade [lemma, in DCOIOmega.iconv_dec]
conv_dec_bot.compute_level_is_min [lemma, in DCOIOmega.iconv_dec]
conv_dec_bot.ifacts [module, in DCOIOmega.iconv_dec]
conv_dec_bot.compute_level [definition, in DCOIOmega.iconv_dec]
conv_dec_bot.preservation [module, in DCOIOmega.iconv_dec]
conv_dec_bot.Solver [module, in DCOIOmega.iconv_dec]
conv_dec_bot.soundness [module, in DCOIOmega.iconv_dec]
conv_dec_bot [module, in DCOIOmega.iconv_dec]

D

dcoi_with_nat_lattice [module, in DCOIOmega.toplevel]

F

factorization [library]
factorization_sig.LoRed_normalize [definition, in DCOIOmega.factorization]
factorization_sig.LoRed'_nf_unique [lemma, in DCOIOmega.factorization]
factorization_sig.LoRed_wn_sn [lemma, in DCOIOmega.factorization]
factorization_sig.nf_no_lored [lemma, in DCOIOmega.factorization]
factorization_sig.LoReds'_Pars [lemma, in DCOIOmega.factorization]
factorization_sig.LoRed'_Par [lemma, in DCOIOmega.factorization]
factorization_sig.LoRedOpt_Par [lemma, in DCOIOmega.factorization]
factorization_sig.IsNumP [lemma, in DCOIOmega.factorization]
factorization_sig.IsNum_sind [definition, in DCOIOmega.factorization]
factorization_sig.IsNum_ind [definition, in DCOIOmega.factorization]
factorization_sig.IsNumFalse [constructor, in DCOIOmega.factorization]
factorization_sig.IsSuc [constructor, in DCOIOmega.factorization]
factorization_sig.IsZero [constructor, in DCOIOmega.factorization]
factorization_sig.IsNum [inductive, in DCOIOmega.factorization]
factorization_sig.IsPackP [lemma, in DCOIOmega.factorization]
factorization_sig.IsPack_sind [definition, in DCOIOmega.factorization]
factorization_sig.IsPack_ind [definition, in DCOIOmega.factorization]
factorization_sig.isPackFalse [constructor, in DCOIOmega.factorization]
factorization_sig.IsPackTrue [constructor, in DCOIOmega.factorization]
factorization_sig.IsPack [inductive, in DCOIOmega.factorization]
factorization_sig.IsAbsP [lemma, in DCOIOmega.factorization]
factorization_sig.IsAbs_sind [definition, in DCOIOmega.factorization]
factorization_sig.IsAbs_ind [definition, in DCOIOmega.factorization]
factorization_sig.isAbsFalse [constructor, in DCOIOmega.factorization]
factorization_sig.IsAbsTrue [constructor, in DCOIOmega.factorization]
factorization_sig.IsAbs [inductive, in DCOIOmega.factorization]
factorization_sig.standardization' [lemma, in DCOIOmega.factorization]
factorization_sig.LoReds_LoReds' [lemma, in DCOIOmega.factorization]
factorization_sig.LoRed_LoRed' [lemma, in DCOIOmega.factorization]
factorization_sig.LoRed' [definition, in DCOIOmega.factorization]
factorization_sig.LoRed_LoRedOpt [lemma, in DCOIOmega.factorization]
factorization_sig.nf_no_red [lemma, in DCOIOmega.factorization]
factorization_sig.LoRedOpt [definition, in DCOIOmega.factorization]
factorization_sig.standardization [lemma, in DCOIOmega.factorization]
factorization_sig.LoRed_Let_Cong [lemma, in DCOIOmega.factorization]
factorization_sig.LoRed_Seq_Cong [lemma, in DCOIOmega.factorization]
factorization_sig.LoRed_J_Cong [lemma, in DCOIOmega.factorization]
factorization_sig.LoRed_Eq_Cong [lemma, in DCOIOmega.factorization]
factorization_sig.LoRed_Absurd_Cong [lemma, in DCOIOmega.factorization]
factorization_sig.LoRed_Pack_Cong [lemma, in DCOIOmega.factorization]
factorization_sig.LoRed_Sig_Cong [lemma, in DCOIOmega.factorization]
factorization_sig.LoRed_Pi_Cong [lemma, in DCOIOmega.factorization]
factorization_sig.LoRed_Ind_Cong [lemma, in DCOIOmega.factorization]
factorization_sig.LoRed_App_Cong [lemma, in DCOIOmega.factorization]
factorization_sig.NPar_Unit_inv [lemma, in DCOIOmega.factorization]
factorization_sig.NPar_Zero_inv [lemma, in DCOIOmega.factorization]
factorization_sig.NPar_TT_inv [lemma, in DCOIOmega.factorization]
factorization_sig.NPar_Refl_inv [lemma, in DCOIOmega.factorization]
factorization_sig.NPar_Let_inv [lemma, in DCOIOmega.factorization]
factorization_sig.LoRed_Abs_inv [lemma, in DCOIOmega.factorization]
factorization_sig.LoRed_IsNum_inv [lemma, in DCOIOmega.factorization]
factorization_sig.LoRed_IsPack_inv [lemma, in DCOIOmega.factorization]
factorization_sig.LoRed_IsAbs_inv [lemma, in DCOIOmega.factorization]
factorization_sig.NPar_Pack_inv [lemma, in DCOIOmega.factorization]
factorization_sig.NPar_Sig_inv [lemma, in DCOIOmega.factorization]
factorization_sig.NPar_J_inv [lemma, in DCOIOmega.factorization]
factorization_sig.NPar_Eq_inv [lemma, in DCOIOmega.factorization]
factorization_sig.NPar_Absurd_inv [lemma, in DCOIOmega.factorization]
factorization_sig.NPar_Nat_inv [lemma, in DCOIOmega.factorization]
factorization_sig.NPar_Void_inv [lemma, in DCOIOmega.factorization]
factorization_sig.NPar_Univ_inv [lemma, in DCOIOmega.factorization]
factorization_sig.NPar_Pi_inv [lemma, in DCOIOmega.factorization]
factorization_sig.NPar_Ind_inv [lemma, in DCOIOmega.factorization]
factorization_sig.NPar_Seq_inv [lemma, in DCOIOmega.factorization]
factorization_sig.NPar_App_inv [lemma, in DCOIOmega.factorization]
factorization_sig.LoRed_Suc_Cong [lemma, in DCOIOmega.factorization]
factorization_sig.LoRed_Abs_Cong [lemma, in DCOIOmega.factorization]
factorization_sig.NPars_Pars [lemma, in DCOIOmega.factorization]
factorization_sig.HReds_LoReds [lemma, in DCOIOmega.factorization]
factorization_sig.HRed_LoRed [lemma, in DCOIOmega.factorization]
factorization_sig.NPar_Suc_inv [lemma, in DCOIOmega.factorization]
factorization_sig.NPar_Abs_inv [lemma, in DCOIOmega.factorization]
factorization_sig.NPar_Var_inv [lemma, in DCOIOmega.factorization]
factorization_sig.nfact [module, in DCOIOmega.factorization]
factorization_sig.LoRed_sind [definition, in DCOIOmega.factorization]
factorization_sig.LoRed_ind [definition, in DCOIOmega.factorization]
factorization_sig.LoR_SeqTT [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_Seq1 [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_Seq0 [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_Suc [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_IndSuc [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_IndZero [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_Ind2 [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_Ind1 [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_Ind0 [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_LetPack [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_Let1 [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_Let0 [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_Pack1 [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_Pack0 [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_Sig1 [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_Sig0 [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_JRefl [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_J1 [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_J0 [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_Eq1 [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_Eq0 [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_Absurd [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_AppAbs [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_App1 [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_App0 [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_Abs [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_Pi1 [constructor, in DCOIOmega.factorization]
factorization_sig.LoR_Pi0 [constructor, in DCOIOmega.factorization]
factorization_sig.LoRed [inductive, in DCOIOmega.factorization]
factorization_sig.isNum [definition, in DCOIOmega.factorization]
factorization_sig.isPack [definition, in DCOIOmega.factorization]
factorization_sig.isAbs [definition, in DCOIOmega.factorization]
factorization_sig.factorization [lemma, in DCOIOmega.factorization]
factorization_sig.local_postponement_star [lemma, in DCOIOmega.factorization]
factorization_sig.local_postponement [lemma, in DCOIOmega.factorization]
factorization_sig.starseq_erase [lemma, in DCOIOmega.factorization]
factorization_sig.split [lemma, in DCOIOmega.factorization]
factorization_sig.ipar_starseq_morphing [lemma, in DCOIOmega.factorization]
factorization_sig.starseq_ρ_par [lemma, in DCOIOmega.factorization]
factorization_sig.starseq_seq_cong [lemma, in DCOIOmega.factorization]
factorization_sig.starseq_ind_cong [lemma, in DCOIOmega.factorization]
factorization_sig.starseq_j_cong [lemma, in DCOIOmega.factorization]
factorization_sig.starseq_let_cong [lemma, in DCOIOmega.factorization]
factorization_sig.starseq_app_cong [lemma, in DCOIOmega.factorization]
factorization_sig.starseq_suc_cong [lemma, in DCOIOmega.factorization]
factorization_sig.starseq_abs_cong [lemma, in DCOIOmega.factorization]
factorization_sig.starseq_renaming [lemma, in DCOIOmega.factorization]
factorization_sig.starseq_par [lemma, in DCOIOmega.factorization]
factorization_sig.starseq_sind [definition, in DCOIOmega.factorization]
factorization_sig.starseq_ind [definition, in DCOIOmega.factorization]
factorization_sig.S_Step [constructor, in DCOIOmega.factorization]
factorization_sig.S_Refl [constructor, in DCOIOmega.factorization]
factorization_sig.starseq [inductive, in DCOIOmega.factorization]
factorization_sig.merge [lemma, in DCOIOmega.factorization]
factorization_sig.HRed_renaming [lemma, in DCOIOmega.factorization]
factorization_sig.HR_IndSuc' [lemma, in DCOIOmega.factorization]
factorization_sig.HR_LetPack' [lemma, in DCOIOmega.factorization]
factorization_sig.HR_AppAbs' [lemma, in DCOIOmega.factorization]
factorization_sig.NPar_renaming [lemma, in DCOIOmega.factorization]
factorization_sig.NPar_Par [lemma, in DCOIOmega.factorization]
factorization_sig.pfacts [module, in DCOIOmega.factorization]
factorization_sig.NPar_sind [definition, in DCOIOmega.factorization]
factorization_sig.NPar_ind [definition, in DCOIOmega.factorization]
factorization_sig.NP_Seq [constructor, in DCOIOmega.factorization]
factorization_sig.NP_Unit [constructor, in DCOIOmega.factorization]
factorization_sig.NP_TT [constructor, in DCOIOmega.factorization]
factorization_sig.NP_Ind [constructor, in DCOIOmega.factorization]
factorization_sig.NP_Suc [constructor, in DCOIOmega.factorization]
factorization_sig.NP_Zero [constructor, in DCOIOmega.factorization]
factorization_sig.NP_Nat [constructor, in DCOIOmega.factorization]
factorization_sig.NP_Refl [constructor, in DCOIOmega.factorization]
factorization_sig.NP_Void [constructor, in DCOIOmega.factorization]
factorization_sig.NP_Let [constructor, in DCOIOmega.factorization]
factorization_sig.NP_Pack [constructor, in DCOIOmega.factorization]
factorization_sig.NP_Sig [constructor, in DCOIOmega.factorization]
factorization_sig.NP_J [constructor, in DCOIOmega.factorization]
factorization_sig.NP_Eq [constructor, in DCOIOmega.factorization]
factorization_sig.NP_Absurd [constructor, in DCOIOmega.factorization]
factorization_sig.NP_App [constructor, in DCOIOmega.factorization]
factorization_sig.NP_Abs [constructor, in DCOIOmega.factorization]
factorization_sig.NP_Pi [constructor, in DCOIOmega.factorization]
factorization_sig.NP_Univ [constructor, in DCOIOmega.factorization]
factorization_sig.NP_Var [constructor, in DCOIOmega.factorization]
factorization_sig.NPar [inductive, in DCOIOmega.factorization]
factorization_sig.HRed_sind [definition, in DCOIOmega.factorization]
factorization_sig.HRed_ind [definition, in DCOIOmega.factorization]
factorization_sig.HR_SeqTT [constructor, in DCOIOmega.factorization]
factorization_sig.HR_Seq [constructor, in DCOIOmega.factorization]
factorization_sig.HR_IndSuc [constructor, in DCOIOmega.factorization]
factorization_sig.HR_IndZero [constructor, in DCOIOmega.factorization]
factorization_sig.HR_Ind [constructor, in DCOIOmega.factorization]
factorization_sig.HR_LetPack [constructor, in DCOIOmega.factorization]
factorization_sig.HR_Let [constructor, in DCOIOmega.factorization]
factorization_sig.HR_JRefl [constructor, in DCOIOmega.factorization]
factorization_sig.HR_J [constructor, in DCOIOmega.factorization]
factorization_sig.HR_AppAbs [constructor, in DCOIOmega.factorization]
factorization_sig.HR_App [constructor, in DCOIOmega.factorization]
factorization_sig.HRed [inductive, in DCOIOmega.factorization]
factorization_sig [module, in DCOIOmega.factorization]
fin [abbreviation, in DCOIOmega.Autosubst2.unscoped]
funcomp [definition, in DCOIOmega.Autosubst2.unscoped]
funcomp [definition, in DCOIOmega.Autosubst2.axioms]

G

geq [library]
geq_facts.iok_ieq_downgrade_iok [lemma, in DCOIOmega.geq]
geq_facts.ieq_trans_heterogeneous [lemma, in DCOIOmega.geq]
geq_facts.ieq_iok_subst [lemma, in DCOIOmega.geq]
geq_facts.gieq_morphing_iok [lemma, in DCOIOmega.geq]
geq_facts.ieq_morphing_iok [lemma, in DCOIOmega.geq]
geq_facts.ieq_morphing_mutual [lemma, in DCOIOmega.geq]
geq_facts.ieq_morphing_helper2 [lemma, in DCOIOmega.geq]
geq_facts.ieq_morphing_helper [lemma, in DCOIOmega.geq]
geq_facts.ieq_subst_cons [lemma, in DCOIOmega.geq]
geq_facts.ieq_subst_id [lemma, in DCOIOmega.geq]
geq_facts.gieq_refl [lemma, in DCOIOmega.geq]
geq_facts.ieq_good_morphing [definition, in DCOIOmega.geq]
geq_facts.ieq_weakening_mutual [lemma, in DCOIOmega.geq]
geq_facts.ieq_weakening_helper [definition, in DCOIOmega.geq]
geq_facts.ieq_pi_inj [lemma, in DCOIOmega.geq]
geq_facts.ieq_trans [lemma, in DCOIOmega.geq]
geq_facts.ieq_trans_mutual [lemma, in DCOIOmega.geq]
geq_facts.ieq_sym [lemma, in DCOIOmega.geq]
geq_facts.ieq_sym_mutual [lemma, in DCOIOmega.geq]
geq_facts.iok_gieq [lemma, in DCOIOmega.geq]
geq_facts.ieq_gieq [lemma, in DCOIOmega.geq]
geq_facts.iok_ieq_downgrade [lemma, in DCOIOmega.geq]
geq_facts.ieq_downgrade_leq [lemma, in DCOIOmega.geq]
geq_facts.ieq_downgrade_mutual [lemma, in DCOIOmega.geq]
geq_facts.elookup_deterministic [lemma, in DCOIOmega.geq]
geq_facts.iok_ieq [lemma, in DCOIOmega.geq]
geq_facts.iok_subst [lemma, in DCOIOmega.geq]
geq_facts.iok_morphing [lemma, in DCOIOmega.geq]
geq_facts.iok_subst_ok_up [lemma, in DCOIOmega.geq]
geq_facts.iok_subst_ok_suc [lemma, in DCOIOmega.geq]
geq_facts.iok_renaming [lemma, in DCOIOmega.geq]
geq_facts.iok_ren_ok_up [lemma, in DCOIOmega.geq]
geq_facts.iok_subst_cons [lemma, in DCOIOmega.geq]
geq_facts.iok_subst_id [lemma, in DCOIOmega.geq]
geq_facts.iok_subsumption [lemma, in DCOIOmega.geq]
geq_facts.IEq_dec [lemma, in DCOIOmega.geq]
geq_facts.IEqb_IEq [lemma, in DCOIOmega.geq]
geq_facts.nat_eqdec [lemma, in DCOIOmega.geq]
geq_facts.IEq_IEqb [lemma, in DCOIOmega.geq]
geq_facts.T_leqb_iff [lemma, in DCOIOmega.geq]
geq_facts.solver [module, in DCOIOmega.geq]
geq_facts.lprop [module, in DCOIOmega.geq]
geq_facts [module, in DCOIOmega.geq]
geq_sig.iok_subst_ok [definition, in DCOIOmega.geq]
geq_sig.iok_ren_ok [definition, in DCOIOmega.geq]
geq_sig.GIEq_ind' [definition, in DCOIOmega.geq]
geq_sig.IEq_ind' [definition, in DCOIOmega.geq]
geq_sig.IEqb [definition, in DCOIOmega.geq]
geq_sig.GIEq_sind [definition, in DCOIOmega.geq]
geq_sig.GIEq_ind [definition, in DCOIOmega.geq]
geq_sig.IEq_sind [definition, in DCOIOmega.geq]
geq_sig.IEq_ind [definition, in DCOIOmega.geq]
geq_sig.GI_InDist [constructor, in DCOIOmega.geq]
geq_sig.GI_Dist [constructor, in DCOIOmega.geq]
geq_sig.GIEq [inductive, in DCOIOmega.geq]
geq_sig.I_Seq [constructor, in DCOIOmega.geq]
geq_sig.I_TT [constructor, in DCOIOmega.geq]
geq_sig.I_Unit [constructor, in DCOIOmega.geq]
geq_sig.I_Nat [constructor, in DCOIOmega.geq]
geq_sig.I_Ind [constructor, in DCOIOmega.geq]
geq_sig.I_Suc [constructor, in DCOIOmega.geq]
geq_sig.I_Zero [constructor, in DCOIOmega.geq]
geq_sig.I_Let [constructor, in DCOIOmega.geq]
geq_sig.I_Pack [constructor, in DCOIOmega.geq]
geq_sig.I_Sig [constructor, in DCOIOmega.geq]
geq_sig.I_J [constructor, in DCOIOmega.geq]
geq_sig.I_Eq [constructor, in DCOIOmega.geq]
geq_sig.I_Refl [constructor, in DCOIOmega.geq]
geq_sig.I_Absurd [constructor, in DCOIOmega.geq]
geq_sig.I_Void [constructor, in DCOIOmega.geq]
geq_sig.I_App [constructor, in DCOIOmega.geq]
geq_sig.I_Abs [constructor, in DCOIOmega.geq]
geq_sig.I_Pi [constructor, in DCOIOmega.geq]
geq_sig.I_Univ [constructor, in DCOIOmega.geq]
geq_sig.I_Var [constructor, in DCOIOmega.geq]
geq_sig.IEq [inductive, in DCOIOmega.geq]
geq_sig.IOk_sind [definition, in DCOIOmega.geq]
geq_sig.IOk_ind [definition, in DCOIOmega.geq]
geq_sig.IO_Seq [constructor, in DCOIOmega.geq]
geq_sig.IO_TT [constructor, in DCOIOmega.geq]
geq_sig.IO_Unit [constructor, in DCOIOmega.geq]
geq_sig.IO_Nat [constructor, in DCOIOmega.geq]
geq_sig.IO_Ind [constructor, in DCOIOmega.geq]
geq_sig.IO_Suc [constructor, in DCOIOmega.geq]
geq_sig.IO_Zero [constructor, in DCOIOmega.geq]
geq_sig.IO_Let [constructor, in DCOIOmega.geq]
geq_sig.IO_Pack [constructor, in DCOIOmega.geq]
geq_sig.IO_Sig [constructor, in DCOIOmega.geq]
geq_sig.IO_J [constructor, in DCOIOmega.geq]
geq_sig.IO_Eq [constructor, in DCOIOmega.geq]
geq_sig.IO_Refl [constructor, in DCOIOmega.geq]
geq_sig.IO_Absurd [constructor, in DCOIOmega.geq]
geq_sig.IO_Void [constructor, in DCOIOmega.geq]
geq_sig.IO_App [constructor, in DCOIOmega.geq]
geq_sig.IO_Abs [constructor, in DCOIOmega.geq]
geq_sig.IO_Pi [constructor, in DCOIOmega.geq]
geq_sig.IO_Univ [constructor, in DCOIOmega.geq]
geq_sig.IO_Var [constructor, in DCOIOmega.geq]
geq_sig.IOk [inductive, in DCOIOmega.geq]
geq_sig.elookup [definition, in DCOIOmega.geq]
geq_sig.econtext [definition, in DCOIOmega.geq]
geq_sig [module, in DCOIOmega.geq]

I

iconv_dec.iconv_dec [lemma, in DCOIOmega.iconv_dec]
iconv_dec.iconvb_iconv [lemma, in DCOIOmega.iconv_dec]
iconv_dec.iconv_iconvb [lemma, in DCOIOmega.iconv_dec]
iconv_dec.iconvb [definition, in DCOIOmega.iconv_dec]
iconv_dec.nfacts [module, in DCOIOmega.iconv_dec]
iconv_dec.pfacts [module, in DCOIOmega.iconv_dec]
iconv_dec.cfacts [module, in DCOIOmega.iconv_dec]
iconv_dec [module, in DCOIOmega.iconv_dec]
iconv_dec [library]
id [definition, in DCOIOmega.Autosubst2.unscoped]
ids [projection, in DCOIOmega.Autosubst2.unscoped]
ids [constructor, in DCOIOmega.Autosubst2.unscoped]
idsRen [instance, in DCOIOmega.Autosubst2.unscoped]
imports [library]

L

Lattice [module, in DCOIOmega.Lattice.All]
LatticeWithBot [module, in DCOIOmega.iconv_dec]
LatticeWithBot.bot [axiom, in DCOIOmega.iconv_dec]
LatticeWithBot.bot_prop [axiom, in DCOIOmega.iconv_dec]
Lattice.join [axiom, in DCOIOmega.Lattice.All]
Lattice.join_idempotent [axiom, in DCOIOmega.Lattice.All]
Lattice.join_absorptive [axiom, in DCOIOmega.Lattice.All]
Lattice.join_associative [axiom, in DCOIOmega.Lattice.All]
Lattice.join_commutative [axiom, in DCOIOmega.Lattice.All]
Lattice.meet [axiom, in DCOIOmega.Lattice.All]
Lattice.meet_idempotent [axiom, in DCOIOmega.Lattice.All]
Lattice.meet_absorptive [axiom, in DCOIOmega.Lattice.All]
Lattice.meet_associative [axiom, in DCOIOmega.Lattice.All]
Lattice.meet_commutative [axiom, in DCOIOmega.Lattice.All]
Lattice.T [axiom, in DCOIOmega.Lattice.All]
Lattice.T_eqdec [axiom, in DCOIOmega.Lattice.All]
Lattice.T_eqb [axiom, in DCOIOmega.Lattice.All]
_ ⊆ _ (lattice_scope) [notation, in DCOIOmega.Lattice.All]
_ ∩ _ (lattice_scope) [notation, in DCOIOmega.Lattice.All]
_ ∪ _ (lattice_scope) [notation, in DCOIOmega.Lattice.All]
list_comp [definition, in DCOIOmega.Autosubst2.axioms]
list_id [definition, in DCOIOmega.Autosubst2.axioms]
list_ext [definition, in DCOIOmega.Autosubst2.axioms]
lr_sig.InterpUnivN_Nat [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_back_clos_star [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_back_clos [lemma, in DCOIOmega.semtyping]
lr_sig.InterpExt_back_clos [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Univ [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Univ_inv [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Sig_inv_nopf [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Fun_inv_nopf [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Conv [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_IEq [lemma, in DCOIOmega.semtyping]
lr_sig.InterpExt_IEq [lemma, in DCOIOmega.semtyping]
lr_sig.InterpExt_Sig_inv_nopf [lemma, in DCOIOmega.semtyping]
lr_sig.InterpExt_Fun_inv_nopf [lemma, in DCOIOmega.semtyping]
lr_sig.InterpExt_Ne_inv' [lemma, in DCOIOmega.semtyping]
lr_sig.adequacy [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_WNe [lemma, in DCOIOmega.semtyping]
lr_sig.InterpExt_adequacy [lemma, in DCOIOmega.semtyping]
lr_sig.wne_var [lemma, in DCOIOmega.semtyping]
lr_sig.CR [definition, in DCOIOmega.semtyping]
lr_sig.InterpUniv_Ok [lemma, in DCOIOmega.semtyping]
lr_sig.InterpExt_Ok [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_deterministic' [lemma, in DCOIOmega.semtyping]
lr_sig.InterpExt_deterministic' [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_deterministic [lemma, in DCOIOmega.semtyping]
lr_sig.InterpExt_deterministic [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Nat_inv [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Ne_inv [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Void_inv [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Eq [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Unit [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Unit_inv [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Void [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Eq_inv [lemma, in DCOIOmega.semtyping]
lr_sig.InterpExt_Eq_inv [lemma, in DCOIOmega.semtyping]
lr_sig.InterpExt_Void_inv [lemma, in DCOIOmega.semtyping]
lr_sig.InterpExt_Univ_inv [lemma, in DCOIOmega.semtyping]
lr_sig.InterpExt_Unit_inv [lemma, in DCOIOmega.semtyping]
lr_sig.InterpExt_Nat_inv [lemma, in DCOIOmega.semtyping]
lr_sig.InterpExt_Ne_inv [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_subsumption [lemma, in DCOIOmega.semtyping]
lr_sig.InterpExt_subsumption [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_back_preservation_star [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_preservation_star [lemma, in DCOIOmega.semtyping]
lr_sig.InterpExt_preservation_star [lemma, in DCOIOmega.semtyping]
lr_sig.InterpExt_back_preservation_star [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_preservation [lemma, in DCOIOmega.semtyping]
lr_sig.InterpExt_preservation [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_cumulative [lemma, in DCOIOmega.semtyping]
lr_sig.InterpExt_cumulative [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Sig_nopf [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Fun_nopf [lemma, in DCOIOmega.semtyping]
lr_sig.InterpExt_Fun_nopf [lemma, in DCOIOmega.semtyping]
lr_sig.InterpExt_Sig_inv [lemma, in DCOIOmega.semtyping]
lr_sig.InterpExt_Fun_inv [lemma, in DCOIOmega.semtyping]
lr_sig.InterpUnivN_nolt [lemma, in DCOIOmega.semtyping]
lr_sig.InterpExt_lt_redundant2 [lemma, in DCOIOmega.semtyping]
lr_sig.InterpExt_lt_redundant [lemma, in DCOIOmega.semtyping]
lr_sig.InterpExt_Univ' [lemma, in DCOIOmega.semtyping]
⟦ _ ⊨ _ ⟧ _ ↘ _ [notation, in DCOIOmega.semtyping]
lr_sig.InterpUnivN [definition, in DCOIOmega.semtyping]
lr_sig.InterpExt_Eq' [lemma, in DCOIOmega.semtyping]
⟦ _ ⊨ _ ⟧ _ ; _ ↘ _ [notation, in DCOIOmega.semtyping]
lr_sig.InterpExt_sind [definition, in DCOIOmega.semtyping]
lr_sig.InterpExt_ind [definition, in DCOIOmega.semtyping]
lr_sig.InterpExt_Unit [constructor, in DCOIOmega.semtyping]
lr_sig.InterpExt_Step [constructor, in DCOIOmega.semtyping]
lr_sig.InterpExt_Sig [constructor, in DCOIOmega.semtyping]
lr_sig.InterpExt_Eq [constructor, in DCOIOmega.semtyping]
lr_sig.InterpExt_Void [constructor, in DCOIOmega.semtyping]
lr_sig.InterpExt_Univ [constructor, in DCOIOmega.semtyping]
lr_sig.InterpExt_Fun [constructor, in DCOIOmega.semtyping]
lr_sig.InterpExt_Nat [constructor, in DCOIOmega.semtyping]
lr_sig.InterpExt_Ne [constructor, in DCOIOmega.semtyping]
lr_sig.InterpExt [inductive, in DCOIOmega.semtyping]
lr_sig.SumSpace [definition, in DCOIOmega.semtyping]
lr_sig.ProdSpace [definition, in DCOIOmega.semtyping]
lr_sig.nfacts [module, in DCOIOmega.semtyping]
lr_sig.cfacts [module, in DCOIOmega.semtyping]
lr_sig.pfacts [module, in DCOIOmega.semtyping]
lr_sig [module, in DCOIOmega.semtyping]

M

MkAll [module, in DCOIOmega.toplevel]
MkAll.admissible [module, in DCOIOmega.toplevel]
MkAll.consistency [module, in DCOIOmega.toplevel]
MkAll.conv [module, in DCOIOmega.toplevel]
MkAll.conv_dec [module, in DCOIOmega.toplevel]
MkAll.factorization [module, in DCOIOmega.toplevel]
MkAll.iconv_dec [module, in DCOIOmega.toplevel]
MkAll.ieq [module, in DCOIOmega.toplevel]
MkAll.lr [module, in DCOIOmega.toplevel]
MkAll.nf [module, in DCOIOmega.toplevel]
MkAll.par [module, in DCOIOmega.toplevel]
MkAll.preservation [module, in DCOIOmega.toplevel]
MkAll.soundness [module, in DCOIOmega.toplevel]
MkAll.syntax [module, in DCOIOmega.toplevel]
MkAll.typing [module, in DCOIOmega.toplevel]

N

nat_lattice_bot.bot_prop [lemma, in DCOIOmega.toplevel]
nat_lattice_bot.bot [definition, in DCOIOmega.toplevel]
nat_lattice_bot [module, in DCOIOmega.toplevel]
nat_lattice.T_eqdec [lemma, in DCOIOmega.toplevel]
nat_lattice.join_idempotent [lemma, in DCOIOmega.toplevel]
nat_lattice.join_absorptive [lemma, in DCOIOmega.toplevel]
nat_lattice.join_associative [lemma, in DCOIOmega.toplevel]
nat_lattice.join_commutative [lemma, in DCOIOmega.toplevel]
nat_lattice.meet_idempotent [lemma, in DCOIOmega.toplevel]
nat_lattice.meet_absorptive [lemma, in DCOIOmega.toplevel]
nat_lattice.meet_associative [lemma, in DCOIOmega.toplevel]
nat_lattice.meet_commutative [lemma, in DCOIOmega.toplevel]
nat_lattice.T_eqb [definition, in DCOIOmega.toplevel]
_ ∩ _ [notation, in DCOIOmega.toplevel]
_ ∪ _ [notation, in DCOIOmega.toplevel]
nat_lattice.join [definition, in DCOIOmega.toplevel]
nat_lattice.meet [definition, in DCOIOmega.toplevel]
nat_lattice.T [definition, in DCOIOmega.toplevel]
nat_lattice [module, in DCOIOmega.toplevel]
normalform [library]
normalform_fact.confluent_nf [lemma, in DCOIOmega.normalform]
normalform_fact.ext_wn [lemma, in DCOIOmega.normalform]
normalform_fact.wn_eq [lemma, in DCOIOmega.normalform]
normalform_fact.wn_pack [lemma, in DCOIOmega.normalform]
normalform_fact.wn_sig [lemma, in DCOIOmega.normalform]
normalform_fact.wn_pi [lemma, in DCOIOmega.normalform]
normalform_fact.wn_abs [lemma, in DCOIOmega.normalform]
normalform_fact.wne_let [lemma, in DCOIOmega.normalform]
normalform_fact.wne_seq [lemma, in DCOIOmega.normalform]
normalform_fact.wne_app [lemma, in DCOIOmega.normalform]
normalform_fact.wne_ind [lemma, in DCOIOmega.normalform]
normalform_fact.wne_j [lemma, in DCOIOmega.normalform]
normalform_fact.wne_absurd [lemma, in DCOIOmega.normalform]
normalform_fact.wn_antirenaming [lemma, in DCOIOmega.normalform]
normalform_fact.Pars_antirenaming [lemma, in DCOIOmega.normalform]
normalform_fact.Par_antirenaming [lemma, in DCOIOmega.normalform]
normalform_fact.ne_nf_renaming_with_d [lemma, in DCOIOmega.normalform]
normalform_fact.ren_with_d_imp [lemma, in DCOIOmega.normalform]
normalform_fact.ren_with_d_up_tm [lemma, in DCOIOmega.normalform]
normalform_fact.ren_with_d_ne [lemma, in DCOIOmega.normalform]
normalform_fact.var_or_d_ne [lemma, in DCOIOmega.normalform]
normalform_fact.ren_var_or_d [lemma, in DCOIOmega.normalform]
normalform_fact.ne_preservation [lemma, in DCOIOmega.normalform]
normalform_fact.nf_preservation [lemma, in DCOIOmega.normalform]
normalform_fact.nf_ne_preservation [lemma, in DCOIOmega.normalform]
normalform_fact.nf_refl_star [lemma, in DCOIOmega.normalform]
normalform_fact.nf_refl [lemma, in DCOIOmega.normalform]
normalform_fact.ne_nf_renaming [lemma, in DCOIOmega.normalform]
normalform_fact.ne_nat_val [lemma, in DCOIOmega.normalform]
normalform_fact.nat_val_nf [lemma, in DCOIOmega.normalform]
normalform_fact.nf_wn [lemma, in DCOIOmega.normalform]
normalform_fact.wne_wn [lemma, in DCOIOmega.normalform]
normalform_fact.ne_nf [lemma, in DCOIOmega.normalform]
normalform_fact.pf [module, in DCOIOmega.normalform]
normalform_fact [module, in DCOIOmega.normalform]
normalform_sig.ren_with_d [definition, in DCOIOmega.normalform]
normalform_sig.var_or_d [definition, in DCOIOmega.normalform]
normalform_sig.wne [definition, in DCOIOmega.normalform]
normalform_sig.wn [definition, in DCOIOmega.normalform]
normalform_sig.nf [definition, in DCOIOmega.normalform]
normalform_sig.ne [definition, in DCOIOmega.normalform]
normalform_sig [module, in DCOIOmega.normalform]

P

par [library]
par_facts.S_Ind [lemma, in DCOIOmega.par]
par_facts.P_SeqTT_star [lemma, in DCOIOmega.par]
par_facts.S_Seq [lemma, in DCOIOmega.par]
par_facts.S_Suc [lemma, in DCOIOmega.par]
par_facts.S_Eq [lemma, in DCOIOmega.par]
par_facts.S_Pack [lemma, in DCOIOmega.par]
par_facts.S_Absurd [lemma, in DCOIOmega.par]
par_facts.S_Abs [lemma, in DCOIOmega.par]
par_facts.S_Sig [lemma, in DCOIOmega.par]
par_facts.S_Pi [lemma, in DCOIOmega.par]
par_facts.S_Let [lemma, in DCOIOmega.par]
par_facts.S_J [lemma, in DCOIOmega.par]
par_facts.S_AppLR [lemma, in DCOIOmega.par]
par_facts.Pars_confluent [lemma, in DCOIOmega.par]
par_facts.Par_confluent [lemma, in DCOIOmega.par]
par_facts.Par_triangle [lemma, in DCOIOmega.par]
par_facts.P_LetPack_star [lemma, in DCOIOmega.par]
par_facts.P_JRefl_star [lemma, in DCOIOmega.par]
par_facts.P_IndSuc_star' [lemma, in DCOIOmega.par]
par_facts.P_IndSuc_star [lemma, in DCOIOmega.par]
par_facts.P_IndZero_star [lemma, in DCOIOmega.par]
par_facts.Pars_sig_inv [lemma, in DCOIOmega.par]
par_facts.Pars_univ_inv [lemma, in DCOIOmega.par]
par_facts.Pars_eq_inv [lemma, in DCOIOmega.par]
par_facts.Pars_pi_inv [lemma, in DCOIOmega.par]
par_facts.Coherent_cong_helper [lemma, in DCOIOmega.par]
par_facts.Pars_cong_star [lemma, in DCOIOmega.par]
par_facts.Par_cong2 [lemma, in DCOIOmega.par]
par_facts.Par_cong [lemma, in DCOIOmega.par]
par_facts.Par_subst_star [lemma, in DCOIOmega.par]
par_facts.Par_subst [lemma, in DCOIOmega.par]
par_facts.good_Pars_morphing_ext2 [lemma, in DCOIOmega.par]
par_facts.good_Pars_morphing_ext [lemma, in DCOIOmega.par]
par_facts.Pars_morphing_star [lemma, in DCOIOmega.par]
par_facts.Pars_morphing [lemma, in DCOIOmega.par]
par_facts.Par_morphing_star [lemma, in DCOIOmega.par]
par_facts.Par_morphing [lemma, in DCOIOmega.par]
par_facts.Coherent_m [definition, in DCOIOmega.par]
_ ⇒ς* _ [notation, in DCOIOmega.par]
_ ⇒ς _ [notation, in DCOIOmega.par]
par_facts.Par_m [definition, in DCOIOmega.par]
par_facts.Par_morphing_lift2 [lemma, in DCOIOmega.par]
par_facts.Par_morphing_lift [lemma, in DCOIOmega.par]
par_facts.Par_morphing_lift_n [lemma, in DCOIOmega.par]
par_facts.up_tm_tm_n [definition, in DCOIOmega.par]
par_facts.Pars_renaming [lemma, in DCOIOmega.par]
par_facts.Par_renaming [lemma, in DCOIOmega.par]
par_facts.P_LetPackCBN' [lemma, in DCOIOmega.par]
par_facts.P_LetPack' [lemma, in DCOIOmega.par]
par_facts.P_IndSuc' [lemma, in DCOIOmega.par]
par_facts.P_AppAbs' [lemma, in DCOIOmega.par]
par_facts.P_AppAbs_cbn [lemma, in DCOIOmega.par]
par_facts.Par_refl [lemma, in DCOIOmega.par]
par_facts [module, in DCOIOmega.par]
_ ⇒* _ [notation, in DCOIOmega.par]
_ ⇒ _ [notation, in DCOIOmega.par]
par_sig.Par_sind [definition, in DCOIOmega.par]
par_sig.Par_ind [definition, in DCOIOmega.par]
par_sig.P_Unit [constructor, in DCOIOmega.par]
par_sig.P_SeqTT [constructor, in DCOIOmega.par]
par_sig.P_Seq [constructor, in DCOIOmega.par]
par_sig.P_TT [constructor, in DCOIOmega.par]
par_sig.P_Nat [constructor, in DCOIOmega.par]
par_sig.P_IndSuc [constructor, in DCOIOmega.par]
par_sig.P_IndZero [constructor, in DCOIOmega.par]
par_sig.P_Ind [constructor, in DCOIOmega.par]
par_sig.P_Suc [constructor, in DCOIOmega.par]
par_sig.P_Zero [constructor, in DCOIOmega.par]
par_sig.P_LetPack [constructor, in DCOIOmega.par]
par_sig.P_Let [constructor, in DCOIOmega.par]
par_sig.P_Pack [constructor, in DCOIOmega.par]
par_sig.P_Sig [constructor, in DCOIOmega.par]
par_sig.P_JRefl [constructor, in DCOIOmega.par]
par_sig.P_J [constructor, in DCOIOmega.par]
par_sig.P_Eq [constructor, in DCOIOmega.par]
par_sig.P_Refl [constructor, in DCOIOmega.par]
par_sig.P_Absurd [constructor, in DCOIOmega.par]
par_sig.P_Void [constructor, in DCOIOmega.par]
par_sig.P_AppAbs [constructor, in DCOIOmega.par]
par_sig.P_App [constructor, in DCOIOmega.par]
par_sig.P_Abs [constructor, in DCOIOmega.par]
par_sig.P_Pi [constructor, in DCOIOmega.par]
par_sig.P_Univ [constructor, in DCOIOmega.par]
par_sig.P_Var [constructor, in DCOIOmega.par]
par_sig.Par [inductive, in DCOIOmega.par]
par_sig [module, in DCOIOmega.par]
preservation [module, in DCOIOmega.preservation]
preservation [library]
preservation.good_morphing_iok_subst_ok [lemma, in DCOIOmega.preservation]
preservation.good_morphing_up [lemma, in DCOIOmega.preservation]
preservation.good_morphing_cons [lemma, in DCOIOmega.preservation]
preservation.good_morphing_nil [lemma, in DCOIOmega.preservation]
preservation.good_morphing_suc [lemma, in DCOIOmega.preservation]
preservation.good_renaming_suc [lemma, in DCOIOmega.preservation]
preservation.good_renaming_up [lemma, in DCOIOmega.preservation]
preservation.here' [lemma, in DCOIOmega.preservation]
preservation.ifacts [module, in DCOIOmega.preservation]
preservation.lookup_deter [lemma, in DCOIOmega.preservation]
preservation.lookup_good_morphing [definition, in DCOIOmega.preservation]
preservation.morphing_Syn_Univ [lemma, in DCOIOmega.preservation]
preservation.morphing_Syn [lemma, in DCOIOmega.preservation]
preservation.preservation_helper2 [lemma, in DCOIOmega.preservation]
preservation.preservation_helper [lemma, in DCOIOmega.preservation]
preservation.renaming_Syn_Univ [lemma, in DCOIOmega.preservation]
preservation.renaming_Syn [lemma, in DCOIOmega.preservation]
preservation.renaming_Syn_helper [lemma, in DCOIOmega.preservation]
preservation.solver [module, in DCOIOmega.preservation]
preservation.subject_reduction_star [lemma, in DCOIOmega.preservation]
preservation.subject_reduction [lemma, in DCOIOmega.preservation]
preservation.subst_Syn_Univ [lemma, in DCOIOmega.preservation]
preservation.subst_Syn [lemma, in DCOIOmega.preservation]
preservation.subsumption [lemma, in DCOIOmega.preservation]
preservation.tcfacts [module, in DCOIOmega.preservation]
preservation.there' [lemma, in DCOIOmega.preservation]
preservation.T_Par [lemma, in DCOIOmega.preservation]
preservation.T_Let_simpl' [lemma, in DCOIOmega.preservation]
preservation.T_Let_simpl [lemma, in DCOIOmega.preservation]
preservation.T_Refl' [lemma, in DCOIOmega.preservation]
preservation.T_Abs_simpl [lemma, in DCOIOmega.preservation]
preservation.T_J_simpl [lemma, in DCOIOmega.preservation]
preservation.T_Var_inv [lemma, in DCOIOmega.preservation]
preservation.T_Eq_simpl [lemma, in DCOIOmega.preservation]
preservation.T_Let' [lemma, in DCOIOmega.preservation]
preservation.T_Pack' [lemma, in DCOIOmega.preservation]
preservation.T_J' [lemma, in DCOIOmega.preservation]
preservation.T_Seq' [lemma, in DCOIOmega.preservation]
preservation.T_App' [lemma, in DCOIOmega.preservation]
preservation.T_Ind' [lemma, in DCOIOmega.preservation]
preservation.weakening_Syn_Univ [lemma, in DCOIOmega.preservation]
preservation.weakening_Syn' [lemma, in DCOIOmega.preservation]
preservation.weakening_Syn [lemma, in DCOIOmega.preservation]
preservation.Wff_lookup [lemma, in DCOIOmega.preservation]
preservation.Wt_J_inv [lemma, in DCOIOmega.preservation]
preservation.Wt_Seq_inv [lemma, in DCOIOmega.preservation]
preservation.Wt_TT_inv [lemma, in DCOIOmega.preservation]
preservation.Wt_Absurd_inv [lemma, in DCOIOmega.preservation]
preservation.Wt_Refl_Coherent [lemma, in DCOIOmega.preservation]
preservation.Wt_Suc_inv [lemma, in DCOIOmega.preservation]
preservation.Wt_Refl_inv [lemma, in DCOIOmega.preservation]
preservation.Wt_Let_inv [lemma, in DCOIOmega.preservation]
preservation.Wt_Eq_inv [lemma, in DCOIOmega.preservation]
preservation.Wt_Ind_inv [lemma, in DCOIOmega.preservation]
preservation.Wt_App_inv [lemma, in DCOIOmega.preservation]
preservation.Wt_regularity [lemma, in DCOIOmega.preservation]
preservation.Wt_Pack_inv [lemma, in DCOIOmega.preservation]
preservation.Wt_Sig_Univ_inv [lemma, in DCOIOmega.preservation]
preservation.Wt_Abs_inv [lemma, in DCOIOmega.preservation]
preservation.Wt_Pi_Univ_inv [lemma, in DCOIOmega.preservation]
preservation.Wt_Sig_inv [lemma, in DCOIOmega.preservation]
preservation.Wt_Pi_inv [lemma, in DCOIOmega.preservation]
preservation.Wt_Univ [lemma, in DCOIOmega.preservation]
preservation.Wt_Wff [lemma, in DCOIOmega.preservation]
prod_comp [definition, in DCOIOmega.Autosubst2.axioms]
prod_ext [definition, in DCOIOmega.Autosubst2.axioms]
prod_id [definition, in DCOIOmega.Autosubst2.axioms]
prod_map [definition, in DCOIOmega.Autosubst2.axioms]
Properties [module, in DCOIOmega.Lattice.All]
Properties.sub_eqdec [lemma, in DCOIOmega.Lattice.All]

R

ren1 [projection, in DCOIOmega.Autosubst2.unscoped]
Ren1 [record, in DCOIOmega.Autosubst2.unscoped]
ren1 [constructor, in DCOIOmega.Autosubst2.unscoped]
Ren1 [inductive, in DCOIOmega.Autosubst2.unscoped]
ren2 [projection, in DCOIOmega.Autosubst2.unscoped]
Ren2 [record, in DCOIOmega.Autosubst2.unscoped]
ren2 [constructor, in DCOIOmega.Autosubst2.unscoped]
Ren2 [inductive, in DCOIOmega.Autosubst2.unscoped]
ren3 [projection, in DCOIOmega.Autosubst2.unscoped]
Ren3 [record, in DCOIOmega.Autosubst2.unscoped]
ren3 [constructor, in DCOIOmega.Autosubst2.unscoped]
Ren3 [inductive, in DCOIOmega.Autosubst2.unscoped]
ren4 [projection, in DCOIOmega.Autosubst2.unscoped]
Ren4 [record, in DCOIOmega.Autosubst2.unscoped]
ren4 [constructor, in DCOIOmega.Autosubst2.unscoped]
Ren4 [inductive, in DCOIOmega.Autosubst2.unscoped]
ren5 [projection, in DCOIOmega.Autosubst2.unscoped]
Ren5 [record, in DCOIOmega.Autosubst2.unscoped]
ren5 [constructor, in DCOIOmega.Autosubst2.unscoped]
Ren5 [inductive, in DCOIOmega.Autosubst2.unscoped]

S

scons [definition, in DCOIOmega.Autosubst2.unscoped]
scons_comp [lemma, in DCOIOmega.Autosubst2.unscoped]
scons_eta [lemma, in DCOIOmega.Autosubst2.unscoped]
scons_eta_id [lemma, in DCOIOmega.Autosubst2.unscoped]
semtyping [library]
shift [abbreviation, in DCOIOmega.Autosubst2.unscoped]
Solver [module, in DCOIOmega.Lattice.All]
Solver.denoteLexp [definition, in DCOIOmega.Lattice.All]
Solver.Join [constructor, in DCOIOmega.Lattice.All]
Solver.leq_meet_prime [lemma, in DCOIOmega.Lattice.All]
Solver.leq_join_prime [lemma, in DCOIOmega.Lattice.All]
Solver.leq_join_iff [lemma, in DCOIOmega.Lattice.All]
Solver.leq_meet_iff [lemma, in DCOIOmega.Lattice.All]
Solver.leq_trans [lemma, in DCOIOmega.Lattice.All]
Solver.leq_join [lemma, in DCOIOmega.Lattice.All]
Solver.leq_lat_leq_lat'_iff [lemma, in DCOIOmega.Lattice.All]
Solver.lexp [inductive, in DCOIOmega.Lattice.All]
Solver.lexp_size [definition, in DCOIOmega.Lattice.All]
Solver.lexp_sind [definition, in DCOIOmega.Lattice.All]
Solver.lexp_rec [definition, in DCOIOmega.Lattice.All]
Solver.lexp_ind [definition, in DCOIOmega.Lattice.All]
Solver.lexp_rect [definition, in DCOIOmega.Lattice.All]
Solver.Meet [constructor, in DCOIOmega.Lattice.All]
Solver.meet_leq [lemma, in DCOIOmega.Lattice.All]
Solver.splitLeq [definition, in DCOIOmega.Lattice.All]
Solver.splitLeqForward [definition, in DCOIOmega.Lattice.All]
Solver.splitLeqForward_complete [lemma, in DCOIOmega.Lattice.All]
Solver.splitLeq_iff [lemma, in DCOIOmega.Lattice.All]
Solver.splitLeq_complete [lemma, in DCOIOmega.Lattice.All]
Solver.splitLeq_sound [lemma, in DCOIOmega.Lattice.All]
Solver.Var [constructor, in DCOIOmega.Lattice.All]
soundness [module, in DCOIOmega.soundness]
soundness [library]
soundness.iok_ρ_ok_morphing [lemma, in DCOIOmega.soundness]
soundness.lfacts [module, in DCOIOmega.soundness]
soundness.normalization [lemma, in DCOIOmega.soundness]
soundness.pfacts [module, in DCOIOmega.soundness]
soundness.renaming_SemWt [lemma, in DCOIOmega.soundness]
soundness.SemWff [inductive, in DCOIOmega.soundness]
soundness.SemWff_lookup [lemma, in DCOIOmega.soundness]
soundness.SemWff_sind [definition, in DCOIOmega.soundness]
soundness.SemWff_ind [definition, in DCOIOmega.soundness]
soundness.SemWff_cons [constructor, in DCOIOmega.soundness]
soundness.SemWff_nil [constructor, in DCOIOmega.soundness]
soundness.SemWt [definition, in DCOIOmega.soundness]
soundness.SemWt_Univ [lemma, in DCOIOmega.soundness]
soundness.solver [module, in DCOIOmega.soundness]
soundness.soundness [lemma, in DCOIOmega.soundness]
soundness.tcfacts [module, in DCOIOmega.soundness]
soundness.weakening_Sem [lemma, in DCOIOmega.soundness]
soundness.wt_ρ_ok_morphing_iok [lemma, in DCOIOmega.soundness]
soundness.ρ_ok_renaming [lemma, in DCOIOmega.soundness]
soundness.ρ_ok_cons [lemma, in DCOIOmega.soundness]
soundness.ρ_ok_id [lemma, in DCOIOmega.soundness]
soundness.ρ_ok_iok [lemma, in DCOIOmega.soundness]
soundness.ρ_ok [definition, in DCOIOmega.soundness]
subst1 [projection, in DCOIOmega.Autosubst2.unscoped]
Subst1 [record, in DCOIOmega.Autosubst2.unscoped]
subst1 [constructor, in DCOIOmega.Autosubst2.unscoped]
Subst1 [inductive, in DCOIOmega.Autosubst2.unscoped]
subst2 [projection, in DCOIOmega.Autosubst2.unscoped]
Subst2 [record, in DCOIOmega.Autosubst2.unscoped]
subst2 [constructor, in DCOIOmega.Autosubst2.unscoped]
Subst2 [inductive, in DCOIOmega.Autosubst2.unscoped]
subst3 [projection, in DCOIOmega.Autosubst2.unscoped]
Subst3 [record, in DCOIOmega.Autosubst2.unscoped]
subst3 [constructor, in DCOIOmega.Autosubst2.unscoped]
Subst3 [inductive, in DCOIOmega.Autosubst2.unscoped]
subst4 [projection, in DCOIOmega.Autosubst2.unscoped]
Subst4 [record, in DCOIOmega.Autosubst2.unscoped]
subst4 [constructor, in DCOIOmega.Autosubst2.unscoped]
Subst4 [inductive, in DCOIOmega.Autosubst2.unscoped]
subst5 [projection, in DCOIOmega.Autosubst2.unscoped]
Subst5 [record, in DCOIOmega.Autosubst2.unscoped]
subst5 [constructor, in DCOIOmega.Autosubst2.unscoped]
Subst5 [inductive, in DCOIOmega.Autosubst2.unscoped]
syntax [library]
_ ⟨ _ ⟩ (subst_scope) [notation, in DCOIOmega.Autosubst2.syntax]
_ [ _ ] (subst_scope) [notation, in DCOIOmega.Autosubst2.syntax]
⟨ _ ⟩ (fscope) [notation, in DCOIOmega.Autosubst2.syntax]
_ ⟨ _ ⟩ (subst_scope) [notation, in DCOIOmega.Autosubst2.syntax]
[ _ ] (fscope) [notation, in DCOIOmega.Autosubst2.syntax]
_ [ _ ] (subst_scope) [notation, in DCOIOmega.Autosubst2.syntax]
syntax_sig.Up_tm_tm [instance, in DCOIOmega.Autosubst2.syntax]
↑__tm (subst_scope) [notation, in DCOIOmega.Autosubst2.syntax]
↑__tm (subst_scope) [notation, in DCOIOmega.Autosubst2.syntax]
syntax_sig.up_tm [projection, in DCOIOmega.Autosubst2.syntax]
syntax_sig.Up_tm [record, in DCOIOmega.Autosubst2.syntax]
syntax_sig.up_tm [constructor, in DCOIOmega.Autosubst2.syntax]
syntax_sig.Up_tm [inductive, in DCOIOmega.Autosubst2.syntax]
var (subst_scope) [notation, in DCOIOmega.Autosubst2.syntax]
_ __tm (subst_scope) [notation, in DCOIOmega.Autosubst2.syntax]
_ __tm (subst_scope) [notation, in DCOIOmega.Autosubst2.syntax]
syntax_sig.VarInstance_tm [instance, in DCOIOmega.Autosubst2.syntax]
syntax_sig.Ren_tm [instance, in DCOIOmega.Autosubst2.syntax]
syntax_sig.Subst_tm [instance, in DCOIOmega.Autosubst2.syntax]
syntax_sig.renRen'_tm [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.renRen_tm [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.renComp'_tm [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.renComp_tm [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.compRen'_tm [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.compRen_tm [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.compComp'_tm [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.compComp_tm [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.varLRen_tm [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.varL_tm [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.rinstId_tm [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.instId_tm [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.rinstInst_tm [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.rinst_inst_tm [definition, in DCOIOmega.Autosubst2.syntax]
syntax_sig.rinstInst_up_tm_tm [definition, in DCOIOmega.Autosubst2.syntax]
syntax_sig.compSubstSubst_tm [definition, in DCOIOmega.Autosubst2.syntax]
syntax_sig.up_subst_subst_tm_tm [definition, in DCOIOmega.Autosubst2.syntax]
syntax_sig.compSubstRen_tm [definition, in DCOIOmega.Autosubst2.syntax]
syntax_sig.up_subst_ren_tm_tm [definition, in DCOIOmega.Autosubst2.syntax]
syntax_sig.compRenSubst_tm [definition, in DCOIOmega.Autosubst2.syntax]
syntax_sig.up_ren_subst_tm_tm [definition, in DCOIOmega.Autosubst2.syntax]
syntax_sig.compRenRen_tm [definition, in DCOIOmega.Autosubst2.syntax]
syntax_sig.up_ren_ren_tm_tm [definition, in DCOIOmega.Autosubst2.syntax]
syntax_sig.ext_tm [definition, in DCOIOmega.Autosubst2.syntax]
syntax_sig.upExt_tm_tm [definition, in DCOIOmega.Autosubst2.syntax]
syntax_sig.extRen_tm [definition, in DCOIOmega.Autosubst2.syntax]
syntax_sig.upExtRen_tm_tm [definition, in DCOIOmega.Autosubst2.syntax]
syntax_sig.idSubst_tm [definition, in DCOIOmega.Autosubst2.syntax]
syntax_sig.upId_tm_tm [definition, in DCOIOmega.Autosubst2.syntax]
syntax_sig.subst_tm [definition, in DCOIOmega.Autosubst2.syntax]
syntax_sig.up_tm_tm [definition, in DCOIOmega.Autosubst2.syntax]
syntax_sig.ren_tm [definition, in DCOIOmega.Autosubst2.syntax]
syntax_sig.upRen_tm_tm [definition, in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tUnit [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tSeq [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tTT [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tNat [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tInd [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tSuc [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tZero [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tLet [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tPack [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tSig [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tRefl [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tJ [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tEq [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tAbsurd [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tVoid [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tUniv [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tPi [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tApp [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tAbs [lemma, in DCOIOmega.Autosubst2.syntax]
syntax_sig.tm_sind [definition, in DCOIOmega.Autosubst2.syntax]
syntax_sig.tm_rec [definition, in DCOIOmega.Autosubst2.syntax]
syntax_sig.tm_ind [definition, in DCOIOmega.Autosubst2.syntax]
syntax_sig.tm_rect [definition, in DCOIOmega.Autosubst2.syntax]
syntax_sig.tUnit [constructor, in DCOIOmega.Autosubst2.syntax]
syntax_sig.tSeq [constructor, in DCOIOmega.Autosubst2.syntax]
syntax_sig.tTT [constructor, in DCOIOmega.Autosubst2.syntax]
syntax_sig.tNat [constructor, in DCOIOmega.Autosubst2.syntax]
syntax_sig.tInd [constructor, in DCOIOmega.Autosubst2.syntax]
syntax_sig.tSuc [constructor, in DCOIOmega.Autosubst2.syntax]
syntax_sig.tZero [constructor, in DCOIOmega.Autosubst2.syntax]
syntax_sig.tLet [constructor, in DCOIOmega.Autosubst2.syntax]
syntax_sig.tPack [constructor, in DCOIOmega.Autosubst2.syntax]
syntax_sig.tSig [constructor, in DCOIOmega.Autosubst2.syntax]
syntax_sig.tRefl [constructor, in DCOIOmega.Autosubst2.syntax]
syntax_sig.tJ [constructor, in DCOIOmega.Autosubst2.syntax]
syntax_sig.tEq [constructor, in DCOIOmega.Autosubst2.syntax]
syntax_sig.tAbsurd [constructor, in DCOIOmega.Autosubst2.syntax]
syntax_sig.tVoid [constructor, in DCOIOmega.Autosubst2.syntax]
syntax_sig.tUniv [constructor, in DCOIOmega.Autosubst2.syntax]
syntax_sig.tPi [constructor, in DCOIOmega.Autosubst2.syntax]
syntax_sig.tApp [constructor, in DCOIOmega.Autosubst2.syntax]
syntax_sig.tAbs [constructor, in DCOIOmega.Autosubst2.syntax]
syntax_sig.var_tm [constructor, in DCOIOmega.Autosubst2.syntax]
syntax_sig.tm [inductive, in DCOIOmega.Autosubst2.syntax]
syntax_sig.tm [section, in DCOIOmega.Autosubst2.syntax]
syntax_sig [module, in DCOIOmega.Autosubst2.syntax]

T

toplevel [library]
typing [library]
typing_conv_facts.lookup_good_renaming_iok_subst_ok [lemma, in DCOIOmega.typing_conv]
typing_conv_facts.typing_conv [lemma, in DCOIOmega.typing_conv]
typing_conv_facts.Wt_IOk_Downgrade [lemma, in DCOIOmega.typing_conv]
typing_conv_facts.typing_iok [lemma, in DCOIOmega.typing_conv]
typing_conv_facts.elookup_lookup [lemma, in DCOIOmega.typing_conv]
typing_conv_facts.lookup_elookup [lemma, in DCOIOmega.typing_conv]
typing_conv_facts.cfacts [module, in DCOIOmega.typing_conv]
typing_conv_facts.lfacts [module, in DCOIOmega.typing_conv]
typing_conv_facts.ifacts [module, in DCOIOmega.typing_conv]
typing_conv_facts.pfacts [module, in DCOIOmega.typing_conv]
typing_conv_facts.solver [module, in DCOIOmega.typing_conv]
typing_conv_facts [module, in DCOIOmega.typing_conv]
typing_sig.wff_ind [definition, in DCOIOmega.typing]
typing_sig.wt_ind [definition, in DCOIOmega.typing]
⊢ _ [notation, in DCOIOmega.typing]
_ ⊢ _ ; _ ∈ _ [notation, in DCOIOmega.typing]
typing_sig.Wff_sind [definition, in DCOIOmega.typing]
typing_sig.Wff_ind [definition, in DCOIOmega.typing]
typing_sig.Wt_sind [definition, in DCOIOmega.typing]
typing_sig.Wt_ind [definition, in DCOIOmega.typing]
typing_sig.Wff_cons [constructor, in DCOIOmega.typing]
typing_sig.Wff_nil [constructor, in DCOIOmega.typing]
typing_sig.Wff [inductive, in DCOIOmega.typing]
typing_sig.T_Seq [constructor, in DCOIOmega.typing]
typing_sig.T_Unit [constructor, in DCOIOmega.typing]
typing_sig.T_TT [constructor, in DCOIOmega.typing]
typing_sig.T_Let [constructor, in DCOIOmega.typing]
typing_sig.T_Pack [constructor, in DCOIOmega.typing]
typing_sig.T_Sig [constructor, in DCOIOmega.typing]
typing_sig.T_J [constructor, in DCOIOmega.typing]
typing_sig.T_Eq [constructor, in DCOIOmega.typing]
typing_sig.T_Refl [constructor, in DCOIOmega.typing]
typing_sig.T_Absurd [constructor, in DCOIOmega.typing]
typing_sig.T_Void [constructor, in DCOIOmega.typing]
typing_sig.T_Univ [constructor, in DCOIOmega.typing]
typing_sig.T_Nat [constructor, in DCOIOmega.typing]
typing_sig.T_Ind [constructor, in DCOIOmega.typing]
typing_sig.T_Suc [constructor, in DCOIOmega.typing]
typing_sig.T_Zero [constructor, in DCOIOmega.typing]
typing_sig.T_Conv [constructor, in DCOIOmega.typing]
typing_sig.T_App [constructor, in DCOIOmega.typing]
typing_sig.T_Abs [constructor, in DCOIOmega.typing]
typing_sig.T_Pi [constructor, in DCOIOmega.typing]
typing_sig.T_Var [constructor, in DCOIOmega.typing]
typing_sig.Wt [inductive, in DCOIOmega.typing]
typing_sig.c2e [definition, in DCOIOmega.typing]
typing_sig.lookup_good_renaming [definition, in DCOIOmega.typing]
typing_sig.lookup_sind [definition, in DCOIOmega.typing]
typing_sig.lookup_ind [definition, in DCOIOmega.typing]
typing_sig.there [constructor, in DCOIOmega.typing]
typing_sig.here [constructor, in DCOIOmega.typing]
typing_sig.lookup [inductive, in DCOIOmega.typing]
typing_sig.context [definition, in DCOIOmega.typing]
typing_sig [module, in DCOIOmega.typing]
typing_conv [library]

U

unscoped [library]
up_ren_ren [lemma, in DCOIOmega.Autosubst2.unscoped]
up_ren [definition, in DCOIOmega.Autosubst2.unscoped]

V

Var [record, in DCOIOmega.Autosubst2.unscoped]
Var [inductive, in DCOIOmega.Autosubst2.unscoped]
var_zero [definition, in DCOIOmega.Autosubst2.unscoped]

other

⟨ _ ; _ ⟩ (fscope) [notation, in DCOIOmega.Autosubst2.unscoped]
⟨ _ ⟩ (fscope) [notation, in DCOIOmega.Autosubst2.unscoped]
_ .. (subst_scope) [notation, in DCOIOmega.Autosubst2.unscoped]
_ >> _ (subst_scope) [notation, in DCOIOmega.Autosubst2.unscoped]
_ [ _ ; _ ] (subst_scope) [notation, in DCOIOmega.Autosubst2.unscoped]
_ [ _ ] (subst_scope) [notation, in DCOIOmega.Autosubst2.unscoped]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in DCOIOmega.Autosubst2.unscoped]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in DCOIOmega.Autosubst2.unscoped]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [notation, in DCOIOmega.Autosubst2.unscoped]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in DCOIOmega.Autosubst2.unscoped]
_ ⟨ _ ⟩ (subst_scope) [notation, in DCOIOmega.Autosubst2.unscoped]
_ .: _ [notation, in DCOIOmega.Autosubst2.unscoped]
list_map [notation, in DCOIOmega.Autosubst2.axioms]
↑ [notation, in DCOIOmega.Autosubst2.unscoped]

---

Notation Index

L

_ ⊆ _ (lattice_scope) [in DCOIOmega.Lattice.All]
_ ∩ _ (lattice_scope) [in DCOIOmega.Lattice.All]
_ ∪ _ (lattice_scope) [in DCOIOmega.Lattice.All]
⟦ _ ⊨ _ ⟧ _ ↘ _ [in DCOIOmega.semtyping]
⟦ _ ⊨ _ ⟧ _ ; _ ↘ _ [in DCOIOmega.semtyping]

N

_ ∩ _ [in DCOIOmega.toplevel]
_ ∪ _ [in DCOIOmega.toplevel]

P

_ ⇒ς* _ [in DCOIOmega.par]
_ ⇒ς _ [in DCOIOmega.par]
_ ⇒* _ [in DCOIOmega.par]
_ ⇒ _ [in DCOIOmega.par]

S

_ ⟨ _ ⟩ (subst_scope) [in DCOIOmega.Autosubst2.syntax]
_ [ _ ] (subst_scope) [in DCOIOmega.Autosubst2.syntax]
⟨ _ ⟩ (fscope) [in DCOIOmega.Autosubst2.syntax]
_ ⟨ _ ⟩ (subst_scope) [in DCOIOmega.Autosubst2.syntax]
[ _ ] (fscope) [in DCOIOmega.Autosubst2.syntax]
_ [ _ ] (subst_scope) [in DCOIOmega.Autosubst2.syntax]
↑__tm (subst_scope) [in DCOIOmega.Autosubst2.syntax]
↑__tm (subst_scope) [in DCOIOmega.Autosubst2.syntax]
var (subst_scope) [in DCOIOmega.Autosubst2.syntax]
_ __tm (subst_scope) [in DCOIOmega.Autosubst2.syntax]
_ __tm (subst_scope) [in DCOIOmega.Autosubst2.syntax]

T

⊢ _ [in DCOIOmega.typing]
_ ⊢ _ ; _ ∈ _ [in DCOIOmega.typing]

other

⟨ _ ; _ ⟩ (fscope) [in DCOIOmega.Autosubst2.unscoped]
⟨ _ ⟩ (fscope) [in DCOIOmega.Autosubst2.unscoped]
_ .. (subst_scope) [in DCOIOmega.Autosubst2.unscoped]
_ >> _ (subst_scope) [in DCOIOmega.Autosubst2.unscoped]
_ [ _ ; _ ] (subst_scope) [in DCOIOmega.Autosubst2.unscoped]
_ [ _ ] (subst_scope) [in DCOIOmega.Autosubst2.unscoped]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [in DCOIOmega.Autosubst2.unscoped]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [in DCOIOmega.Autosubst2.unscoped]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [in DCOIOmega.Autosubst2.unscoped]
_ ⟨ _ ; _ ⟩ (subst_scope) [in DCOIOmega.Autosubst2.unscoped]
_ ⟨ _ ⟩ (subst_scope) [in DCOIOmega.Autosubst2.unscoped]
_ .: _ [in DCOIOmega.Autosubst2.unscoped]
list_map [in DCOIOmega.Autosubst2.axioms]
↑ [in DCOIOmega.Autosubst2.unscoped]

---

Module Index

A

admissible [in DCOIOmega.admissible]
admissible.cfacts [in DCOIOmega.admissible]
admissible.ifacts [in DCOIOmega.admissible]
admissible.preservation [in DCOIOmega.admissible]
admissible.solver [in DCOIOmega.admissible]
admissible.tcfacts [in DCOIOmega.admissible]

C

consistency [in DCOIOmega.consistency]
consistency.preservation [in DCOIOmega.consistency]
consistency.soundness [in DCOIOmega.consistency]
conv_facts.ifacts [in DCOIOmega.conv]
conv_facts.pfacts [in DCOIOmega.conv]
conv_facts [in DCOIOmega.conv]
conv_sig [in DCOIOmega.conv]
conv_dec_bot.ifacts [in DCOIOmega.iconv_dec]
conv_dec_bot.preservation [in DCOIOmega.iconv_dec]
conv_dec_bot.Solver [in DCOIOmega.iconv_dec]
conv_dec_bot.soundness [in DCOIOmega.iconv_dec]
conv_dec_bot [in DCOIOmega.iconv_dec]

D

dcoi_with_nat_lattice [in DCOIOmega.toplevel]

F

factorization_sig.nfact [in DCOIOmega.factorization]
factorization_sig.pfacts [in DCOIOmega.factorization]
factorization_sig [in DCOIOmega.factorization]

G

geq_facts.solver [in DCOIOmega.geq]
geq_facts.lprop [in DCOIOmega.geq]
geq_facts [in DCOIOmega.geq]
geq_sig [in DCOIOmega.geq]

I

iconv_dec.nfacts [in DCOIOmega.iconv_dec]
iconv_dec.pfacts [in DCOIOmega.iconv_dec]
iconv_dec.cfacts [in DCOIOmega.iconv_dec]
iconv_dec [in DCOIOmega.iconv_dec]

L

Lattice [in DCOIOmega.Lattice.All]
LatticeWithBot [in DCOIOmega.iconv_dec]
lr_sig.nfacts [in DCOIOmega.semtyping]
lr_sig.cfacts [in DCOIOmega.semtyping]
lr_sig.pfacts [in DCOIOmega.semtyping]
lr_sig [in DCOIOmega.semtyping]

M

MkAll [in DCOIOmega.toplevel]
MkAll.admissible [in DCOIOmega.toplevel]
MkAll.consistency [in DCOIOmega.toplevel]
MkAll.conv [in DCOIOmega.toplevel]
MkAll.conv_dec [in DCOIOmega.toplevel]
MkAll.factorization [in DCOIOmega.toplevel]
MkAll.iconv_dec [in DCOIOmega.toplevel]
MkAll.ieq [in DCOIOmega.toplevel]
MkAll.lr [in DCOIOmega.toplevel]
MkAll.nf [in DCOIOmega.toplevel]
MkAll.par [in DCOIOmega.toplevel]
MkAll.preservation [in DCOIOmega.toplevel]
MkAll.soundness [in DCOIOmega.toplevel]
MkAll.syntax [in DCOIOmega.toplevel]
MkAll.typing [in DCOIOmega.toplevel]

N

nat_lattice_bot [in DCOIOmega.toplevel]
nat_lattice [in DCOIOmega.toplevel]
normalform_fact.pf [in DCOIOmega.normalform]
normalform_fact [in DCOIOmega.normalform]
normalform_sig [in DCOIOmega.normalform]

P

par_facts [in DCOIOmega.par]
par_sig [in DCOIOmega.par]
preservation [in DCOIOmega.preservation]
preservation.ifacts [in DCOIOmega.preservation]
preservation.solver [in DCOIOmega.preservation]
preservation.tcfacts [in DCOIOmega.preservation]
Properties [in DCOIOmega.Lattice.All]

S

Solver [in DCOIOmega.Lattice.All]
soundness [in DCOIOmega.soundness]
soundness.lfacts [in DCOIOmega.soundness]
soundness.pfacts [in DCOIOmega.soundness]
soundness.solver [in DCOIOmega.soundness]
soundness.tcfacts [in DCOIOmega.soundness]
syntax_sig [in DCOIOmega.Autosubst2.syntax]

T

typing_conv_facts.cfacts [in DCOIOmega.typing_conv]
typing_conv_facts.lfacts [in DCOIOmega.typing_conv]
typing_conv_facts.ifacts [in DCOIOmega.typing_conv]
typing_conv_facts.pfacts [in DCOIOmega.typing_conv]
typing_conv_facts.solver [in DCOIOmega.typing_conv]
typing_conv_facts [in DCOIOmega.typing_conv]
typing_sig [in DCOIOmega.typing]

---

Library Index

A

admissible
All
axioms

C

consistency
conv

F

factorization

G

geq

I

iconv_dec
imports

N

normalform

P

par
preservation

S

semtyping
soundness
syntax

T

toplevel
typing
typing_conv

U

unscoped

---

Lemma Index

A

admissible.T_Proj2_Alt [in DCOIOmega.admissible]
admissible.T_Proj2 [in DCOIOmega.admissible]
admissible.T_Proj2_leq [in DCOIOmega.admissible]
admissible.T_Proj1 [in DCOIOmega.admissible]
admissible.T_Unbox [in DCOIOmega.admissible]
admissible.T_Box [in DCOIOmega.admissible]
admissible.T_T [in DCOIOmega.admissible]
admissible.T_Down_Alt [in DCOIOmega.admissible]

C

consistency.consistency [in DCOIOmega.consistency]
consistency.ne_contra [in DCOIOmega.consistency]
conv_facts.conv_par_star2 [in DCOIOmega.conv]
conv_facts.iconv_par_star2 [in DCOIOmega.conv]
conv_facts.iconv_par_star [in DCOIOmega.conv]
conv_facts.iconv_conv [in DCOIOmega.conv]
conv_facts.conv_renaming [in DCOIOmega.conv]
conv_facts.iconv_renaming [in DCOIOmega.conv]
conv_facts.iconv_iok_downgrade [in DCOIOmega.conv]
conv_facts.conv_eq_inj [in DCOIOmega.conv]
conv_facts.conv_sig_inj [in DCOIOmega.conv]
conv_facts.conv_pi_inj [in DCOIOmega.conv]
conv_facts.iconv_sig_inj [in DCOIOmega.conv]
conv_facts.iconv_pi_inj [in DCOIOmega.conv]
conv_facts.conv_univ_inj [in DCOIOmega.conv]
conv_facts.ieq_conv [in DCOIOmega.conv]
conv_facts.conv_subst [in DCOIOmega.conv]
conv_facts.iconv_subst [in DCOIOmega.conv]
conv_facts.conv_trans [in DCOIOmega.conv]
conv_facts.iconv_trans [in DCOIOmega.conv]
conv_facts.iconv_trans_heterogeneous_leq' [in DCOIOmega.conv]
conv_facts.iconv_trans_heterogeneous_leq [in DCOIOmega.conv]
conv_facts.iconv_trans_heterogeneous [in DCOIOmega.conv]
conv_facts.ieq_trans_heterogeneous_leq' [in DCOIOmega.conv]
conv_facts.ieq_trans_heterogeneous_leq [in DCOIOmega.conv]
conv_facts.ieq_trans_heterogeneous [in DCOIOmega.conv]
conv_facts.iconv_par2 [in DCOIOmega.conv]
conv_facts.conv_par [in DCOIOmega.conv]
conv_facts.iconv_par [in DCOIOmega.conv]
conv_facts.conv_rpar [in DCOIOmega.conv]
conv_facts.iconv_rpar [in DCOIOmega.conv]
conv_facts.conv_sym [in DCOIOmega.conv]
conv_facts.iconv_sym [in DCOIOmega.conv]
conv_facts.conv_refl [in DCOIOmega.conv]
conv_facts.simulation_star [in DCOIOmega.conv]
conv_facts.simulation [in DCOIOmega.conv]
conv_facts.iok_preservation_star [in DCOIOmega.conv]
conv_facts.iok_preservation [in DCOIOmega.conv]
conv_facts.ieq_iconv [in DCOIOmega.conv]
conv_dec_bot.conv_dec [in DCOIOmega.iconv_dec]
conv_dec_bot.conv_convb [in DCOIOmega.iconv_dec]
conv_dec_bot.convb_conv [in DCOIOmega.iconv_dec]
conv_dec_bot.compute_level_downgrade [in DCOIOmega.iconv_dec]
conv_dec_bot.compute_level_is_min [in DCOIOmega.iconv_dec]

F

factorization_sig.LoRed'_nf_unique [in DCOIOmega.factorization]
factorization_sig.LoRed_wn_sn [in DCOIOmega.factorization]
factorization_sig.nf_no_lored [in DCOIOmega.factorization]
factorization_sig.LoReds'_Pars [in DCOIOmega.factorization]
factorization_sig.LoRed'_Par [in DCOIOmega.factorization]
factorization_sig.LoRedOpt_Par [in DCOIOmega.factorization]
factorization_sig.IsNumP [in DCOIOmega.factorization]
factorization_sig.IsPackP [in DCOIOmega.factorization]
factorization_sig.IsAbsP [in DCOIOmega.factorization]
factorization_sig.standardization' [in DCOIOmega.factorization]
factorization_sig.LoReds_LoReds' [in DCOIOmega.factorization]
factorization_sig.LoRed_LoRed' [in DCOIOmega.factorization]
factorization_sig.LoRed_LoRedOpt [in DCOIOmega.factorization]
factorization_sig.nf_no_red [in DCOIOmega.factorization]
factorization_sig.standardization [in DCOIOmega.factorization]
factorization_sig.LoRed_Let_Cong [in DCOIOmega.factorization]
factorization_sig.LoRed_Seq_Cong [in DCOIOmega.factorization]
factorization_sig.LoRed_J_Cong [in DCOIOmega.factorization]
factorization_sig.LoRed_Eq_Cong [in DCOIOmega.factorization]
factorization_sig.LoRed_Absurd_Cong [in DCOIOmega.factorization]
factorization_sig.LoRed_Pack_Cong [in DCOIOmega.factorization]
factorization_sig.LoRed_Sig_Cong [in DCOIOmega.factorization]
factorization_sig.LoRed_Pi_Cong [in DCOIOmega.factorization]
factorization_sig.LoRed_Ind_Cong [in DCOIOmega.factorization]
factorization_sig.LoRed_App_Cong [in DCOIOmega.factorization]
factorization_sig.NPar_Unit_inv [in DCOIOmega.factorization]
factorization_sig.NPar_Zero_inv [in DCOIOmega.factorization]
factorization_sig.NPar_TT_inv [in DCOIOmega.factorization]
factorization_sig.NPar_Refl_inv [in DCOIOmega.factorization]
factorization_sig.NPar_Let_inv [in DCOIOmega.factorization]
factorization_sig.LoRed_Abs_inv [in DCOIOmega.factorization]
factorization_sig.LoRed_IsNum_inv [in DCOIOmega.factorization]
factorization_sig.LoRed_IsPack_inv [in DCOIOmega.factorization]
factorization_sig.LoRed_IsAbs_inv [in DCOIOmega.factorization]
factorization_sig.NPar_Pack_inv [in DCOIOmega.factorization]
factorization_sig.NPar_Sig_inv [in DCOIOmega.factorization]
factorization_sig.NPar_J_inv [in DCOIOmega.factorization]
factorization_sig.NPar_Eq_inv [in DCOIOmega.factorization]
factorization_sig.NPar_Absurd_inv [in DCOIOmega.factorization]
factorization_sig.NPar_Nat_inv [in DCOIOmega.factorization]
factorization_sig.NPar_Void_inv [in DCOIOmega.factorization]
factorization_sig.NPar_Univ_inv [in DCOIOmega.factorization]
factorization_sig.NPar_Pi_inv [in DCOIOmega.factorization]
factorization_sig.NPar_Ind_inv [in DCOIOmega.factorization]
factorization_sig.NPar_Seq_inv [in DCOIOmega.factorization]
factorization_sig.NPar_App_inv [in DCOIOmega.factorization]
factorization_sig.LoRed_Suc_Cong [in DCOIOmega.factorization]
factorization_sig.LoRed_Abs_Cong [in DCOIOmega.factorization]
factorization_sig.NPars_Pars [in DCOIOmega.factorization]
factorization_sig.HReds_LoReds [in DCOIOmega.factorization]
factorization_sig.HRed_LoRed [in DCOIOmega.factorization]
factorization_sig.NPar_Suc_inv [in DCOIOmega.factorization]
factorization_sig.NPar_Abs_inv [in DCOIOmega.factorization]
factorization_sig.NPar_Var_inv [in DCOIOmega.factorization]
factorization_sig.factorization [in DCOIOmega.factorization]
factorization_sig.local_postponement_star [in DCOIOmega.factorization]
factorization_sig.local_postponement [in DCOIOmega.factorization]
factorization_sig.starseq_erase [in DCOIOmega.factorization]
factorization_sig.split [in DCOIOmega.factorization]
factorization_sig.ipar_starseq_morphing [in DCOIOmega.factorization]
factorization_sig.starseq_ρ_par [in DCOIOmega.factorization]
factorization_sig.starseq_seq_cong [in DCOIOmega.factorization]
factorization_sig.starseq_ind_cong [in DCOIOmega.factorization]
factorization_sig.starseq_j_cong [in DCOIOmega.factorization]
factorization_sig.starseq_let_cong [in DCOIOmega.factorization]
factorization_sig.starseq_app_cong [in DCOIOmega.factorization]
factorization_sig.starseq_suc_cong [in DCOIOmega.factorization]
factorization_sig.starseq_abs_cong [in DCOIOmega.factorization]
factorization_sig.starseq_renaming [in DCOIOmega.factorization]
factorization_sig.starseq_par [in DCOIOmega.factorization]
factorization_sig.merge [in DCOIOmega.factorization]
factorization_sig.HRed_renaming [in DCOIOmega.factorization]
factorization_sig.HR_IndSuc' [in DCOIOmega.factorization]
factorization_sig.HR_LetPack' [in DCOIOmega.factorization]
factorization_sig.HR_AppAbs' [in DCOIOmega.factorization]
factorization_sig.NPar_renaming [in DCOIOmega.factorization]
factorization_sig.NPar_Par [in DCOIOmega.factorization]

G

geq_facts.iok_ieq_downgrade_iok [in DCOIOmega.geq]
geq_facts.ieq_trans_heterogeneous [in DCOIOmega.geq]
geq_facts.ieq_iok_subst [in DCOIOmega.geq]
geq_facts.gieq_morphing_iok [in DCOIOmega.geq]
geq_facts.ieq_morphing_iok [in DCOIOmega.geq]
geq_facts.ieq_morphing_mutual [in DCOIOmega.geq]
geq_facts.ieq_morphing_helper2 [in DCOIOmega.geq]
geq_facts.ieq_morphing_helper [in DCOIOmega.geq]
geq_facts.ieq_subst_cons [in DCOIOmega.geq]
geq_facts.ieq_subst_id [in DCOIOmega.geq]
geq_facts.gieq_refl [in DCOIOmega.geq]
geq_facts.ieq_weakening_mutual [in DCOIOmega.geq]
geq_facts.ieq_pi_inj [in DCOIOmega.geq]
geq_facts.ieq_trans [in DCOIOmega.geq]
geq_facts.ieq_trans_mutual [in DCOIOmega.geq]
geq_facts.ieq_sym [in DCOIOmega.geq]
geq_facts.ieq_sym_mutual [in DCOIOmega.geq]
geq_facts.iok_gieq [in DCOIOmega.geq]
geq_facts.ieq_gieq [in DCOIOmega.geq]
geq_facts.iok_ieq_downgrade [in DCOIOmega.geq]
geq_facts.ieq_downgrade_leq [in DCOIOmega.geq]
geq_facts.ieq_downgrade_mutual [in DCOIOmega.geq]
geq_facts.elookup_deterministic [in DCOIOmega.geq]
geq_facts.iok_ieq [in DCOIOmega.geq]
geq_facts.iok_subst [in DCOIOmega.geq]
geq_facts.iok_morphing [in DCOIOmega.geq]
geq_facts.iok_subst_ok_up [in DCOIOmega.geq]
geq_facts.iok_subst_ok_suc [in DCOIOmega.geq]
geq_facts.iok_renaming [in DCOIOmega.geq]
geq_facts.iok_ren_ok_up [in DCOIOmega.geq]
geq_facts.iok_subst_cons [in DCOIOmega.geq]
geq_facts.iok_subst_id [in DCOIOmega.geq]
geq_facts.iok_subsumption [in DCOIOmega.geq]
geq_facts.IEq_dec [in DCOIOmega.geq]
geq_facts.IEqb_IEq [in DCOIOmega.geq]
geq_facts.nat_eqdec [in DCOIOmega.geq]
geq_facts.IEq_IEqb [in DCOIOmega.geq]
geq_facts.T_leqb_iff [in DCOIOmega.geq]

I

iconv_dec.iconv_dec [in DCOIOmega.iconv_dec]
iconv_dec.iconvb_iconv [in DCOIOmega.iconv_dec]
iconv_dec.iconv_iconvb [in DCOIOmega.iconv_dec]

L

lr_sig.InterpUnivN_Nat [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_back_clos_star [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_back_clos [in DCOIOmega.semtyping]
lr_sig.InterpExt_back_clos [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Univ [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Univ_inv [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Sig_inv_nopf [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Fun_inv_nopf [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Conv [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_IEq [in DCOIOmega.semtyping]
lr_sig.InterpExt_IEq [in DCOIOmega.semtyping]
lr_sig.InterpExt_Sig_inv_nopf [in DCOIOmega.semtyping]
lr_sig.InterpExt_Fun_inv_nopf [in DCOIOmega.semtyping]
lr_sig.InterpExt_Ne_inv' [in DCOIOmega.semtyping]
lr_sig.adequacy [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_WNe [in DCOIOmega.semtyping]
lr_sig.InterpExt_adequacy [in DCOIOmega.semtyping]
lr_sig.wne_var [in DCOIOmega.semtyping]
lr_sig.InterpUniv_Ok [in DCOIOmega.semtyping]
lr_sig.InterpExt_Ok [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_deterministic' [in DCOIOmega.semtyping]
lr_sig.InterpExt_deterministic' [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_deterministic [in DCOIOmega.semtyping]
lr_sig.InterpExt_deterministic [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Nat_inv [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Ne_inv [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Void_inv [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Eq [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Unit [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Unit_inv [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Void [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Eq_inv [in DCOIOmega.semtyping]
lr_sig.InterpExt_Eq_inv [in DCOIOmega.semtyping]
lr_sig.InterpExt_Void_inv [in DCOIOmega.semtyping]
lr_sig.InterpExt_Univ_inv [in DCOIOmega.semtyping]
lr_sig.InterpExt_Unit_inv [in DCOIOmega.semtyping]
lr_sig.InterpExt_Nat_inv [in DCOIOmega.semtyping]
lr_sig.InterpExt_Ne_inv [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_subsumption [in DCOIOmega.semtyping]
lr_sig.InterpExt_subsumption [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_back_preservation_star [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_preservation_star [in DCOIOmega.semtyping]
lr_sig.InterpExt_preservation_star [in DCOIOmega.semtyping]
lr_sig.InterpExt_back_preservation_star [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_preservation [in DCOIOmega.semtyping]
lr_sig.InterpExt_preservation [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_cumulative [in DCOIOmega.semtyping]
lr_sig.InterpExt_cumulative [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Sig_nopf [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_Fun_nopf [in DCOIOmega.semtyping]
lr_sig.InterpExt_Fun_nopf [in DCOIOmega.semtyping]
lr_sig.InterpExt_Sig_inv [in DCOIOmega.semtyping]
lr_sig.InterpExt_Fun_inv [in DCOIOmega.semtyping]
lr_sig.InterpUnivN_nolt [in DCOIOmega.semtyping]
lr_sig.InterpExt_lt_redundant2 [in DCOIOmega.semtyping]
lr_sig.InterpExt_lt_redundant [in DCOIOmega.semtyping]
lr_sig.InterpExt_Univ' [in DCOIOmega.semtyping]
lr_sig.InterpExt_Eq' [in DCOIOmega.semtyping]

N

nat_lattice_bot.bot_prop [in DCOIOmega.toplevel]
nat_lattice.T_eqdec [in DCOIOmega.toplevel]
nat_lattice.join_idempotent [in DCOIOmega.toplevel]
nat_lattice.join_absorptive [in DCOIOmega.toplevel]
nat_lattice.join_associative [in DCOIOmega.toplevel]
nat_lattice.join_commutative [in DCOIOmega.toplevel]
nat_lattice.meet_idempotent [in DCOIOmega.toplevel]
nat_lattice.meet_absorptive [in DCOIOmega.toplevel]
nat_lattice.meet_associative [in DCOIOmega.toplevel]
nat_lattice.meet_commutative [in DCOIOmega.toplevel]
normalform_fact.confluent_nf [in DCOIOmega.normalform]
normalform_fact.ext_wn [in DCOIOmega.normalform]
normalform_fact.wn_eq [in DCOIOmega.normalform]
normalform_fact.wn_pack [in DCOIOmega.normalform]
normalform_fact.wn_sig [in DCOIOmega.normalform]
normalform_fact.wn_pi [in DCOIOmega.normalform]
normalform_fact.wn_abs [in DCOIOmega.normalform]
normalform_fact.wne_let [in DCOIOmega.normalform]
normalform_fact.wne_seq [in DCOIOmega.normalform]
normalform_fact.wne_app [in DCOIOmega.normalform]
normalform_fact.wne_ind [in DCOIOmega.normalform]
normalform_fact.wne_j [in DCOIOmega.normalform]
normalform_fact.wne_absurd [in DCOIOmega.normalform]
normalform_fact.wn_antirenaming [in DCOIOmega.normalform]
normalform_fact.Pars_antirenaming [in DCOIOmega.normalform]
normalform_fact.Par_antirenaming [in DCOIOmega.normalform]
normalform_fact.ne_nf_renaming_with_d [in DCOIOmega.normalform]
normalform_fact.ren_with_d_imp [in DCOIOmega.normalform]
normalform_fact.ren_with_d_up_tm [in DCOIOmega.normalform]
normalform_fact.ren_with_d_ne [in DCOIOmega.normalform]
normalform_fact.var_or_d_ne [in DCOIOmega.normalform]
normalform_fact.ren_var_or_d [in DCOIOmega.normalform]
normalform_fact.ne_preservation [in DCOIOmega.normalform]
normalform_fact.nf_preservation [in DCOIOmega.normalform]
normalform_fact.nf_ne_preservation [in DCOIOmega.normalform]
normalform_fact.nf_refl_star [in DCOIOmega.normalform]
normalform_fact.nf_refl [in DCOIOmega.normalform]
normalform_fact.ne_nf_renaming [in DCOIOmega.normalform]
normalform_fact.ne_nat_val [in DCOIOmega.normalform]
normalform_fact.nat_val_nf [in DCOIOmega.normalform]
normalform_fact.nf_wn [in DCOIOmega.normalform]
normalform_fact.wne_wn [in DCOIOmega.normalform]
normalform_fact.ne_nf [in DCOIOmega.normalform]

P

par_facts.S_Ind [in DCOIOmega.par]
par_facts.P_SeqTT_star [in DCOIOmega.par]
par_facts.S_Seq [in DCOIOmega.par]
par_facts.S_Suc [in DCOIOmega.par]
par_facts.S_Eq [in DCOIOmega.par]
par_facts.S_Pack [in DCOIOmega.par]
par_facts.S_Absurd [in DCOIOmega.par]
par_facts.S_Abs [in DCOIOmega.par]
par_facts.S_Sig [in DCOIOmega.par]
par_facts.S_Pi [in DCOIOmega.par]
par_facts.S_Let [in DCOIOmega.par]
par_facts.S_J [in DCOIOmega.par]
par_facts.S_AppLR [in DCOIOmega.par]
par_facts.Pars_confluent [in DCOIOmega.par]
par_facts.Par_confluent [in DCOIOmega.par]
par_facts.Par_triangle [in DCOIOmega.par]
par_facts.P_LetPack_star [in DCOIOmega.par]
par_facts.P_JRefl_star [in DCOIOmega.par]
par_facts.P_IndSuc_star' [in DCOIOmega.par]
par_facts.P_IndSuc_star [in DCOIOmega.par]
par_facts.P_IndZero_star [in DCOIOmega.par]
par_facts.Pars_sig_inv [in DCOIOmega.par]
par_facts.Pars_univ_inv [in DCOIOmega.par]
par_facts.Pars_eq_inv [in DCOIOmega.par]
par_facts.Pars_pi_inv [in DCOIOmega.par]
par_facts.Coherent_cong_helper [in DCOIOmega.par]
par_facts.Pars_cong_star [in DCOIOmega.par]
par_facts.Par_cong2 [in DCOIOmega.par]
par_facts.Par_cong [in DCOIOmega.par]
par_facts.Par_subst_star [in DCOIOmega.par]
par_facts.Par_subst [in DCOIOmega.par]
par_facts.good_Pars_morphing_ext2 [in DCOIOmega.par]
par_facts.good_Pars_morphing_ext [in DCOIOmega.par]
par_facts.Pars_morphing_star [in DCOIOmega.par]
par_facts.Pars_morphing [in DCOIOmega.par]
par_facts.Par_morphing_star [in DCOIOmega.par]
par_facts.Par_morphing [in DCOIOmega.par]
par_facts.Par_morphing_lift2 [in DCOIOmega.par]
par_facts.Par_morphing_lift [in DCOIOmega.par]
par_facts.Par_morphing_lift_n [in DCOIOmega.par]
par_facts.Pars_renaming [in DCOIOmega.par]
par_facts.Par_renaming [in DCOIOmega.par]
par_facts.P_LetPackCBN' [in DCOIOmega.par]
par_facts.P_LetPack' [in DCOIOmega.par]
par_facts.P_IndSuc' [in DCOIOmega.par]
par_facts.P_AppAbs' [in DCOIOmega.par]
par_facts.P_AppAbs_cbn [in DCOIOmega.par]
par_facts.Par_refl [in DCOIOmega.par]
preservation.good_morphing_iok_subst_ok [in DCOIOmega.preservation]
preservation.good_morphing_up [in DCOIOmega.preservation]
preservation.good_morphing_cons [in DCOIOmega.preservation]
preservation.good_morphing_nil [in DCOIOmega.preservation]
preservation.good_morphing_suc [in DCOIOmega.preservation]
preservation.good_renaming_suc [in DCOIOmega.preservation]
preservation.good_renaming_up [in DCOIOmega.preservation]
preservation.here' [in DCOIOmega.preservation]
preservation.lookup_deter [in DCOIOmega.preservation]
preservation.morphing_Syn_Univ [in DCOIOmega.preservation]
preservation.morphing_Syn [in DCOIOmega.preservation]
preservation.preservation_helper2 [in DCOIOmega.preservation]
preservation.preservation_helper [in DCOIOmega.preservation]
preservation.renaming_Syn_Univ [in DCOIOmega.preservation]
preservation.renaming_Syn [in DCOIOmega.preservation]
preservation.renaming_Syn_helper [in DCOIOmega.preservation]
preservation.subject_reduction_star [in DCOIOmega.preservation]
preservation.subject_reduction [in DCOIOmega.preservation]
preservation.subst_Syn_Univ [in DCOIOmega.preservation]
preservation.subst_Syn [in DCOIOmega.preservation]
preservation.subsumption [in DCOIOmega.preservation]
preservation.there' [in DCOIOmega.preservation]
preservation.T_Par [in DCOIOmega.preservation]
preservation.T_Let_simpl' [in DCOIOmega.preservation]
preservation.T_Let_simpl [in DCOIOmega.preservation]
preservation.T_Refl' [in DCOIOmega.preservation]
preservation.T_Abs_simpl [in DCOIOmega.preservation]
preservation.T_J_simpl [in DCOIOmega.preservation]
preservation.T_Var_inv [in DCOIOmega.preservation]
preservation.T_Eq_simpl [in DCOIOmega.preservation]
preservation.T_Let' [in DCOIOmega.preservation]
preservation.T_Pack' [in DCOIOmega.preservation]
preservation.T_J' [in DCOIOmega.preservation]
preservation.T_Seq' [in DCOIOmega.preservation]
preservation.T_App' [in DCOIOmega.preservation]
preservation.T_Ind' [in DCOIOmega.preservation]
preservation.weakening_Syn_Univ [in DCOIOmega.preservation]
preservation.weakening_Syn' [in DCOIOmega.preservation]
preservation.weakening_Syn [in DCOIOmega.preservation]
preservation.Wff_lookup [in DCOIOmega.preservation]
preservation.Wt_J_inv [in DCOIOmega.preservation]
preservation.Wt_Seq_inv [in DCOIOmega.preservation]
preservation.Wt_TT_inv [in DCOIOmega.preservation]
preservation.Wt_Absurd_inv [in DCOIOmega.preservation]
preservation.Wt_Refl_Coherent [in DCOIOmega.preservation]
preservation.Wt_Suc_inv [in DCOIOmega.preservation]
preservation.Wt_Refl_inv [in DCOIOmega.preservation]
preservation.Wt_Let_inv [in DCOIOmega.preservation]
preservation.Wt_Eq_inv [in DCOIOmega.preservation]
preservation.Wt_Ind_inv [in DCOIOmega.preservation]
preservation.Wt_App_inv [in DCOIOmega.preservation]
preservation.Wt_regularity [in DCOIOmega.preservation]
preservation.Wt_Pack_inv [in DCOIOmega.preservation]
preservation.Wt_Sig_Univ_inv [in DCOIOmega.preservation]
preservation.Wt_Abs_inv [in DCOIOmega.preservation]
preservation.Wt_Pi_Univ_inv [in DCOIOmega.preservation]
preservation.Wt_Sig_inv [in DCOIOmega.preservation]
preservation.Wt_Pi_inv [in DCOIOmega.preservation]
preservation.Wt_Univ [in DCOIOmega.preservation]
preservation.Wt_Wff [in DCOIOmega.preservation]
Properties.sub_eqdec [in DCOIOmega.Lattice.All]

S

scons_comp [in DCOIOmega.Autosubst2.unscoped]
scons_eta [in DCOIOmega.Autosubst2.unscoped]
scons_eta_id [in DCOIOmega.Autosubst2.unscoped]
Solver.leq_meet_prime [in DCOIOmega.Lattice.All]
Solver.leq_join_prime [in DCOIOmega.Lattice.All]
Solver.leq_join_iff [in DCOIOmega.Lattice.All]
Solver.leq_meet_iff [in DCOIOmega.Lattice.All]
Solver.leq_trans [in DCOIOmega.Lattice.All]
Solver.leq_join [in DCOIOmega.Lattice.All]
Solver.leq_lat_leq_lat'_iff [in DCOIOmega.Lattice.All]
Solver.meet_leq [in DCOIOmega.Lattice.All]
Solver.splitLeqForward_complete [in DCOIOmega.Lattice.All]
Solver.splitLeq_iff [in DCOIOmega.Lattice.All]
Solver.splitLeq_complete [in DCOIOmega.Lattice.All]
Solver.splitLeq_sound [in DCOIOmega.Lattice.All]
soundness.iok_ρ_ok_morphing [in DCOIOmega.soundness]
soundness.normalization [in DCOIOmega.soundness]
soundness.renaming_SemWt [in DCOIOmega.soundness]
soundness.SemWff_lookup [in DCOIOmega.soundness]
soundness.SemWt_Univ [in DCOIOmega.soundness]
soundness.soundness [in DCOIOmega.soundness]
soundness.weakening_Sem [in DCOIOmega.soundness]
soundness.wt_ρ_ok_morphing_iok [in DCOIOmega.soundness]
soundness.ρ_ok_renaming [in DCOIOmega.soundness]
soundness.ρ_ok_cons [in DCOIOmega.soundness]
soundness.ρ_ok_id [in DCOIOmega.soundness]
soundness.ρ_ok_iok [in DCOIOmega.soundness]
syntax_sig.renRen'_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.renRen_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.renComp'_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.renComp_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.compRen'_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.compRen_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.compComp'_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.compComp_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.varLRen_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.varL_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.rinstId_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.instId_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.rinstInst_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tUnit [in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tSeq [in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tTT [in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tNat [in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tInd [in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tSuc [in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tZero [in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tLet [in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tPack [in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tSig [in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tRefl [in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tJ [in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tEq [in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tAbsurd [in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tVoid [in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tUniv [in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tPi [in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tApp [in DCOIOmega.Autosubst2.syntax]
syntax_sig.congr_tAbs [in DCOIOmega.Autosubst2.syntax]

T

typing_conv_facts.lookup_good_renaming_iok_subst_ok [in DCOIOmega.typing_conv]
typing_conv_facts.typing_conv [in DCOIOmega.typing_conv]
typing_conv_facts.Wt_IOk_Downgrade [in DCOIOmega.typing_conv]
typing_conv_facts.typing_iok [in DCOIOmega.typing_conv]
typing_conv_facts.elookup_lookup [in DCOIOmega.typing_conv]
typing_conv_facts.lookup_elookup [in DCOIOmega.typing_conv]

U

up_ren_ren [in DCOIOmega.Autosubst2.unscoped]

---

Axiom Index

L

LatticeWithBot.bot [in DCOIOmega.iconv_dec]
LatticeWithBot.bot_prop [in DCOIOmega.iconv_dec]
Lattice.join [in DCOIOmega.Lattice.All]
Lattice.join_idempotent [in DCOIOmega.Lattice.All]
Lattice.join_absorptive [in DCOIOmega.Lattice.All]
Lattice.join_associative [in DCOIOmega.Lattice.All]
Lattice.join_commutative [in DCOIOmega.Lattice.All]
Lattice.meet [in DCOIOmega.Lattice.All]
Lattice.meet_idempotent [in DCOIOmega.Lattice.All]
Lattice.meet_absorptive [in DCOIOmega.Lattice.All]
Lattice.meet_associative [in DCOIOmega.Lattice.All]
Lattice.meet_commutative [in DCOIOmega.Lattice.All]
Lattice.T [in DCOIOmega.Lattice.All]
Lattice.T_eqdec [in DCOIOmega.Lattice.All]
Lattice.T_eqb [in DCOIOmega.Lattice.All]

---

Constructor Index

F

factorization_sig.IsNumFalse [in DCOIOmega.factorization]
factorization_sig.IsSuc [in DCOIOmega.factorization]
factorization_sig.IsZero [in DCOIOmega.factorization]
factorization_sig.isPackFalse [in DCOIOmega.factorization]
factorization_sig.IsPackTrue [in DCOIOmega.factorization]
factorization_sig.isAbsFalse [in DCOIOmega.factorization]
factorization_sig.IsAbsTrue [in DCOIOmega.factorization]
factorization_sig.LoR_SeqTT [in DCOIOmega.factorization]
factorization_sig.LoR_Seq1 [in DCOIOmega.factorization]
factorization_sig.LoR_Seq0 [in DCOIOmega.factorization]
factorization_sig.LoR_Suc [in DCOIOmega.factorization]
factorization_sig.LoR_IndSuc [in DCOIOmega.factorization]
factorization_sig.LoR_IndZero [in DCOIOmega.factorization]
factorization_sig.LoR_Ind2 [in DCOIOmega.factorization]
factorization_sig.LoR_Ind1 [in DCOIOmega.factorization]
factorization_sig.LoR_Ind0 [in DCOIOmega.factorization]
factorization_sig.LoR_LetPack [in DCOIOmega.factorization]
factorization_sig.LoR_Let1 [in DCOIOmega.factorization]
factorization_sig.LoR_Let0 [in DCOIOmega.factorization]
factorization_sig.LoR_Pack1 [in DCOIOmega.factorization]
factorization_sig.LoR_Pack0 [in DCOIOmega.factorization]
factorization_sig.LoR_Sig1 [in DCOIOmega.factorization]
factorization_sig.LoR_Sig0 [in DCOIOmega.factorization]
factorization_sig.LoR_JRefl [in DCOIOmega.factorization]
factorization_sig.LoR_J1 [in DCOIOmega.factorization]
factorization_sig.LoR_J0 [in DCOIOmega.factorization]
factorization_sig.LoR_Eq1 [in DCOIOmega.factorization]
factorization_sig.LoR_Eq0 [in DCOIOmega.factorization]
factorization_sig.LoR_Absurd [in DCOIOmega.factorization]
factorization_sig.LoR_AppAbs [in DCOIOmega.factorization]
factorization_sig.LoR_App1 [in DCOIOmega.factorization]
factorization_sig.LoR_App0 [in DCOIOmega.factorization]
factorization_sig.LoR_Abs [in DCOIOmega.factorization]
factorization_sig.LoR_Pi1 [in DCOIOmega.factorization]
factorization_sig.LoR_Pi0 [in DCOIOmega.factorization]
factorization_sig.S_Step [in DCOIOmega.factorization]
factorization_sig.S_Refl [in DCOIOmega.factorization]
factorization_sig.NP_Seq [in DCOIOmega.factorization]
factorization_sig.NP_Unit [in DCOIOmega.factorization]
factorization_sig.NP_TT [in DCOIOmega.factorization]
factorization_sig.NP_Ind [in DCOIOmega.factorization]
factorization_sig.NP_Suc [in DCOIOmega.factorization]
factorization_sig.NP_Zero [in DCOIOmega.factorization]
factorization_sig.NP_Nat [in DCOIOmega.factorization]
factorization_sig.NP_Refl [in DCOIOmega.factorization]
factorization_sig.NP_Void [in DCOIOmega.factorization]
factorization_sig.NP_Let [in DCOIOmega.factorization]
factorization_sig.NP_Pack [in DCOIOmega.factorization]
factorization_sig.NP_Sig [in DCOIOmega.factorization]
factorization_sig.NP_J [in DCOIOmega.factorization]
factorization_sig.NP_Eq [in DCOIOmega.factorization]
factorization_sig.NP_Absurd [in DCOIOmega.factorization]
factorization_sig.NP_App [in DCOIOmega.factorization]
factorization_sig.NP_Abs [in DCOIOmega.factorization]
factorization_sig.NP_Pi [in DCOIOmega.factorization]
factorization_sig.NP_Univ [in DCOIOmega.factorization]
factorization_sig.NP_Var [in DCOIOmega.factorization]
factorization_sig.HR_SeqTT [in DCOIOmega.factorization]
factorization_sig.HR_Seq [in DCOIOmega.factorization]
factorization_sig.HR_IndSuc [in DCOIOmega.factorization]
factorization_sig.HR_IndZero [in DCOIOmega.factorization]
factorization_sig.HR_Ind [in DCOIOmega.factorization]
factorization_sig.HR_LetPack [in DCOIOmega.factorization]
factorization_sig.HR_Let [in DCOIOmega.factorization]
factorization_sig.HR_JRefl [in DCOIOmega.factorization]
factorization_sig.HR_J [in DCOIOmega.factorization]
factorization_sig.HR_AppAbs [in DCOIOmega.factorization]
factorization_sig.HR_App [in DCOIOmega.factorization]

G

geq_sig.GI_InDist [in DCOIOmega.geq]
geq_sig.GI_Dist [in DCOIOmega.geq]
geq_sig.I_Seq [in DCOIOmega.geq]
geq_sig.I_TT [in DCOIOmega.geq]
geq_sig.I_Unit [in DCOIOmega.geq]
geq_sig.I_Nat [in DCOIOmega.geq]
geq_sig.I_Ind [in DCOIOmega.geq]
geq_sig.I_Suc [in DCOIOmega.geq]
geq_sig.I_Zero [in DCOIOmega.geq]
geq_sig.I_Let [in DCOIOmega.geq]
geq_sig.I_Pack [in DCOIOmega.geq]
geq_sig.I_Sig [in DCOIOmega.geq]
geq_sig.I_J [in DCOIOmega.geq]
geq_sig.I_Eq [in DCOIOmega.geq]
geq_sig.I_Refl [in DCOIOmega.geq]
geq_sig.I_Absurd [in DCOIOmega.geq]
geq_sig.I_Void [in DCOIOmega.geq]
geq_sig.I_App [in DCOIOmega.geq]
geq_sig.I_Abs [in DCOIOmega.geq]
geq_sig.I_Pi [in DCOIOmega.geq]
geq_sig.I_Univ [in DCOIOmega.geq]
geq_sig.I_Var [in DCOIOmega.geq]
geq_sig.IO_Seq [in DCOIOmega.geq]
geq_sig.IO_TT [in DCOIOmega.geq]
geq_sig.IO_Unit [in DCOIOmega.geq]
geq_sig.IO_Nat [in DCOIOmega.geq]
geq_sig.IO_Ind [in DCOIOmega.geq]
geq_sig.IO_Suc [in DCOIOmega.geq]
geq_sig.IO_Zero [in DCOIOmega.geq]
geq_sig.IO_Let [in DCOIOmega.geq]
geq_sig.IO_Pack [in DCOIOmega.geq]
geq_sig.IO_Sig [in DCOIOmega.geq]
geq_sig.IO_J [in DCOIOmega.geq]
geq_sig.IO_Eq [in DCOIOmega.geq]
geq_sig.IO_Refl [in DCOIOmega.geq]
geq_sig.IO_Absurd [in DCOIOmega.geq]
geq_sig.IO_Void [in DCOIOmega.geq]
geq_sig.IO_App [in DCOIOmega.geq]
geq_sig.IO_Abs [in DCOIOmega.geq]
geq_sig.IO_Pi [in DCOIOmega.geq]
geq_sig.IO_Univ [in DCOIOmega.geq]
geq_sig.IO_Var [in DCOIOmega.geq]

I

ids [in DCOIOmega.Autosubst2.unscoped]

L

lr_sig.InterpExt_Unit [in DCOIOmega.semtyping]
lr_sig.InterpExt_Step [in DCOIOmega.semtyping]
lr_sig.InterpExt_Sig [in DCOIOmega.semtyping]
lr_sig.InterpExt_Eq [in DCOIOmega.semtyping]
lr_sig.InterpExt_Void [in DCOIOmega.semtyping]
lr_sig.InterpExt_Univ [in DCOIOmega.semtyping]
lr_sig.InterpExt_Fun [in DCOIOmega.semtyping]
lr_sig.InterpExt_Nat [in DCOIOmega.semtyping]
lr_sig.InterpExt_Ne [in DCOIOmega.semtyping]

P

par_sig.P_Unit [in DCOIOmega.par]
par_sig.P_SeqTT [in DCOIOmega.par]
par_sig.P_Seq [in DCOIOmega.par]
par_sig.P_TT [in DCOIOmega.par]
par_sig.P_Nat [in DCOIOmega.par]
par_sig.P_IndSuc [in DCOIOmega.par]
par_sig.P_IndZero [in DCOIOmega.par]
par_sig.P_Ind [in DCOIOmega.par]
par_sig.P_Suc [in DCOIOmega.par]
par_sig.P_Zero [in DCOIOmega.par]
par_sig.P_LetPack [in DCOIOmega.par]
par_sig.P_Let [in DCOIOmega.par]
par_sig.P_Pack [in DCOIOmega.par]
par_sig.P_Sig [in DCOIOmega.par]
par_sig.P_JRefl [in DCOIOmega.par]
par_sig.P_J [in DCOIOmega.par]
par_sig.P_Eq [in DCOIOmega.par]
par_sig.P_Refl [in DCOIOmega.par]
par_sig.P_Absurd [in DCOIOmega.par]
par_sig.P_Void [in DCOIOmega.par]
par_sig.P_AppAbs [in DCOIOmega.par]
par_sig.P_App [in DCOIOmega.par]
par_sig.P_Abs [in DCOIOmega.par]
par_sig.P_Pi [in DCOIOmega.par]
par_sig.P_Univ [in DCOIOmega.par]
par_sig.P_Var [in DCOIOmega.par]

R

ren1 [in DCOIOmega.Autosubst2.unscoped]
ren2 [in DCOIOmega.Autosubst2.unscoped]
ren3 [in DCOIOmega.Autosubst2.unscoped]
ren4 [in DCOIOmega.Autosubst2.unscoped]
ren5 [in DCOIOmega.Autosubst2.unscoped]

S

Solver.Join [in DCOIOmega.Lattice.All]
Solver.Meet [in DCOIOmega.Lattice.All]
Solver.Var [in DCOIOmega.Lattice.All]
soundness.SemWff_cons [in DCOIOmega.soundness]
soundness.SemWff_nil [in DCOIOmega.soundness]
subst1 [in DCOIOmega.Autosubst2.unscoped]
subst2 [in DCOIOmega.Autosubst2.unscoped]
subst3 [in DCOIOmega.Autosubst2.unscoped]
subst4 [in DCOIOmega.Autosubst2.unscoped]
subst5 [in DCOIOmega.Autosubst2.unscoped]
syntax_sig.up_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.tUnit [in DCOIOmega.Autosubst2.syntax]
syntax_sig.tSeq [in DCOIOmega.Autosubst2.syntax]
syntax_sig.tTT [in DCOIOmega.Autosubst2.syntax]
syntax_sig.tNat [in DCOIOmega.Autosubst2.syntax]
syntax_sig.tInd [in DCOIOmega.Autosubst2.syntax]
syntax_sig.tSuc [in DCOIOmega.Autosubst2.syntax]
syntax_sig.tZero [in DCOIOmega.Autosubst2.syntax]
syntax_sig.tLet [in DCOIOmega.Autosubst2.syntax]
syntax_sig.tPack [in DCOIOmega.Autosubst2.syntax]
syntax_sig.tSig [in DCOIOmega.Autosubst2.syntax]
syntax_sig.tRefl [in DCOIOmega.Autosubst2.syntax]
syntax_sig.tJ [in DCOIOmega.Autosubst2.syntax]
syntax_sig.tEq [in DCOIOmega.Autosubst2.syntax]
syntax_sig.tAbsurd [in DCOIOmega.Autosubst2.syntax]
syntax_sig.tVoid [in DCOIOmega.Autosubst2.syntax]
syntax_sig.tUniv [in DCOIOmega.Autosubst2.syntax]
syntax_sig.tPi [in DCOIOmega.Autosubst2.syntax]
syntax_sig.tApp [in DCOIOmega.Autosubst2.syntax]
syntax_sig.tAbs [in DCOIOmega.Autosubst2.syntax]
syntax_sig.var_tm [in DCOIOmega.Autosubst2.syntax]

T

typing_sig.Wff_cons [in DCOIOmega.typing]
typing_sig.Wff_nil [in DCOIOmega.typing]
typing_sig.T_Seq [in DCOIOmega.typing]
typing_sig.T_Unit [in DCOIOmega.typing]
typing_sig.T_TT [in DCOIOmega.typing]
typing_sig.T_Let [in DCOIOmega.typing]
typing_sig.T_Pack [in DCOIOmega.typing]
typing_sig.T_Sig [in DCOIOmega.typing]
typing_sig.T_J [in DCOIOmega.typing]
typing_sig.T_Eq [in DCOIOmega.typing]
typing_sig.T_Refl [in DCOIOmega.typing]
typing_sig.T_Absurd [in DCOIOmega.typing]
typing_sig.T_Void [in DCOIOmega.typing]
typing_sig.T_Univ [in DCOIOmega.typing]
typing_sig.T_Nat [in DCOIOmega.typing]
typing_sig.T_Ind [in DCOIOmega.typing]
typing_sig.T_Suc [in DCOIOmega.typing]
typing_sig.T_Zero [in DCOIOmega.typing]
typing_sig.T_Conv [in DCOIOmega.typing]
typing_sig.T_App [in DCOIOmega.typing]
typing_sig.T_Abs [in DCOIOmega.typing]
typing_sig.T_Pi [in DCOIOmega.typing]
typing_sig.T_Var [in DCOIOmega.typing]
typing_sig.there [in DCOIOmega.typing]
typing_sig.here [in DCOIOmega.typing]

---

Projection Index

I

ids [in DCOIOmega.Autosubst2.unscoped]

R

ren1 [in DCOIOmega.Autosubst2.unscoped]
ren2 [in DCOIOmega.Autosubst2.unscoped]
ren3 [in DCOIOmega.Autosubst2.unscoped]
ren4 [in DCOIOmega.Autosubst2.unscoped]
ren5 [in DCOIOmega.Autosubst2.unscoped]

S

subst1 [in DCOIOmega.Autosubst2.unscoped]
subst2 [in DCOIOmega.Autosubst2.unscoped]
subst3 [in DCOIOmega.Autosubst2.unscoped]
subst4 [in DCOIOmega.Autosubst2.unscoped]
subst5 [in DCOIOmega.Autosubst2.unscoped]
syntax_sig.up_tm [in DCOIOmega.Autosubst2.syntax]

---

Inductive Index

F

factorization_sig.IsNum [in DCOIOmega.factorization]
factorization_sig.IsPack [in DCOIOmega.factorization]
factorization_sig.IsAbs [in DCOIOmega.factorization]
factorization_sig.LoRed [in DCOIOmega.factorization]
factorization_sig.starseq [in DCOIOmega.factorization]
factorization_sig.NPar [in DCOIOmega.factorization]
factorization_sig.HRed [in DCOIOmega.factorization]

G

geq_sig.GIEq [in DCOIOmega.geq]
geq_sig.IEq [in DCOIOmega.geq]
geq_sig.IOk [in DCOIOmega.geq]

L

lr_sig.InterpExt [in DCOIOmega.semtyping]

P

par_sig.Par [in DCOIOmega.par]

R

Ren1 [in DCOIOmega.Autosubst2.unscoped]
Ren2 [in DCOIOmega.Autosubst2.unscoped]
Ren3 [in DCOIOmega.Autosubst2.unscoped]
Ren4 [in DCOIOmega.Autosubst2.unscoped]
Ren5 [in DCOIOmega.Autosubst2.unscoped]

S

Solver.lexp [in DCOIOmega.Lattice.All]
soundness.SemWff [in DCOIOmega.soundness]
Subst1 [in DCOIOmega.Autosubst2.unscoped]
Subst2 [in DCOIOmega.Autosubst2.unscoped]
Subst3 [in DCOIOmega.Autosubst2.unscoped]
Subst4 [in DCOIOmega.Autosubst2.unscoped]
Subst5 [in DCOIOmega.Autosubst2.unscoped]
syntax_sig.Up_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.tm [in DCOIOmega.Autosubst2.syntax]

T

typing_sig.Wff [in DCOIOmega.typing]
typing_sig.Wt [in DCOIOmega.typing]
typing_sig.lookup [in DCOIOmega.typing]

V

Var [in DCOIOmega.Autosubst2.unscoped]

---

Instance Index

I

idsRen [in DCOIOmega.Autosubst2.unscoped]

S

syntax_sig.Up_tm_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.VarInstance_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.Ren_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.Subst_tm [in DCOIOmega.Autosubst2.syntax]

---

Section Index

S

syntax_sig.tm [in DCOIOmega.Autosubst2.syntax]

---

Abbreviation Index

F

fin [in DCOIOmega.Autosubst2.unscoped]

S

shift [in DCOIOmega.Autosubst2.unscoped]

---

Definition Index

A

ap [in DCOIOmega.Autosubst2.unscoped]
apc [in DCOIOmega.Autosubst2.unscoped]

C

cod [in DCOIOmega.Autosubst2.axioms]
cod_comp [in DCOIOmega.Autosubst2.axioms]
cod_ext [in DCOIOmega.Autosubst2.axioms]
cod_id [in DCOIOmega.Autosubst2.axioms]
cod_map [in DCOIOmega.Autosubst2.axioms]
conv_sig.conv [in DCOIOmega.conv]
conv_sig.iconv [in DCOIOmega.conv]
conv_dec_bot.convb [in DCOIOmega.iconv_dec]
conv_dec_bot.compute_level [in DCOIOmega.iconv_dec]

F

factorization_sig.LoRed_normalize [in DCOIOmega.factorization]
factorization_sig.IsNum_sind [in DCOIOmega.factorization]
factorization_sig.IsNum_ind [in DCOIOmega.factorization]
factorization_sig.IsPack_sind [in DCOIOmega.factorization]
factorization_sig.IsPack_ind [in DCOIOmega.factorization]
factorization_sig.IsAbs_sind [in DCOIOmega.factorization]
factorization_sig.IsAbs_ind [in DCOIOmega.factorization]
factorization_sig.LoRed' [in DCOIOmega.factorization]
factorization_sig.LoRedOpt [in DCOIOmega.factorization]
factorization_sig.LoRed_sind [in DCOIOmega.factorization]
factorization_sig.LoRed_ind [in DCOIOmega.factorization]
factorization_sig.isNum [in DCOIOmega.factorization]
factorization_sig.isPack [in DCOIOmega.factorization]
factorization_sig.isAbs [in DCOIOmega.factorization]
factorization_sig.starseq_sind [in DCOIOmega.factorization]
factorization_sig.starseq_ind [in DCOIOmega.factorization]
factorization_sig.NPar_sind [in DCOIOmega.factorization]
factorization_sig.NPar_ind [in DCOIOmega.factorization]
factorization_sig.HRed_sind [in DCOIOmega.factorization]
factorization_sig.HRed_ind [in DCOIOmega.factorization]
funcomp [in DCOIOmega.Autosubst2.unscoped]
funcomp [in DCOIOmega.Autosubst2.axioms]

G

geq_facts.ieq_good_morphing [in DCOIOmega.geq]
geq_facts.ieq_weakening_helper [in DCOIOmega.geq]
geq_sig.iok_subst_ok [in DCOIOmega.geq]
geq_sig.iok_ren_ok [in DCOIOmega.geq]
geq_sig.GIEq_ind' [in DCOIOmega.geq]
geq_sig.IEq_ind' [in DCOIOmega.geq]
geq_sig.IEqb [in DCOIOmega.geq]
geq_sig.GIEq_sind [in DCOIOmega.geq]
geq_sig.GIEq_ind [in DCOIOmega.geq]
geq_sig.IEq_sind [in DCOIOmega.geq]
geq_sig.IEq_ind [in DCOIOmega.geq]
geq_sig.IOk_sind [in DCOIOmega.geq]
geq_sig.IOk_ind [in DCOIOmega.geq]
geq_sig.elookup [in DCOIOmega.geq]
geq_sig.econtext [in DCOIOmega.geq]

I

iconv_dec.iconvb [in DCOIOmega.iconv_dec]
id [in DCOIOmega.Autosubst2.unscoped]

L

list_comp [in DCOIOmega.Autosubst2.axioms]
list_id [in DCOIOmega.Autosubst2.axioms]
list_ext [in DCOIOmega.Autosubst2.axioms]
lr_sig.CR [in DCOIOmega.semtyping]
lr_sig.InterpUnivN [in DCOIOmega.semtyping]
lr_sig.InterpExt_sind [in DCOIOmega.semtyping]
lr_sig.InterpExt_ind [in DCOIOmega.semtyping]
lr_sig.SumSpace [in DCOIOmega.semtyping]
lr_sig.ProdSpace [in DCOIOmega.semtyping]

N

nat_lattice_bot.bot [in DCOIOmega.toplevel]
nat_lattice.T_eqb [in DCOIOmega.toplevel]
nat_lattice.join [in DCOIOmega.toplevel]
nat_lattice.meet [in DCOIOmega.toplevel]
nat_lattice.T [in DCOIOmega.toplevel]
normalform_sig.ren_with_d [in DCOIOmega.normalform]
normalform_sig.var_or_d [in DCOIOmega.normalform]
normalform_sig.wne [in DCOIOmega.normalform]
normalform_sig.wn [in DCOIOmega.normalform]
normalform_sig.nf [in DCOIOmega.normalform]
normalform_sig.ne [in DCOIOmega.normalform]

P

par_facts.Coherent_m [in DCOIOmega.par]
par_facts.Par_m [in DCOIOmega.par]
par_facts.up_tm_tm_n [in DCOIOmega.par]
par_sig.Par_sind [in DCOIOmega.par]
par_sig.Par_ind [in DCOIOmega.par]
preservation.lookup_good_morphing [in DCOIOmega.preservation]
prod_comp [in DCOIOmega.Autosubst2.axioms]
prod_ext [in DCOIOmega.Autosubst2.axioms]
prod_id [in DCOIOmega.Autosubst2.axioms]
prod_map [in DCOIOmega.Autosubst2.axioms]

S

scons [in DCOIOmega.Autosubst2.unscoped]
Solver.denoteLexp [in DCOIOmega.Lattice.All]
Solver.lexp_size [in DCOIOmega.Lattice.All]
Solver.lexp_sind [in DCOIOmega.Lattice.All]
Solver.lexp_rec [in DCOIOmega.Lattice.All]
Solver.lexp_ind [in DCOIOmega.Lattice.All]
Solver.lexp_rect [in DCOIOmega.Lattice.All]
Solver.splitLeq [in DCOIOmega.Lattice.All]
Solver.splitLeqForward [in DCOIOmega.Lattice.All]
soundness.SemWff_sind [in DCOIOmega.soundness]
soundness.SemWff_ind [in DCOIOmega.soundness]
soundness.SemWt [in DCOIOmega.soundness]
soundness.ρ_ok [in DCOIOmega.soundness]
syntax_sig.rinst_inst_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.rinstInst_up_tm_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.compSubstSubst_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.up_subst_subst_tm_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.compSubstRen_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.up_subst_ren_tm_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.compRenSubst_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.up_ren_subst_tm_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.compRenRen_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.up_ren_ren_tm_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.ext_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.upExt_tm_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.extRen_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.upExtRen_tm_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.idSubst_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.upId_tm_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.subst_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.up_tm_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.ren_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.upRen_tm_tm [in DCOIOmega.Autosubst2.syntax]
syntax_sig.tm_sind [in DCOIOmega.Autosubst2.syntax]
syntax_sig.tm_rec [in DCOIOmega.Autosubst2.syntax]
syntax_sig.tm_ind [in DCOIOmega.Autosubst2.syntax]
syntax_sig.tm_rect [in DCOIOmega.Autosubst2.syntax]

T

typing_sig.wff_ind [in DCOIOmega.typing]
typing_sig.wt_ind [in DCOIOmega.typing]
typing_sig.Wff_sind [in DCOIOmega.typing]
typing_sig.Wff_ind [in DCOIOmega.typing]
typing_sig.Wt_sind [in DCOIOmega.typing]
typing_sig.Wt_ind [in DCOIOmega.typing]
typing_sig.c2e [in DCOIOmega.typing]
typing_sig.lookup_good_renaming [in DCOIOmega.typing]
typing_sig.lookup_sind [in DCOIOmega.typing]
typing_sig.lookup_ind [in DCOIOmega.typing]
typing_sig.context [in DCOIOmega.typing]

U

up_ren [in DCOIOmega.Autosubst2.unscoped]

V

var_zero [in DCOIOmega.Autosubst2.unscoped]

---

Record Index

R

Ren1 [in DCOIOmega.Autosubst2.unscoped]
Ren2 [in DCOIOmega.Autosubst2.unscoped]
Ren3 [in DCOIOmega.Autosubst2.unscoped]
Ren4 [in DCOIOmega.Autosubst2.unscoped]
Ren5 [in DCOIOmega.Autosubst2.unscoped]

S

Subst1 [in DCOIOmega.Autosubst2.unscoped]
Subst2 [in DCOIOmega.Autosubst2.unscoped]
Subst3 [in DCOIOmega.Autosubst2.unscoped]
Subst4 [in DCOIOmega.Autosubst2.unscoped]
Subst5 [in DCOIOmega.Autosubst2.unscoped]
syntax_sig.Up_tm [in DCOIOmega.Autosubst2.syntax]

V

Var [in DCOIOmega.Autosubst2.unscoped]

---

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

(994 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

(38 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

(77 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

(19 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

(446 entries)

Axiom 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

(15 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

(207 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

(12 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

(30 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

(5 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

(1 entry)

Abbreviation 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)

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

(130 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

(12 entries)

Generated by coqdoc and improved with CoqdocJS