Global Index

H

J

K

X

Y

Z

_

(1572 entries)

Notation Index

A

B

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

T

V

W

X

Y

Z

_

(64 entries)

Module Index

B

D

F

G

H

J

K

L

M

N

O

P

Q

T

V

W

X

Y

Z

_

other

(12 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1 entry)

Library Index

D

H

I

J

K

L

N

O

Q

V

W

X

Y

Z

_

other

(34 entries)

Lemma Index

B

H

J

K

L

Q

X

Y

Z

_

other

(523 entries)

Constructor Index

B

D

F

G

H

J

K

L

U

X

Y

Z

_

other

(479 entries)

Axiom Index

A

B

D

E

F

G

H

I

J

K

L

M

N

O

Q

R

S

T

U

V

W

X

Y

Z

_

other

(2 entries)

Inductive Index

A

B

D

F

H

I

J

K

L

O

U

X

Y

Z

_

other

(59 entries)

Projection Index

B

D

E

F

G

H

J

K

L

M

N

O

P

Q

T

U

V

W

X

Y

Z

_

other

(18 entries)

Section Index

B

C

D

E

F

G

H

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(3 entries)

Instance Index

A

B

D

E

G

H

J

K

L

M

N

O

P

Q

T

U

V

W

X

Y

Z

_

other

(29 entries)

Abbreviation Index

A

B

E

F

G

H

I

J

K

L

N

O

P

Q

R

U

V

W

X

Y

Z

_

other

(10 entries)

Definition Index

H

J

K

X

Y

Z

_

other

(320 entries)

Record Index

A

B

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

U

W

X

Y

Z

_

other

(18 entries)

Global Index

A

Admissible [section, in GhostTT.Admissible]
Admissible [library]
Allfv [module, in GhostTT.autosubst.GAST]
Allfv [module, in GhostTT.autosubst.CCAST]
Allfv.allfvImpl_term [definition, in GhostTT.autosubst.GAST]
Allfv.allfvImpl_cterm [definition, in GhostTT.autosubst.CCAST]
Allfv.allfvRenL_term [definition, in GhostTT.autosubst.GAST]
Allfv.allfvRenL_cterm [definition, in GhostTT.autosubst.CCAST]
Allfv.allfvRenR_term [definition, in GhostTT.autosubst.GAST]
Allfv.allfvRenR_cterm [definition, in GhostTT.autosubst.CCAST]
Allfv.allfvTriv_term [definition, in GhostTT.autosubst.GAST]
Allfv.allfvTriv_cterm [definition, in GhostTT.autosubst.CCAST]
Allfv.allfv_term [definition, in GhostTT.autosubst.GAST]
Allfv.allfv_cterm [definition, in GhostTT.autosubst.CCAST]
Allfv.upAllfvImpl_term_term [lemma, in GhostTT.autosubst.GAST]
Allfv.upAllfvImpl_cterm_cterm [lemma, in GhostTT.autosubst.CCAST]
Allfv.upAllfvRenL_term_term [lemma, in GhostTT.autosubst.GAST]
Allfv.upAllfvRenL_cterm_cterm [lemma, in GhostTT.autosubst.CCAST]
Allfv.upAllfvRenR_term_term [lemma, in GhostTT.autosubst.GAST]
Allfv.upAllfvRenR_cterm_cterm [lemma, in GhostTT.autosubst.CCAST]
Allfv.upAllfvTriv_term_term [lemma, in GhostTT.autosubst.GAST]
Allfv.upAllfvTriv_cterm_cterm [lemma, in GhostTT.autosubst.CCAST]
Allfv.upAllfv_term_term [lemma, in GhostTT.autosubst.GAST]
Allfv.upAllfv_cterm_cterm [lemma, in GhostTT.autosubst.CCAST]
Any [constructor, in GhostTT.BasicAST]
ap [definition, in GhostTT.autosubst.unscoped]
apc [definition, in GhostTT.autosubst.unscoped]
apply_subst_sound [lemma, in GhostTT.autosubst.CCAST_rasimpl]
apply_subst [definition, in GhostTT.autosubst.CCAST_rasimpl]
apply_ren_sound [lemma, in GhostTT.autosubst.RAsimpl]
apply_ren [definition, in GhostTT.autosubst.RAsimpl]
apply_subst_sound [lemma, in GhostTT.autosubst.GAST_rasimpl]
apply_subst [definition, in GhostTT.autosubst.GAST_rasimpl]
Assumptions [library]
autosubst_simpl_cstyping [lemma, in GhostTT.CCMetaTheory]
autosubst_simpl_crtyping [lemma, in GhostTT.CCMetaTheory]
autosubst_simpl_csscoping [lemma, in GhostTT.CCMetaTheory]
autosubst_simpl_crscoping [lemma, in GhostTT.CCMetaTheory]
autosubst_simpl_cterm_subst [lemma, in GhostTT.autosubst.CCAST_rasimpl]
autosubst_simpl_cterm_ren [lemma, in GhostTT.autosubst.CCAST_rasimpl]
autosubst_simpl_csubst [projection, in GhostTT.autosubst.CCAST_rasimpl]
autosubst_simpl_cterm [projection, in GhostTT.autosubst.CCAST_rasimpl]
autosubst_simpl_ren [projection, in GhostTT.autosubst.RAsimpl]
autosubst_simpl_term_subst [lemma, in GhostTT.autosubst.GAST_rasimpl]
autosubst_simpl_term_ren [lemma, in GhostTT.autosubst.GAST_rasimpl]
autosubst_simpl_csubst [projection, in GhostTT.autosubst.GAST_rasimpl]
autosubst_simpl_term [projection, in GhostTT.autosubst.GAST_rasimpl]
autosubst_simpl_styping [lemma, in GhostTT.BasicMetaTheory]
autosubst_simpl_rtyping [lemma, in GhostTT.BasicMetaTheory]
autosubst_simpl_sscoping [lemma, in GhostTT.BasicMetaTheory]
autosubst_simpl_rscoping [lemma, in GhostTT.BasicMetaTheory]

B

BasicAST [library]
BasicMetaTheory [library]
beq [definition, in GhostTT.FreeTheorem]

C

capps [definition, in GhostTT.CTyping]
CastRemoval [library]
castrm [definition, in GhostTT.CastRemoval]
castrm_subst [lemma, in GhostTT.BasicMetaTheory]
castrm_ren [lemma, in GhostTT.BasicMetaTheory]
CCAST [library]
CCAST_rasimpl [library]
CCMetaTheory [library]
ccmeta_conv [lemma, in GhostTT.CCMetaTheory]
ccmeta_refl [lemma, in GhostTT.Erasure]
ccong_pmPi [lemma, in GhostTT.Param]
ccong_pmifK [lemma, in GhostTT.Param]
ccong_pmif [lemma, in GhostTT.Param]
ccong_perif [lemma, in GhostTT.Param]
ccong_rpm_lift [lemma, in GhostTT.Param]
ccong_epm_lift [lemma, in GhostTT.Param]
ccong_plam [lemma, in GhostTT.Param]
ccong_pPi [lemma, in GhostTT.Param]
ccong_pvec_elimP [constructor, in GhostTT.CTyping]
ccong_pvec_elimG [constructor, in GhostTT.CTyping]
ccong_pvec_elim [constructor, in GhostTT.CTyping]
ccong_pvcons [constructor, in GhostTT.CTyping]
ccong_pvnil [constructor, in GhostTT.CTyping]
ccong_pvec [constructor, in GhostTT.CTyping]
ccong_evec_elim [constructor, in GhostTT.CTyping]
ccong_evcons [constructor, in GhostTT.CTyping]
ccong_evnil [constructor, in GhostTT.CTyping]
ccong_evec [constructor, in GhostTT.CTyping]
ccong_pnat_elimP [constructor, in GhostTT.CTyping]
ccong_pnat_elim [constructor, in GhostTT.CTyping]
ccong_psucc [constructor, in GhostTT.CTyping]
ccong_enat_elim [constructor, in GhostTT.CTyping]
ccong_esucc [constructor, in GhostTT.CTyping]
ccong_pif [constructor, in GhostTT.CTyping]
ccong_eif [constructor, in GhostTT.CTyping]
ccong_tJ [constructor, in GhostTT.CTyping]
ccong_trefl [constructor, in GhostTT.CTyping]
ccong_teq [constructor, in GhostTT.CTyping]
ccong_squash [constructor, in GhostTT.CTyping]
ccong_Err [constructor, in GhostTT.CTyping]
ccong_El [constructor, in GhostTT.CTyping]
ccong_tyval [constructor, in GhostTT.CTyping]
ccong_bot_elim [constructor, in GhostTT.CTyping]
ccong_app [constructor, in GhostTT.CTyping]
ccong_clam [constructor, in GhostTT.CTyping]
ccong_Pi [constructor, in GhostTT.CTyping]
ccong_Prop [constructor, in GhostTT.CTyping]
ccontext [abbreviation, in GhostTT.ContextDecl]
cconv_close [lemma, in GhostTT.CCMetaTheory]
cconv_subst [lemma, in GhostTT.CCMetaTheory]
cconv_ren [lemma, in GhostTT.CCMetaTheory]
cconv_irr [constructor, in GhostTT.CTyping]
cconv_trans [constructor, in GhostTT.CTyping]
cconv_sym [constructor, in GhostTT.CTyping]
cconv_refl [constructor, in GhostTT.CTyping]
cconv_evec_elim_cons [constructor, in GhostTT.CTyping]
cconv_evec_elim_nil [constructor, in GhostTT.CTyping]
cconv_enat_elim_succ [constructor, in GhostTT.CTyping]
cconv_enat_elim_zero [constructor, in GhostTT.CTyping]
cconv_pif_false [constructor, in GhostTT.CTyping]
cconv_pif_true [constructor, in GhostTT.CTyping]
cconv_if_err [constructor, in GhostTT.CTyping]
cconv_if_false [constructor, in GhostTT.CTyping]
cconv_if_true [constructor, in GhostTT.CTyping]
cconv_J_refl [constructor, in GhostTT.CTyping]
cconv_Err_err [constructor, in GhostTT.CTyping]
cconv_El_err [constructor, in GhostTT.CTyping]
cconv_Err_val [constructor, in GhostTT.CTyping]
cconv_El_val [constructor, in GhostTT.CTyping]
cconv_beta [constructor, in GhostTT.CTyping]
cconv_ty_lift [lemma, in GhostTT.Erasure]
ccscoping [inductive, in GhostTT.CScoping]
ccscoping_sind [definition, in GhostTT.CScoping]
ccscoping_ind [definition, in GhostTT.CScoping]
ccxscoping [abbreviation, in GhostTT.CScoping]
cc_consistency [definition, in GhostTT.Model]
cdecl [abbreviation, in GhostTT.ContextDecl]
cDummy [definition, in GhostTT.Erasure]
close [definition, in GhostTT.CCMetaTheory]
cmeta_conv_trans_r [lemma, in GhostTT.CCMetaTheory]
cmeta_conv_trans_l [lemma, in GhostTT.CCMetaTheory]
cmeta_conv [lemma, in GhostTT.CCMetaTheory]
cmeta_ctx_conv [lemma, in GhostTT.Param]
cmode [inductive, in GhostTT.BasicAST]
cmode_sind [definition, in GhostTT.BasicAST]
cmode_rec [definition, in GhostTT.BasicAST]
cmode_ind [definition, in GhostTT.BasicAST]
cmode_rect [definition, in GhostTT.BasicAST]
CombineNotations [module, in GhostTT.autosubst.unscoped]
_ >> _ (fscope) [notation, in GhostTT.autosubst.unscoped]
_ .: _ (subst_scope) [notation, in GhostTT.autosubst.unscoped]
cong_bot_elim [constructor, in GhostTT.Typing]
cong_vec_elim [constructor, in GhostTT.Typing]
cong_vcons [constructor, in GhostTT.Typing]
cong_vnil [constructor, in GhostTT.Typing]
cong_vec [constructor, in GhostTT.Typing]
cong_nat_elim [constructor, in GhostTT.Typing]
cong_succ [constructor, in GhostTT.Typing]
cong_if [constructor, in GhostTT.Typing]
cong_gheq [constructor, in GhostTT.Typing]
cong_Reveal [constructor, in GhostTT.Typing]
cong_reveal [constructor, in GhostTT.Typing]
cong_hide [constructor, in GhostTT.Typing]
cong_Erased [constructor, in GhostTT.Typing]
cong_app [constructor, in GhostTT.Typing]
cong_lam [constructor, in GhostTT.Typing]
cong_Pi [constructor, in GhostTT.Typing]
cong_Prop [constructor, in GhostTT.Typing]
conservativity [lemma, in GhostTT.ElimReflection]
consistency [lemma, in GhostTT.ElimReflection]
constant_free_theorem [lemma, in GhostTT.FreeTheorem]
context [abbreviation, in GhostTT.ContextDecl]
ContextDecl [library]
conversion [inductive, in GhostTT.CTyping]
conversion [inductive, in GhostTT.Typing]
conversion_sind [definition, in GhostTT.CTyping]
conversion_ind [definition, in GhostTT.CTyping]
conversion_sind [definition, in GhostTT.Typing]
conversion_ind [definition, in GhostTT.Typing]
conv_to_rev [lemma, in GhostTT.Revival]
conv_upto [lemma, in GhostTT.Model]
conv_meta_refl [lemma, in GhostTT.Model]
conv_urm [lemma, in GhostTT.Model]
conv_subst [lemma, in GhostTT.BasicMetaTheory]
conv_ren [lemma, in GhostTT.BasicMetaTheory]
conv_md [lemma, in GhostTT.BasicMetaTheory]
conv_irr [constructor, in GhostTT.Typing]
conv_trans [constructor, in GhostTT.Typing]
conv_sym [constructor, in GhostTT.Typing]
conv_refl [constructor, in GhostTT.Typing]
conv_vec_elim_cons [constructor, in GhostTT.Typing]
conv_vec_elim_nil [constructor, in GhostTT.Typing]
conv_nat_elim_succ [constructor, in GhostTT.Typing]
conv_nat_elim_zero [constructor, in GhostTT.Typing]
conv_if_false [constructor, in GhostTT.Typing]
conv_if_true [constructor, in GhostTT.Typing]
conv_beta [constructor, in GhostTT.Typing]
Core [module, in GhostTT.autosubst.GAST]
Core [module, in GhostTT.autosubst.CCAST]
core [library]
Core.app [constructor, in GhostTT.autosubst.GAST]
Core.bool_err [constructor, in GhostTT.autosubst.CCAST]
Core.bot [constructor, in GhostTT.autosubst.GAST]
Core.bot_elim [constructor, in GhostTT.autosubst.GAST]
Core.capp [constructor, in GhostTT.autosubst.CCAST]
Core.cbot [constructor, in GhostTT.autosubst.CCAST]
Core.cbot_elim [constructor, in GhostTT.autosubst.CCAST]
Core.cEl [constructor, in GhostTT.autosubst.CCAST]
Core.cErr [constructor, in GhostTT.autosubst.CCAST]
Core.clam [constructor, in GhostTT.autosubst.CCAST]
Core.compRenRen_term [definition, in GhostTT.autosubst.GAST]
Core.compRenRen_cterm [definition, in GhostTT.autosubst.CCAST]
Core.compRenSubst_term [definition, in GhostTT.autosubst.GAST]
Core.compRenSubst_cterm [definition, in GhostTT.autosubst.CCAST]
Core.compSubstRen_term [definition, in GhostTT.autosubst.GAST]
Core.compSubstRen_cterm [definition, in GhostTT.autosubst.CCAST]
Core.compSubstSubst_term [definition, in GhostTT.autosubst.GAST]
Core.compSubstSubst_cterm [definition, in GhostTT.autosubst.CCAST]
Core.congr_bot_elim [lemma, in GhostTT.autosubst.GAST]
Core.congr_bot [lemma, in GhostTT.autosubst.GAST]
Core.congr_tvec_elim [lemma, in GhostTT.autosubst.GAST]
Core.congr_tvcons [lemma, in GhostTT.autosubst.GAST]
Core.congr_tvnil [lemma, in GhostTT.autosubst.GAST]
Core.congr_tvec [lemma, in GhostTT.autosubst.GAST]
Core.congr_tnat_elim [lemma, in GhostTT.autosubst.GAST]
Core.congr_tsucc [lemma, in GhostTT.autosubst.GAST]
Core.congr_tzero [lemma, in GhostTT.autosubst.GAST]
Core.congr_tnat [lemma, in GhostTT.autosubst.GAST]
Core.congr_tif [lemma, in GhostTT.autosubst.GAST]
Core.congr_tfalse [lemma, in GhostTT.autosubst.GAST]
Core.congr_ttrue [lemma, in GhostTT.autosubst.GAST]
Core.congr_tbool [lemma, in GhostTT.autosubst.GAST]
Core.congr_ghcast [lemma, in GhostTT.autosubst.GAST]
Core.congr_ghrefl [lemma, in GhostTT.autosubst.GAST]
Core.congr_gheq [lemma, in GhostTT.autosubst.GAST]
Core.congr_fromRev [lemma, in GhostTT.autosubst.GAST]
Core.congr_toRev [lemma, in GhostTT.autosubst.GAST]
Core.congr_Reveal [lemma, in GhostTT.autosubst.GAST]
Core.congr_reveal [lemma, in GhostTT.autosubst.GAST]
Core.congr_hide [lemma, in GhostTT.autosubst.GAST]
Core.congr_Erased [lemma, in GhostTT.autosubst.GAST]
Core.congr_app [lemma, in GhostTT.autosubst.GAST]
Core.congr_lam [lemma, in GhostTT.autosubst.GAST]
Core.congr_Pi [lemma, in GhostTT.autosubst.GAST]
Core.congr_Sort [lemma, in GhostTT.autosubst.GAST]
Core.congr_pvec_elimP [lemma, in GhostTT.autosubst.CCAST]
Core.congr_pvec_elimG [lemma, in GhostTT.autosubst.CCAST]
Core.congr_pvec_elim [lemma, in GhostTT.autosubst.CCAST]
Core.congr_pvcons [lemma, in GhostTT.autosubst.CCAST]
Core.congr_pvnil [lemma, in GhostTT.autosubst.CCAST]
Core.congr_pvec [lemma, in GhostTT.autosubst.CCAST]
Core.congr_evec_elim [lemma, in GhostTT.autosubst.CCAST]
Core.congr_evcons [lemma, in GhostTT.autosubst.CCAST]
Core.congr_evnil [lemma, in GhostTT.autosubst.CCAST]
Core.congr_evec [lemma, in GhostTT.autosubst.CCAST]
Core.congr_pnat_elimP [lemma, in GhostTT.autosubst.CCAST]
Core.congr_pnat_elim [lemma, in GhostTT.autosubst.CCAST]
Core.congr_psucc [lemma, in GhostTT.autosubst.CCAST]
Core.congr_pzero [lemma, in GhostTT.autosubst.CCAST]
Core.congr_pnat [lemma, in GhostTT.autosubst.CCAST]
Core.congr_enat_elim [lemma, in GhostTT.autosubst.CCAST]
Core.congr_esucc [lemma, in GhostTT.autosubst.CCAST]
Core.congr_ezero [lemma, in GhostTT.autosubst.CCAST]
Core.congr_enat [lemma, in GhostTT.autosubst.CCAST]
Core.congr_pif [lemma, in GhostTT.autosubst.CCAST]
Core.congr_pfalse [lemma, in GhostTT.autosubst.CCAST]
Core.congr_ptrue [lemma, in GhostTT.autosubst.CCAST]
Core.congr_pbool [lemma, in GhostTT.autosubst.CCAST]
Core.congr_eif [lemma, in GhostTT.autosubst.CCAST]
Core.congr_bool_err [lemma, in GhostTT.autosubst.CCAST]
Core.congr_efalse [lemma, in GhostTT.autosubst.CCAST]
Core.congr_etrue [lemma, in GhostTT.autosubst.CCAST]
Core.congr_ebool [lemma, in GhostTT.autosubst.CCAST]
Core.congr_tJ [lemma, in GhostTT.autosubst.CCAST]
Core.congr_trefl [lemma, in GhostTT.autosubst.CCAST]
Core.congr_teq [lemma, in GhostTT.autosubst.CCAST]
Core.congr_sq_elim [lemma, in GhostTT.autosubst.CCAST]
Core.congr_sq [lemma, in GhostTT.autosubst.CCAST]
Core.congr_squash [lemma, in GhostTT.autosubst.CCAST]
Core.congr_cErr [lemma, in GhostTT.autosubst.CCAST]
Core.congr_cEl [lemma, in GhostTT.autosubst.CCAST]
Core.congr_ctyerr [lemma, in GhostTT.autosubst.CCAST]
Core.congr_ctyval [lemma, in GhostTT.autosubst.CCAST]
Core.congr_cty [lemma, in GhostTT.autosubst.CCAST]
Core.congr_cbot_elim [lemma, in GhostTT.autosubst.CCAST]
Core.congr_cbot [lemma, in GhostTT.autosubst.CCAST]
Core.congr_cstar [lemma, in GhostTT.autosubst.CCAST]
Core.congr_ctop [lemma, in GhostTT.autosubst.CCAST]
Core.congr_ctt [lemma, in GhostTT.autosubst.CCAST]
Core.congr_cunit [lemma, in GhostTT.autosubst.CCAST]
Core.congr_capp [lemma, in GhostTT.autosubst.CCAST]
Core.congr_clam [lemma, in GhostTT.autosubst.CCAST]
Core.congr_cPi [lemma, in GhostTT.autosubst.CCAST]
Core.congr_cSort [lemma, in GhostTT.autosubst.CCAST]
Core.cPi [constructor, in GhostTT.autosubst.CCAST]
Core.cSort [constructor, in GhostTT.autosubst.CCAST]
Core.cstar [constructor, in GhostTT.autosubst.CCAST]
Core.cterm [inductive, in GhostTT.autosubst.CCAST]
Core.cterm_sind [definition, in GhostTT.autosubst.CCAST]
Core.cterm_rec [definition, in GhostTT.autosubst.CCAST]
Core.cterm_ind [definition, in GhostTT.autosubst.CCAST]
Core.cterm_rect [definition, in GhostTT.autosubst.CCAST]
Core.ctop [constructor, in GhostTT.autosubst.CCAST]
Core.ctt [constructor, in GhostTT.autosubst.CCAST]
Core.cty [constructor, in GhostTT.autosubst.CCAST]
Core.ctyerr [constructor, in GhostTT.autosubst.CCAST]
Core.ctyval [constructor, in GhostTT.autosubst.CCAST]
Core.cunit [constructor, in GhostTT.autosubst.CCAST]
Core.cvar [constructor, in GhostTT.autosubst.CCAST]
Core.ebool [constructor, in GhostTT.autosubst.CCAST]
Core.efalse [constructor, in GhostTT.autosubst.CCAST]
Core.eif [constructor, in GhostTT.autosubst.CCAST]
Core.enat [constructor, in GhostTT.autosubst.CCAST]
Core.enat_elim [constructor, in GhostTT.autosubst.CCAST]
Core.Erased [constructor, in GhostTT.autosubst.GAST]
Core.esucc [constructor, in GhostTT.autosubst.CCAST]
Core.etrue [constructor, in GhostTT.autosubst.CCAST]
Core.evcons [constructor, in GhostTT.autosubst.CCAST]
Core.evec [constructor, in GhostTT.autosubst.CCAST]
Core.evec_elim [constructor, in GhostTT.autosubst.CCAST]
Core.evnil [constructor, in GhostTT.autosubst.CCAST]
Core.extRen_term [definition, in GhostTT.autosubst.GAST]
Core.extRen_cterm [definition, in GhostTT.autosubst.CCAST]
Core.ext_term [definition, in GhostTT.autosubst.GAST]
Core.ext_cterm [definition, in GhostTT.autosubst.CCAST]
Core.ezero [constructor, in GhostTT.autosubst.CCAST]
Core.fromRev [constructor, in GhostTT.autosubst.GAST]
Core.ghcast [constructor, in GhostTT.autosubst.GAST]
Core.gheq [constructor, in GhostTT.autosubst.GAST]
Core.ghrefl [constructor, in GhostTT.autosubst.GAST]
Core.hide [constructor, in GhostTT.autosubst.GAST]
Core.idSubst_term [definition, in GhostTT.autosubst.GAST]
Core.idSubst_cterm [definition, in GhostTT.autosubst.CCAST]
Core.instId'_term_pointwise [lemma, in GhostTT.autosubst.GAST]
Core.instId'_term [lemma, in GhostTT.autosubst.GAST]
Core.instId'_cterm_pointwise [lemma, in GhostTT.autosubst.CCAST]
Core.instId'_cterm [lemma, in GhostTT.autosubst.CCAST]
Core.lam [constructor, in GhostTT.autosubst.GAST]
Core.pbool [constructor, in GhostTT.autosubst.CCAST]
Core.pfalse [constructor, in GhostTT.autosubst.CCAST]
Core.Pi [constructor, in GhostTT.autosubst.GAST]
Core.pif [constructor, in GhostTT.autosubst.CCAST]
Core.pnat [constructor, in GhostTT.autosubst.CCAST]
Core.pnat_elimP [constructor, in GhostTT.autosubst.CCAST]
Core.pnat_elim [constructor, in GhostTT.autosubst.CCAST]
Core.psucc [constructor, in GhostTT.autosubst.CCAST]
Core.ptrue [constructor, in GhostTT.autosubst.CCAST]
Core.pvcons [constructor, in GhostTT.autosubst.CCAST]
Core.pvec [constructor, in GhostTT.autosubst.CCAST]
Core.pvec_elimP [constructor, in GhostTT.autosubst.CCAST]
Core.pvec_elimG [constructor, in GhostTT.autosubst.CCAST]
Core.pvec_elim [constructor, in GhostTT.autosubst.CCAST]
Core.pvnil [constructor, in GhostTT.autosubst.CCAST]
Core.pzero [constructor, in GhostTT.autosubst.CCAST]
Core.renRen_term [lemma, in GhostTT.autosubst.GAST]
Core.renRen_cterm [lemma, in GhostTT.autosubst.CCAST]
Core.renRen'_term_pointwise [lemma, in GhostTT.autosubst.GAST]
Core.renRen'_cterm_pointwise [lemma, in GhostTT.autosubst.CCAST]
Core.renSubst_term_pointwise [lemma, in GhostTT.autosubst.GAST]
Core.renSubst_term [lemma, in GhostTT.autosubst.GAST]
Core.renSubst_cterm_pointwise [lemma, in GhostTT.autosubst.CCAST]
Core.renSubst_cterm [lemma, in GhostTT.autosubst.CCAST]
Core.ren_term_morphism2 [instance, in GhostTT.autosubst.GAST]
Core.ren_term_morphism [instance, in GhostTT.autosubst.GAST]
Core.Ren_term [instance, in GhostTT.autosubst.GAST]
Core.ren_term [definition, in GhostTT.autosubst.GAST]
Core.ren_cterm_morphism2 [instance, in GhostTT.autosubst.CCAST]
Core.ren_cterm_morphism [instance, in GhostTT.autosubst.CCAST]
Core.Ren_cterm [instance, in GhostTT.autosubst.CCAST]
Core.ren_cterm [definition, in GhostTT.autosubst.CCAST]
Core.Reveal [constructor, in GhostTT.autosubst.GAST]
Core.reveal [constructor, in GhostTT.autosubst.GAST]
Core.rinstId'_term_pointwise [lemma, in GhostTT.autosubst.GAST]
Core.rinstId'_term [lemma, in GhostTT.autosubst.GAST]
Core.rinstId'_cterm_pointwise [lemma, in GhostTT.autosubst.CCAST]
Core.rinstId'_cterm [lemma, in GhostTT.autosubst.CCAST]
Core.rinstInst_up_term_term [lemma, in GhostTT.autosubst.GAST]
Core.rinstInst_up_cterm_cterm [lemma, in GhostTT.autosubst.CCAST]
Core.rinstInst'_term_pointwise [lemma, in GhostTT.autosubst.GAST]
Core.rinstInst'_term [lemma, in GhostTT.autosubst.GAST]
Core.rinstInst'_cterm_pointwise [lemma, in GhostTT.autosubst.CCAST]
Core.rinstInst'_cterm [lemma, in GhostTT.autosubst.CCAST]
Core.rinst_inst_term [definition, in GhostTT.autosubst.GAST]
Core.rinst_inst_cterm [definition, in GhostTT.autosubst.CCAST]
Core.Sort [constructor, in GhostTT.autosubst.GAST]
Core.sq [constructor, in GhostTT.autosubst.CCAST]
Core.squash [constructor, in GhostTT.autosubst.CCAST]
Core.sq_elim [constructor, in GhostTT.autosubst.CCAST]
Core.substRen_term_pointwise [lemma, in GhostTT.autosubst.GAST]
Core.substRen_term [lemma, in GhostTT.autosubst.GAST]
Core.substRen_cterm_pointwise [lemma, in GhostTT.autosubst.CCAST]
Core.substRen_cterm [lemma, in GhostTT.autosubst.CCAST]
Core.substSubst_term_pointwise [lemma, in GhostTT.autosubst.GAST]
Core.substSubst_term [lemma, in GhostTT.autosubst.GAST]
Core.substSubst_cterm_pointwise [lemma, in GhostTT.autosubst.CCAST]
Core.substSubst_cterm [lemma, in GhostTT.autosubst.CCAST]
Core.subst_term_morphism2 [instance, in GhostTT.autosubst.GAST]
Core.subst_term_morphism [instance, in GhostTT.autosubst.GAST]
Core.Subst_term [instance, in GhostTT.autosubst.GAST]
Core.subst_term [definition, in GhostTT.autosubst.GAST]
Core.subst_cterm_morphism2 [instance, in GhostTT.autosubst.CCAST]
Core.subst_cterm_morphism [instance, in GhostTT.autosubst.CCAST]
Core.Subst_cterm [instance, in GhostTT.autosubst.CCAST]
Core.subst_cterm [definition, in GhostTT.autosubst.CCAST]
Core.tbool [constructor, in GhostTT.autosubst.GAST]
Core.teq [constructor, in GhostTT.autosubst.CCAST]
Core.term [inductive, in GhostTT.autosubst.GAST]
Core.term_sind [definition, in GhostTT.autosubst.GAST]
Core.term_rec [definition, in GhostTT.autosubst.GAST]
Core.term_ind [definition, in GhostTT.autosubst.GAST]
Core.term_rect [definition, in GhostTT.autosubst.GAST]
Core.tfalse [constructor, in GhostTT.autosubst.GAST]
Core.tif [constructor, in GhostTT.autosubst.GAST]
Core.tJ [constructor, in GhostTT.autosubst.CCAST]
Core.tnat [constructor, in GhostTT.autosubst.GAST]
Core.tnat_elim [constructor, in GhostTT.autosubst.GAST]
Core.toRev [constructor, in GhostTT.autosubst.GAST]
Core.trefl [constructor, in GhostTT.autosubst.CCAST]
Core.tsucc [constructor, in GhostTT.autosubst.GAST]
Core.ttrue [constructor, in GhostTT.autosubst.GAST]
Core.tvcons [constructor, in GhostTT.autosubst.GAST]
Core.tvec [constructor, in GhostTT.autosubst.GAST]
Core.tvec_elim [constructor, in GhostTT.autosubst.GAST]
Core.tvnil [constructor, in GhostTT.autosubst.GAST]
Core.tzero [constructor, in GhostTT.autosubst.GAST]
Core.upExtRen_term_term [lemma, in GhostTT.autosubst.GAST]
Core.upExtRen_cterm_cterm [lemma, in GhostTT.autosubst.CCAST]
Core.upExt_term_term [lemma, in GhostTT.autosubst.GAST]
Core.upExt_cterm_cterm [lemma, in GhostTT.autosubst.CCAST]
Core.upId_term_term [lemma, in GhostTT.autosubst.GAST]
Core.upId_cterm_cterm [lemma, in GhostTT.autosubst.CCAST]
Core.upRen_term_term [lemma, in GhostTT.autosubst.GAST]
Core.upRen_cterm_cterm [lemma, in GhostTT.autosubst.CCAST]
Core.Up_term_term [instance, in GhostTT.autosubst.GAST]
Core.up_term [projection, in GhostTT.autosubst.GAST]
Core.Up_term [record, in GhostTT.autosubst.GAST]
Core.up_term [constructor, in GhostTT.autosubst.GAST]
Core.Up_term [inductive, in GhostTT.autosubst.GAST]
Core.up_subst_subst_term_term [lemma, in GhostTT.autosubst.GAST]
Core.up_subst_ren_term_term [lemma, in GhostTT.autosubst.GAST]
Core.up_ren_subst_term_term [lemma, in GhostTT.autosubst.GAST]
Core.up_ren_ren_term_term [lemma, in GhostTT.autosubst.GAST]
Core.up_term_term [lemma, in GhostTT.autosubst.GAST]
Core.Up_cterm_cterm [instance, in GhostTT.autosubst.CCAST]
Core.up_cterm [projection, in GhostTT.autosubst.CCAST]
Core.Up_cterm [record, in GhostTT.autosubst.CCAST]
Core.up_cterm [constructor, in GhostTT.autosubst.CCAST]
Core.Up_cterm [inductive, in GhostTT.autosubst.CCAST]
Core.up_subst_subst_cterm_cterm [lemma, in GhostTT.autosubst.CCAST]
Core.up_subst_ren_cterm_cterm [lemma, in GhostTT.autosubst.CCAST]
Core.up_ren_subst_cterm_cterm [lemma, in GhostTT.autosubst.CCAST]
Core.up_ren_ren_cterm_cterm [lemma, in GhostTT.autosubst.CCAST]
Core.up_cterm_cterm [lemma, in GhostTT.autosubst.CCAST]
Core.var [constructor, in GhostTT.autosubst.GAST]
Core.VarInstance_term [instance, in GhostTT.autosubst.GAST]
Core.VarInstance_cterm [instance, in GhostTT.autosubst.CCAST]
Core.varLRen'_term_pointwise [lemma, in GhostTT.autosubst.GAST]
Core.varLRen'_term [lemma, in GhostTT.autosubst.GAST]
Core.varLRen'_cterm_pointwise [lemma, in GhostTT.autosubst.CCAST]
Core.varLRen'_cterm [lemma, in GhostTT.autosubst.CCAST]
Core.varL'_term_pointwise [lemma, in GhostTT.autosubst.GAST]
Core.varL'_term [lemma, in GhostTT.autosubst.GAST]
Core.varL'_cterm_pointwise [lemma, in GhostTT.autosubst.CCAST]
Core.varL'_cterm [lemma, in GhostTT.autosubst.CCAST]
[ _ ] (fscope) [notation, in GhostTT.autosubst.GAST]
[ _ ] (fscope) [notation, in GhostTT.autosubst.CCAST]
⟨ _ ⟩ (fscope) [notation, in GhostTT.autosubst.GAST]
⟨ _ ⟩ (fscope) [notation, in GhostTT.autosubst.CCAST]
_ __term (subst_scope) [notation, in GhostTT.autosubst.GAST]
_ __term (subst_scope) [notation, in GhostTT.autosubst.GAST]
var (subst_scope) [notation, in GhostTT.autosubst.GAST]
_ ⟨ _ ⟩ (subst_scope) [notation, in GhostTT.autosubst.GAST]
↑__term (subst_scope) [notation, in GhostTT.autosubst.GAST]
↑__term (subst_scope) [notation, in GhostTT.autosubst.GAST]
_ [ _ ] (subst_scope) [notation, in GhostTT.autosubst.GAST]
_ __cterm (subst_scope) [notation, in GhostTT.autosubst.CCAST]
_ __cterm (subst_scope) [notation, in GhostTT.autosubst.CCAST]
var (subst_scope) [notation, in GhostTT.autosubst.CCAST]
_ ⟨ _ ⟩ (subst_scope) [notation, in GhostTT.autosubst.CCAST]
↑__cterm (subst_scope) [notation, in GhostTT.autosubst.CCAST]
↑__cterm (subst_scope) [notation, in GhostTT.autosubst.CCAST]
_ [ _ ] (subst_scope) [notation, in GhostTT.autosubst.CCAST]
cProp [constructor, in GhostTT.BasicAST]
crscoping [definition, in GhostTT.CCMetaTheory]
crscoping_sscoping [lemma, in GhostTT.CCMetaTheory]
crscoping_morphism [instance, in GhostTT.CCMetaTheory]
crscoping_shift_none [lemma, in GhostTT.CCMetaTheory]
crscoping_shift [lemma, in GhostTT.CCMetaTheory]
crscoping_plus [lemma, in GhostTT.CCMetaTheory]
crscoping_S [lemma, in GhostTT.CCMetaTheory]
crscoping_comp [lemma, in GhostTT.Revival]
crtyping [definition, in GhostTT.CCMetaTheory]
crtyping_typing [lemma, in GhostTT.CCMetaTheory]
crtyping_S [lemma, in GhostTT.CCMetaTheory]
crtyping_upren_none [lemma, in GhostTT.CCMetaTheory]
crtyping_shift [lemma, in GhostTT.CCMetaTheory]
crtyping_cscoping [lemma, in GhostTT.CCMetaTheory]
crtyping_morphism [instance, in GhostTT.CCMetaTheory]
crtyping_shift_eq [lemma, in GhostTT.Param]
crtyping_comp [lemma, in GhostTT.Erasure]
csc [definition, in GhostTT.ContextDecl]
cscope [abbreviation, in GhostTT.ContextDecl]
cscope_ignore [lemma, in GhostTT.CCMetaTheory]
cscope_close [lemma, in GhostTT.CCMetaTheory]
cscope_cons [constructor, in GhostTT.CCMetaTheory]
cscope_nil [constructor, in GhostTT.CCMetaTheory]
cscope_pvec_elimP [constructor, in GhostTT.CScoping]
cscope_pvec_elimG [constructor, in GhostTT.CScoping]
cscope_pvec_elim [constructor, in GhostTT.CScoping]
cscope_pvcons [constructor, in GhostTT.CScoping]
cscope_pvnil [constructor, in GhostTT.CScoping]
cscope_pvec [constructor, in GhostTT.CScoping]
cscope_evec_elim [constructor, in GhostTT.CScoping]
cscope_evcons [constructor, in GhostTT.CScoping]
cscope_evnil [constructor, in GhostTT.CScoping]
cscope_evec [constructor, in GhostTT.CScoping]
cscope_pnat_elimP [constructor, in GhostTT.CScoping]
cscope_pnat_elim [constructor, in GhostTT.CScoping]
cscope_psucc [constructor, in GhostTT.CScoping]
cscope_pzero [constructor, in GhostTT.CScoping]
cscope_pnat [constructor, in GhostTT.CScoping]
cscope_enat_elim [constructor, in GhostTT.CScoping]
cscope_esucc [constructor, in GhostTT.CScoping]
cscope_ezero [constructor, in GhostTT.CScoping]
cscope_enat [constructor, in GhostTT.CScoping]
cscope_pif [constructor, in GhostTT.CScoping]
cscope_pfalse [constructor, in GhostTT.CScoping]
cscope_ptrue [constructor, in GhostTT.CScoping]
cscope_pbool [constructor, in GhostTT.CScoping]
cscope_eif [constructor, in GhostTT.CScoping]
cscope_bool_err [constructor, in GhostTT.CScoping]
cscope_efalse [constructor, in GhostTT.CScoping]
cscope_etrue [constructor, in GhostTT.CScoping]
cscope_ebool [constructor, in GhostTT.CScoping]
cscope_tJ [constructor, in GhostTT.CScoping]
cscope_trefl [constructor, in GhostTT.CScoping]
cscope_teq [constructor, in GhostTT.CScoping]
cscope_sq_elim [constructor, in GhostTT.CScoping]
cscope_sq [constructor, in GhostTT.CScoping]
cscope_squash [constructor, in GhostTT.CScoping]
cscope_Err [constructor, in GhostTT.CScoping]
cscope_El [constructor, in GhostTT.CScoping]
cscope_tyerr [constructor, in GhostTT.CScoping]
cscope_tyval [constructor, in GhostTT.CScoping]
cscope_ty [constructor, in GhostTT.CScoping]
cscope_bot_elim [constructor, in GhostTT.CScoping]
cscope_bot [constructor, in GhostTT.CScoping]
cscope_star [constructor, in GhostTT.CScoping]
cscope_top [constructor, in GhostTT.CScoping]
cscope_tt [constructor, in GhostTT.CScoping]
cscope_unit [constructor, in GhostTT.CScoping]
cscope_app [constructor, in GhostTT.CScoping]
cscope_lam [constructor, in GhostTT.CScoping]
cscope_pi [constructor, in GhostTT.CScoping]
cscope_sort [constructor, in GhostTT.CScoping]
cscope_var [constructor, in GhostTT.CScoping]
cscope_ty_lift [lemma, in GhostTT.Erasure]
cscoping [abbreviation, in GhostTT.Scoping]
CScoping [library]
cscoping_subst [lemma, in GhostTT.CCMetaTheory]
cscoping_ren [lemma, in GhostTT.CCMetaTheory]
csc_param_ctx [lemma, in GhostTT.Param]
csscoping [inductive, in GhostTT.CCMetaTheory]
csscoping_nones [lemma, in GhostTT.CCMetaTheory]
csscoping_one_none [lemma, in GhostTT.CCMetaTheory]
csscoping_one [lemma, in GhostTT.CCMetaTheory]
csscoping_ids [lemma, in GhostTT.CCMetaTheory]
csscoping_morphism [instance, in GhostTT.CCMetaTheory]
csscoping_shift [lemma, in GhostTT.CCMetaTheory]
csscoping_weak [lemma, in GhostTT.CCMetaTheory]
csscoping_sind [definition, in GhostTT.CCMetaTheory]
csscoping_ind [definition, in GhostTT.CCMetaTheory]
cstyping [inductive, in GhostTT.CCMetaTheory]
cstyping_nones [lemma, in GhostTT.CCMetaTheory]
cstyping_one_none [lemma, in GhostTT.CCMetaTheory]
cstyping_one [lemma, in GhostTT.CCMetaTheory]
cstyping_ids [lemma, in GhostTT.CCMetaTheory]
cstyping_shift_none [lemma, in GhostTT.CCMetaTheory]
cstyping_shift [lemma, in GhostTT.CCMetaTheory]
cstyping_weak_none [lemma, in GhostTT.CCMetaTheory]
cstyping_weak [lemma, in GhostTT.CCMetaTheory]
cstyping_cscoping [lemma, in GhostTT.CCMetaTheory]
cstyping_sind [definition, in GhostTT.CCMetaTheory]
cstyping_ind [definition, in GhostTT.CCMetaTheory]
cstyping_shift_eq [lemma, in GhostTT.Param]
cst_ty [definition, in GhostTT.FreeTheorem]
CSubstSimplification [record, in GhostTT.autosubst.CCAST_rasimpl]
CTermSimplification [record, in GhostTT.autosubst.CCAST_rasimpl]
cType [constructor, in GhostTT.BasicAST]
ctype_ignore [lemma, in GhostTT.CCMetaTheory]
ctype_close [lemma, in GhostTT.CCMetaTheory]
ctype_cons [constructor, in GhostTT.CCMetaTheory]
ctype_nil [constructor, in GhostTT.CCMetaTheory]
ctype_cumul [constructor, in GhostTT.CTyping]
ctype_conv [constructor, in GhostTT.CTyping]
ctype_pvec_elimP [constructor, in GhostTT.CTyping]
ctype_pvec_elimG [constructor, in GhostTT.CTyping]
ctype_pvec_elim [constructor, in GhostTT.CTyping]
ctype_pvcons [constructor, in GhostTT.CTyping]
ctype_pvnil [constructor, in GhostTT.CTyping]
ctype_pvec [constructor, in GhostTT.CTyping]
ctype_evec_elim [constructor, in GhostTT.CTyping]
ctype_evcons [constructor, in GhostTT.CTyping]
ctype_evnil [constructor, in GhostTT.CTyping]
ctype_evec [constructor, in GhostTT.CTyping]
ctype_pnat_elimP [constructor, in GhostTT.CTyping]
ctype_pnat_elim [constructor, in GhostTT.CTyping]
ctype_psucc [constructor, in GhostTT.CTyping]
ctype_pzero [constructor, in GhostTT.CTyping]
ctype_pnat [constructor, in GhostTT.CTyping]
ctype_enat_elim [constructor, in GhostTT.CTyping]
ctype_esucc [constructor, in GhostTT.CTyping]
ctype_ezero [constructor, in GhostTT.CTyping]
ctype_enat [constructor, in GhostTT.CTyping]
ctype_pif [constructor, in GhostTT.CTyping]
ctype_pfalse [constructor, in GhostTT.CTyping]
ctype_ptrue [constructor, in GhostTT.CTyping]
ctype_pbool [constructor, in GhostTT.CTyping]
ctype_eif [constructor, in GhostTT.CTyping]
ctype_bool_err [constructor, in GhostTT.CTyping]
ctype_efalse [constructor, in GhostTT.CTyping]
ctype_etrue [constructor, in GhostTT.CTyping]
ctype_ebool [constructor, in GhostTT.CTyping]
ctype_tJ [constructor, in GhostTT.CTyping]
ctype_trefl [constructor, in GhostTT.CTyping]
ctype_teq [constructor, in GhostTT.CTyping]
ctype_sq_elim [constructor, in GhostTT.CTyping]
ctype_sq [constructor, in GhostTT.CTyping]
ctype_squash [constructor, in GhostTT.CTyping]
ctype_Err [constructor, in GhostTT.CTyping]
ctype_El [constructor, in GhostTT.CTyping]
ctype_tyerr [constructor, in GhostTT.CTyping]
ctype_tyval [constructor, in GhostTT.CTyping]
ctype_ty [constructor, in GhostTT.CTyping]
ctype_bot_elim [constructor, in GhostTT.CTyping]
ctype_bot [constructor, in GhostTT.CTyping]
ctype_star [constructor, in GhostTT.CTyping]
ctype_top [constructor, in GhostTT.CTyping]
ctype_tt [constructor, in GhostTT.CTyping]
ctype_unit [constructor, in GhostTT.CTyping]
ctype_app [constructor, in GhostTT.CTyping]
ctype_lam [constructor, in GhostTT.CTyping]
ctype_pi [constructor, in GhostTT.CTyping]
ctype_sort [constructor, in GhostTT.CTyping]
ctype_var [constructor, in GhostTT.CTyping]
ctype_ty_lift [lemma, in GhostTT.Erasure]
ctyping [inductive, in GhostTT.CTyping]
CTyping [library]
ctyping_subst [lemma, in GhostTT.CCMetaTheory]
ctyping_ren [lemma, in GhostTT.CCMetaTheory]
ctyping_sind [definition, in GhostTT.CTyping]
ctyping_ind [definition, in GhostTT.CTyping]
ctyval_inj [axiom, in GhostTT.Model]
cty_lift [definition, in GhostTT.Erasure]
cumax [definition, in GhostTT.CTyping]
cusup [definition, in GhostTT.CTyping]
cwf [inductive, in GhostTT.CTyping]
cwf_sind [definition, in GhostTT.CTyping]
cwf_ind [definition, in GhostTT.CTyping]
cwf_cons [constructor, in GhostTT.CTyping]
cwf_nil [constructor, in GhostTT.CTyping]

D

decl [abbreviation, in GhostTT.ContextDecl]
discr [definition, in GhostTT.Examples]
discr_nat [definition, in GhostTT.Examples]
discr_bool [definition, in GhostTT.Examples]
div2_vpar [lemma, in GhostTT.Param]
div2_vreg [lemma, in GhostTT.Param]
div2_SS [lemma, in GhostTT.Param]

E

El [definition, in GhostTT.TransNat]
elength [definition, in GhostTT.CTyping]
ElimReflection [library]
elim_ctx [lemma, in GhostTT.ElimReflection]
elim_reflection [lemma, in GhostTT.ElimReflection]
epm_lift_eq [lemma, in GhostTT.Param]
epm_lift [definition, in GhostTT.Param]
eq_subst_on_up [lemma, in GhostTT.CCMetaTheory]
eq_subst_on [definition, in GhostTT.CCMetaTheory]
erased_nat_discrP [definition, in GhostTT.Examples]
erase_S [definition, in GhostTT.TransNat]
erase_O [definition, in GhostTT.TransNat]
erase_nat [definition, in GhostTT.TransNat]
erase_typing_eq [lemma, in GhostTT.Param]
erase_conv_eq [lemma, in GhostTT.Param]
erase_scoping_eq [lemma, in GhostTT.Param]
erase_rev_subst [lemma, in GhostTT.Revival]
erase_context [lemma, in GhostTT.Erasure]
erase_typing [lemma, in GhostTT.Erasure]
erase_typing_Err [lemma, in GhostTT.Erasure]
erase_typing_El [lemma, in GhostTT.Erasure]
erase_castrm_conv [lemma, in GhostTT.Erasure]
erase_castrm [lemma, in GhostTT.Erasure]
erase_conv [lemma, in GhostTT.Erasure]
erase_subst [lemma, in GhostTT.Erasure]
erase_ren [lemma, in GhostTT.Erasure]
erase_scoping [lemma, in GhostTT.Erasure]
erase_ctx_var [lemma, in GhostTT.Erasure]
erase_sc_var [lemma, in GhostTT.Erasure]
erase_irr [lemma, in GhostTT.Erasure]
erase_sc [definition, in GhostTT.Erasure]
erase_ctx [definition, in GhostTT.Erasure]
erase_term [definition, in GhostTT.Erasure]
Erasure [library]
Err [definition, in GhostTT.TransNat]
err [constructor, in GhostTT.FreeTheorem]
err_nat_elim_S [lemma, in GhostTT.TransNat]
err_nat_elim_O [lemma, in GhostTT.TransNat]
err_nat_elim [lemma, in GhostTT.TransNat]
err_nat_sind [definition, in GhostTT.TransNat]
err_nat_rec [definition, in GhostTT.TransNat]
err_nat_ind [definition, in GhostTT.TransNat]
err_nat_rect [definition, in GhostTT.TransNat]
err_S [constructor, in GhostTT.TransNat]
err_O [constructor, in GhostTT.TransNat]
err_nat [inductive, in GhostTT.TransNat]
err_length_eq [lemma, in GhostTT.TransVec]
err_length [definition, in GhostTT.TransVec]
err_vec_elim_vcons [lemma, in GhostTT.TransVec]
err_vec_elim_vnil [lemma, in GhostTT.TransVec]
err_vec_elim [lemma, in GhostTT.TransVec]
err_vec_sind [definition, in GhostTT.TransVec]
err_vec_rec [definition, in GhostTT.TransVec]
err_vec_ind [definition, in GhostTT.TransVec]
err_vec_rect [definition, in GhostTT.TransVec]
err_vcons [constructor, in GhostTT.TransVec]
err_vnil [constructor, in GhostTT.TransVec]
err_vec [inductive, in GhostTT.TransVec]
err_bool_sind [definition, in GhostTT.FreeTheorem]
err_bool_rec [definition, in GhostTT.FreeTheorem]
err_bool_ind [definition, in GhostTT.FreeTheorem]
err_bool_rect [definition, in GhostTT.FreeTheorem]
err_false [constructor, in GhostTT.FreeTheorem]
err_true [constructor, in GhostTT.FreeTheorem]
err_bool [inductive, in GhostTT.FreeTheorem]
ers_other [constructor, in GhostTT.autosubst.CCAST_rasimpl]
ers_ren_r [constructor, in GhostTT.autosubst.CCAST_rasimpl]
ers_cons_r [constructor, in GhostTT.autosubst.CCAST_rasimpl]
ers_rcomp_r [constructor, in GhostTT.autosubst.CCAST_rasimpl]
ers_compr_r [constructor, in GhostTT.autosubst.CCAST_rasimpl]
ers_comp_r [constructor, in GhostTT.autosubst.CCAST_rasimpl]
ers_id_r [constructor, in GhostTT.autosubst.CCAST_rasimpl]
ers_id_l [constructor, in GhostTT.autosubst.CCAST_rasimpl]
ers_other [constructor, in GhostTT.autosubst.GAST_rasimpl]
ers_ren_r [constructor, in GhostTT.autosubst.GAST_rasimpl]
ers_cons_r [constructor, in GhostTT.autosubst.GAST_rasimpl]
ers_rcomp_r [constructor, in GhostTT.autosubst.GAST_rasimpl]
ers_compr_r [constructor, in GhostTT.autosubst.GAST_rasimpl]
ers_comp_r [constructor, in GhostTT.autosubst.GAST_rasimpl]
ers_id_r [constructor, in GhostTT.autosubst.GAST_rasimpl]
ers_id_l [constructor, in GhostTT.autosubst.GAST_rasimpl]
er_bool_cst [definition, in GhostTT.FreeTheorem]
esr_other [constructor, in GhostTT.autosubst.CCAST_rasimpl]
esr_cons_shift [constructor, in GhostTT.autosubst.CCAST_rasimpl]
esr_ren_l [constructor, in GhostTT.autosubst.CCAST_rasimpl]
esr_cons_r [constructor, in GhostTT.autosubst.CCAST_rasimpl]
esr_comp_r [constructor, in GhostTT.autosubst.CCAST_rasimpl]
esr_id_r [constructor, in GhostTT.autosubst.CCAST_rasimpl]
esr_id_l [constructor, in GhostTT.autosubst.CCAST_rasimpl]
esr_other [constructor, in GhostTT.autosubst.GAST_rasimpl]
esr_cons_shift [constructor, in GhostTT.autosubst.GAST_rasimpl]
esr_ren_l [constructor, in GhostTT.autosubst.GAST_rasimpl]
esr_cons_r [constructor, in GhostTT.autosubst.GAST_rasimpl]
esr_comp_r [constructor, in GhostTT.autosubst.GAST_rasimpl]
esr_id_r [constructor, in GhostTT.autosubst.GAST_rasimpl]
esr_id_l [constructor, in GhostTT.autosubst.GAST_rasimpl]
es_other [constructor, in GhostTT.autosubst.CCAST_rasimpl]
es_ren_r [constructor, in GhostTT.autosubst.CCAST_rasimpl]
es_ren_l [constructor, in GhostTT.autosubst.CCAST_rasimpl]
es_cons_r [constructor, in GhostTT.autosubst.CCAST_rasimpl]
es_rcomp_r [constructor, in GhostTT.autosubst.CCAST_rasimpl]
es_compr_r [constructor, in GhostTT.autosubst.CCAST_rasimpl]
es_comp_r [constructor, in GhostTT.autosubst.CCAST_rasimpl]
es_id_r [constructor, in GhostTT.autosubst.CCAST_rasimpl]
es_id_l [constructor, in GhostTT.autosubst.CCAST_rasimpl]
es_other [constructor, in GhostTT.autosubst.GAST_rasimpl]
es_ren_r [constructor, in GhostTT.autosubst.GAST_rasimpl]
es_ren_l [constructor, in GhostTT.autosubst.GAST_rasimpl]
es_cons_r [constructor, in GhostTT.autosubst.GAST_rasimpl]
es_rcomp_r [constructor, in GhostTT.autosubst.GAST_rasimpl]
es_compr_r [constructor, in GhostTT.autosubst.GAST_rasimpl]
es_comp_r [constructor, in GhostTT.autosubst.GAST_rasimpl]
es_id_r [constructor, in GhostTT.autosubst.GAST_rasimpl]
es_id_l [constructor, in GhostTT.autosubst.GAST_rasimpl]
eval_cterm_sound [definition, in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_sound [definition, in GhostTT.autosubst.CCAST_rasimpl]
eval_cterm [definition, in GhostTT.autosubst.CCAST_rasimpl]
eval_subst [definition, in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_rcomp_c [definition, in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_rcomp_view_sind [definition, in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_rcomp_view_rec [definition, in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_rcomp_view_ind [definition, in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_rcomp_view_rect [definition, in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_rcomp_view [inductive, in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_compr_c [definition, in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_compr_view_sind [definition, in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_compr_view_rec [definition, in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_compr_view_ind [definition, in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_compr_view_rect [definition, in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_compr_view [inductive, in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_comp_c [definition, in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_comp_view_sind [definition, in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_comp_view_rec [definition, in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_comp_view_ind [definition, in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_comp_view_rect [definition, in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_comp_view [inductive, in GhostTT.autosubst.CCAST_rasimpl]
eval_ren_sound [lemma, in GhostTT.autosubst.RAsimpl]
eval_ren [definition, in GhostTT.autosubst.RAsimpl]
eval_ren_comp_c [definition, in GhostTT.autosubst.RAsimpl]
eval_ren_comp_view_sind [definition, in GhostTT.autosubst.RAsimpl]
eval_ren_comp_view_rec [definition, in GhostTT.autosubst.RAsimpl]
eval_ren_comp_view_ind [definition, in GhostTT.autosubst.RAsimpl]
eval_ren_comp_view_rect [definition, in GhostTT.autosubst.RAsimpl]
eval_ren_comp_other [constructor, in GhostTT.autosubst.RAsimpl]
eval_ren_cons_r [constructor, in GhostTT.autosubst.RAsimpl]
eval_ren_comp_r [constructor, in GhostTT.autosubst.RAsimpl]
eval_ren_cons_shift [constructor, in GhostTT.autosubst.RAsimpl]
eval_ren_id_r [constructor, in GhostTT.autosubst.RAsimpl]
eval_ren_id_l [constructor, in GhostTT.autosubst.RAsimpl]
eval_ren_comp_view [inductive, in GhostTT.autosubst.RAsimpl]
eval_term_sound [definition, in GhostTT.autosubst.GAST_rasimpl]
eval_subst_sound [definition, in GhostTT.autosubst.GAST_rasimpl]
eval_term [definition, in GhostTT.autosubst.GAST_rasimpl]
eval_subst [definition, in GhostTT.autosubst.GAST_rasimpl]
eval_subst_rcomp_c [definition, in GhostTT.autosubst.GAST_rasimpl]
eval_subst_rcomp_view_sind [definition, in GhostTT.autosubst.GAST_rasimpl]
eval_subst_rcomp_view_rec [definition, in GhostTT.autosubst.GAST_rasimpl]
eval_subst_rcomp_view_ind [definition, in GhostTT.autosubst.GAST_rasimpl]
eval_subst_rcomp_view_rect [definition, in GhostTT.autosubst.GAST_rasimpl]
eval_subst_rcomp_view [inductive, in GhostTT.autosubst.GAST_rasimpl]
eval_subst_compr_c [definition, in GhostTT.autosubst.GAST_rasimpl]
eval_subst_compr_view_sind [definition, in GhostTT.autosubst.GAST_rasimpl]
eval_subst_compr_view_rec [definition, in GhostTT.autosubst.GAST_rasimpl]
eval_subst_compr_view_ind [definition, in GhostTT.autosubst.GAST_rasimpl]
eval_subst_compr_view_rect [definition, in GhostTT.autosubst.GAST_rasimpl]
eval_subst_compr_view [inductive, in GhostTT.autosubst.GAST_rasimpl]
eval_subst_comp_c [definition, in GhostTT.autosubst.GAST_rasimpl]
eval_subst_comp_view_sind [definition, in GhostTT.autosubst.GAST_rasimpl]
eval_subst_comp_view_rec [definition, in GhostTT.autosubst.GAST_rasimpl]
eval_subst_comp_view_ind [definition, in GhostTT.autosubst.GAST_rasimpl]
eval_subst_comp_view_rect [definition, in GhostTT.autosubst.GAST_rasimpl]
eval_subst_comp_view [inductive, in GhostTT.autosubst.GAST_rasimpl]
Examples [library]
Extra [module, in GhostTT.autosubst.GAST]
Extra [module, in GhostTT.autosubst.CCAST]
ext_cterm_scoped [lemma, in GhostTT.CCMetaTheory]

F

FreeTheorem [library]
funcomp [definition, in GhostTT.autosubst.core]
funcomp_morphism2 [instance, in GhostTT.autosubst.core]
funcomp_morphism [instance, in GhostTT.autosubst.core]
funcomp_assoc [lemma, in GhostTT.autosubst.core]

G

GAST [library]
GAST_rasimpl [library]
ghv [definition, in GhostTT.Revival]
glength [definition, in GhostTT.Typing]
goal [lemma, in GhostTT.FreeTheorem]
grtt_consistency [definition, in GhostTT.ElimReflection]
grtyping [inductive, in GhostTT.RTyping]
grtyping_sind [definition, in GhostTT.RTyping]
grtyping_rec [definition, in GhostTT.RTyping]
grtyping_ind [definition, in GhostTT.RTyping]
grtyping_rect [definition, in GhostTT.RTyping]
gS [definition, in GhostTT.Typing]
gtt_consistency [definition, in GhostTT.Model]

I

id [definition, in GhostTT.autosubst.unscoped]
ids [projection, in GhostTT.autosubst.unscoped]
ids [constructor, in GhostTT.autosubst.unscoped]
idsRen [instance, in GhostTT.autosubst.unscoped]
ignore [definition, in GhostTT.CCMetaTheory]
inb [definition, in GhostTT.Util]
Inb [section, in GhostTT.Util]
inclb [definition, in GhostTT.Util]
inscope [definition, in GhostTT.CCMetaTheory]
interface [module, in GhostTT.autosubst.GAST]
interface [module, in GhostTT.autosubst.CCAST]
inv [definition, in GhostTT.FreeTheorem]
iscProp [definition, in GhostTT.CTyping]
isGhost [definition, in GhostTT.TermMode]
isGhost_eq [lemma, in GhostTT.TermMode]
isKind [definition, in GhostTT.TermMode]
isKind_eq [lemma, in GhostTT.TermMode]
isProp [definition, in GhostTT.TermMode]
isProp_eq [lemma, in GhostTT.TermMode]
isType [definition, in GhostTT.TermMode]
isType [definition, in GhostTT.CTyping]
isType_eq [lemma, in GhostTT.TermMode]
iszero [definition, in GhostTT.Examples]
is_qsubst_id [constructor, in GhostTT.autosubst.CCAST_rasimpl]
is_qsubst_ren [constructor, in GhostTT.autosubst.CCAST_rasimpl]
is_qren_id [constructor, in GhostTT.autosubst.RAsimpl]
is_qsubst_id [constructor, in GhostTT.autosubst.GAST_rasimpl]
is_qsubst_ren [constructor, in GhostTT.autosubst.GAST_rasimpl]

L

level [definition, in GhostTT.BasicAST]
list_comp [definition, in GhostTT.autosubst.core]
list_id [definition, in GhostTT.autosubst.core]
list_ext [definition, in GhostTT.autosubst.core]

M

mark [inductive, in GhostTT.BasicAST]
mark_sind [definition, in GhostTT.BasicAST]
mark_rec [definition, in GhostTT.BasicAST]
mark_ind [definition, in GhostTT.BasicAST]
mark_rect [definition, in GhostTT.BasicAST]
md [definition, in GhostTT.TermMode]
mdc [abbreviation, in GhostTT.TermMode]
mdmk [definition, in GhostTT.Erasure]
md_subst [lemma, in GhostTT.BasicMetaTheory]
md_ren [lemma, in GhostTT.BasicMetaTheory]
md_castrm [lemma, in GhostTT.BasicMetaTheory]
meta_ccscoping_conv [lemma, in GhostTT.Param]
meta_ctx_param_conv [lemma, in GhostTT.Param]
meta_ctx_conv_conv [lemma, in GhostTT.Param]
meta_conv_refl [lemma, in GhostTT.BasicMetaTheory]
meta_conv_trans_r [lemma, in GhostTT.BasicMetaTheory]
meta_conv_trans_l [lemma, in GhostTT.BasicMetaTheory]
meta_conv [lemma, in GhostTT.BasicMetaTheory]
mGhost [constructor, in GhostTT.BasicAST]
mKind [constructor, in GhostTT.BasicAST]
Mode [section, in GhostTT.TermMode]
mode [inductive, in GhostTT.BasicAST]
Model [library]
mode_eqb [definition, in GhostTT.TermMode]
mode_sind [definition, in GhostTT.BasicAST]
mode_rec [definition, in GhostTT.BasicAST]
mode_ind [definition, in GhostTT.BasicAST]
mode_rect [definition, in GhostTT.BasicAST]
mode_coherence [lemma, in GhostTT.Model]
Mode.dummy [variable, in GhostTT.TermMode]
mProp [constructor, in GhostTT.BasicAST]
mType [constructor, in GhostTT.BasicAST]

N

nat [inductive, in GhostTT.TransNat]
nat_err [constructor, in GhostTT.TransNat]
nat_sind [definition, in GhostTT.TransNat]
nat_rec [definition, in GhostTT.TransNat]
nat_ind [definition, in GhostTT.TransNat]
nat_rect [definition, in GhostTT.TransNat]
nones [definition, in GhostTT.CCMetaTheory]
not_qsubst_ren_id [constructor, in GhostTT.autosubst.CCAST_rasimpl]
not_qren_id [constructor, in GhostTT.autosubst.RAsimpl]
not_qsubst_ren_id [constructor, in GhostTT.autosubst.GAST_rasimpl]
nth_app_r [lemma, in GhostTT.Util]
nth_error_skipn [lemma, in GhostTT.Util]
nth_skipn [lemma, in GhostTT.Util]
nth_error_app_r [lemma, in GhostTT.Util]
nth_error_param_vpar [lemma, in GhostTT.Param]
nth_error_param_vreg [lemma, in GhostTT.Param]
nth_nth_error [lemma, in GhostTT.BasicMetaTheory]

O

O [constructor, in GhostTT.TransNat]
odd_vpar [lemma, in GhostTT.Param]
odd_vreg [lemma, in GhostTT.Param]
option_bind [definition, in GhostTT.Util]
option_comp [definition, in GhostTT.autosubst.core]
option_ext [definition, in GhostTT.autosubst.core]
option_id [definition, in GhostTT.autosubst.core]
option_map [definition, in GhostTT.autosubst.core]

P

Param [library]
param_context [lemma, in GhostTT.Param]
param_pTypeGhost [lemma, in GhostTT.Param]
param_typing [lemma, in GhostTT.Param]
param_erase_typing_eq [lemma, in GhostTT.Param]
param_pKind_eq [lemma, in GhostTT.Param]
param_pKind [lemma, in GhostTT.Param]
param_pGhost_eq [lemma, in GhostTT.Param]
param_pGhost [lemma, in GhostTT.Param]
param_pType_eq [lemma, in GhostTT.Param]
param_pType [lemma, in GhostTT.Param]
param_pProp [lemma, in GhostTT.Param]
param_erase_err [lemma, in GhostTT.Param]
param_erase_ty [lemma, in GhostTT.Param]
param_erase_ty_tm [lemma, in GhostTT.Param]
param_revive_typing [lemma, in GhostTT.Param]
param_erase_typing [lemma, in GhostTT.Param]
param_ctx_vpar [lemma, in GhostTT.Param]
param_ctx_vreg [lemma, in GhostTT.Param]
param_castrm_conv [lemma, in GhostTT.Param]
param_castrm [lemma, in GhostTT.Param]
param_conv [lemma, in GhostTT.Param]
param_subst [lemma, in GhostTT.Param]
param_ren [lemma, in GhostTT.Param]
param_scoping [lemma, in GhostTT.Param]
param_sc [definition, in GhostTT.Param]
param_ctx [definition, in GhostTT.Param]
param_term [definition, in GhostTT.Param]
pbool_bool_err_inv [definition, in GhostTT.Param]
pcastP [definition, in GhostTT.Param]
pcastTG [definition, in GhostTT.Param]
perif [definition, in GhostTT.Param]
pi_inj [axiom, in GhostTT.Model]
pKind [definition, in GhostTT.Param]
plam [definition, in GhostTT.Param]
pmif [definition, in GhostTT.Param]
pmifK [definition, in GhostTT.Param]
pmPi [definition, in GhostTT.Param]
pmPiNP [definition, in GhostTT.Param]
pmPiP [definition, in GhostTT.Param]
pm_nat_elim_Prop [lemma, in GhostTT.TransNat]
pm_nat_elim [lemma, in GhostTT.TransNat]
pm_nat_sind [definition, in GhostTT.TransNat]
pm_S [constructor, in GhostTT.TransNat]
pm_O [constructor, in GhostTT.TransNat]
pm_nat [inductive, in GhostTT.TransNat]
pm_vec_elim_Prop [lemma, in GhostTT.TransVec]
pm_vec_elimG [lemma, in GhostTT.TransVec]
pm_vec_elim [lemma, in GhostTT.TransVec]
pm_vec_sind [definition, in GhostTT.TransVec]
pm_vcons [constructor, in GhostTT.TransVec]
pm_vnil [constructor, in GhostTT.TransVec]
pm_vec [inductive, in GhostTT.TransVec]
pm_bool_sind [definition, in GhostTT.FreeTheorem]
pm_false [constructor, in GhostTT.FreeTheorem]
pm_true [constructor, in GhostTT.FreeTheorem]
pm_bool [inductive, in GhostTT.FreeTheorem]
pointwise_forall [lemma, in GhostTT.autosubst.core]
Potential [library]
pPi [definition, in GhostTT.Param]
pPi_scoping [lemma, in GhostTT.Param]
pProp [definition, in GhostTT.Param]
pren [definition, in GhostTT.Param]
pren_plus [lemma, in GhostTT.Param]
pren_S_pw [lemma, in GhostTT.Param]
pren_S [lemma, in GhostTT.Param]
pren_rpm_lift [lemma, in GhostTT.Param]
pren_epm_lift [lemma, in GhostTT.Param]
pren_id [lemma, in GhostTT.Param]
pren_comp_S [lemma, in GhostTT.Param]
pren_SS [lemma, in GhostTT.Param]
pren_odd [lemma, in GhostTT.Param]
pren_even [lemma, in GhostTT.Param]
prod_comp [definition, in GhostTT.autosubst.core]
prod_ext [definition, in GhostTT.autosubst.core]
prod_id [definition, in GhostTT.autosubst.core]
prod_map [definition, in GhostTT.autosubst.core]
pscoping_revive [lemma, in GhostTT.Param]
pscoping_erase_err [lemma, in GhostTT.Param]
pscoping_erase_type [lemma, in GhostTT.Param]
pscoping_erase_term [lemma, in GhostTT.Param]
psubst [definition, in GhostTT.Param]
psubst_SS_id [lemma, in GhostTT.Param]
psubst_rpm_lift [lemma, in GhostTT.Param]
psubst_epm_lift [lemma, in GhostTT.Param]
psubst_SS' [lemma, in GhostTT.Param]
psubst_SS [lemma, in GhostTT.Param]
ptype [definition, in GhostTT.Param]
pType [definition, in GhostTT.Param]

Q

qatom [constructor, in GhostTT.autosubst.CCAST_rasimpl]
qatom [constructor, in GhostTT.autosubst.GAST_rasimpl]
qnat_atom [constructor, in GhostTT.autosubst.RAsimpl]
qren [constructor, in GhostTT.autosubst.CCAST_rasimpl]
qren [constructor, in GhostTT.autosubst.GAST_rasimpl]
qren_id_view_sind [definition, in GhostTT.autosubst.RAsimpl]
qren_id_view_rec [definition, in GhostTT.autosubst.RAsimpl]
qren_id_view_ind [definition, in GhostTT.autosubst.RAsimpl]
qren_id_view_rect [definition, in GhostTT.autosubst.RAsimpl]
qren_id_view [inductive, in GhostTT.autosubst.RAsimpl]
qren_shift [constructor, in GhostTT.autosubst.RAsimpl]
qren_id [constructor, in GhostTT.autosubst.RAsimpl]
qren_cons [constructor, in GhostTT.autosubst.RAsimpl]
qren_comp [constructor, in GhostTT.autosubst.RAsimpl]
qren_atom [constructor, in GhostTT.autosubst.RAsimpl]
qS [constructor, in GhostTT.autosubst.RAsimpl]
qsubst [constructor, in GhostTT.autosubst.CCAST_rasimpl]
qsubst [constructor, in GhostTT.autosubst.GAST_rasimpl]
qsubst_ren_id_view_sind [definition, in GhostTT.autosubst.CCAST_rasimpl]
qsubst_ren_id_view_rec [definition, in GhostTT.autosubst.CCAST_rasimpl]
qsubst_ren_id_view_ind [definition, in GhostTT.autosubst.CCAST_rasimpl]
qsubst_ren_id_view_rect [definition, in GhostTT.autosubst.CCAST_rasimpl]
qsubst_ren_id_view [inductive, in GhostTT.autosubst.CCAST_rasimpl]
qsubst_ren [constructor, in GhostTT.autosubst.CCAST_rasimpl]
qsubst_id [constructor, in GhostTT.autosubst.CCAST_rasimpl]
qsubst_cons [constructor, in GhostTT.autosubst.CCAST_rasimpl]
qsubst_rcomp [constructor, in GhostTT.autosubst.CCAST_rasimpl]
qsubst_compr [constructor, in GhostTT.autosubst.CCAST_rasimpl]
qsubst_comp [constructor, in GhostTT.autosubst.CCAST_rasimpl]
qsubst_atom [constructor, in GhostTT.autosubst.CCAST_rasimpl]
qsubst_ren_id_view_sind [definition, in GhostTT.autosubst.GAST_rasimpl]
qsubst_ren_id_view_rec [definition, in GhostTT.autosubst.GAST_rasimpl]
qsubst_ren_id_view_ind [definition, in GhostTT.autosubst.GAST_rasimpl]
qsubst_ren_id_view_rect [definition, in GhostTT.autosubst.GAST_rasimpl]
qsubst_ren_id_view [inductive, in GhostTT.autosubst.GAST_rasimpl]
qsubst_ren [constructor, in GhostTT.autosubst.GAST_rasimpl]
qsubst_id [constructor, in GhostTT.autosubst.GAST_rasimpl]
qsubst_cons [constructor, in GhostTT.autosubst.GAST_rasimpl]
qsubst_rcomp [constructor, in GhostTT.autosubst.GAST_rasimpl]
qsubst_compr [constructor, in GhostTT.autosubst.GAST_rasimpl]
qsubst_comp [constructor, in GhostTT.autosubst.GAST_rasimpl]
qsubst_atom [constructor, in GhostTT.autosubst.GAST_rasimpl]
quoted_cterm_sind [definition, in GhostTT.autosubst.CCAST_rasimpl]
quoted_cterm_rec [definition, in GhostTT.autosubst.CCAST_rasimpl]
quoted_cterm_ind [definition, in GhostTT.autosubst.CCAST_rasimpl]
quoted_cterm_rect [definition, in GhostTT.autosubst.CCAST_rasimpl]
quoted_subst_sind [definition, in GhostTT.autosubst.CCAST_rasimpl]
quoted_subst_rec [definition, in GhostTT.autosubst.CCAST_rasimpl]
quoted_subst_ind [definition, in GhostTT.autosubst.CCAST_rasimpl]
quoted_subst_rect [definition, in GhostTT.autosubst.CCAST_rasimpl]
quoted_cterm [inductive, in GhostTT.autosubst.CCAST_rasimpl]
quoted_subst [inductive, in GhostTT.autosubst.CCAST_rasimpl]
quoted_ren_sind [definition, in GhostTT.autosubst.RAsimpl]
quoted_ren_rec [definition, in GhostTT.autosubst.RAsimpl]
quoted_ren_ind [definition, in GhostTT.autosubst.RAsimpl]
quoted_ren_rect [definition, in GhostTT.autosubst.RAsimpl]
quoted_ren [inductive, in GhostTT.autosubst.RAsimpl]
quoted_nat_sind [definition, in GhostTT.autosubst.RAsimpl]
quoted_nat_rec [definition, in GhostTT.autosubst.RAsimpl]
quoted_nat_ind [definition, in GhostTT.autosubst.RAsimpl]
quoted_nat_rect [definition, in GhostTT.autosubst.RAsimpl]
quoted_nat [inductive, in GhostTT.autosubst.RAsimpl]
quoted_term_sind [definition, in GhostTT.autosubst.GAST_rasimpl]
quoted_term_rec [definition, in GhostTT.autosubst.GAST_rasimpl]
quoted_term_ind [definition, in GhostTT.autosubst.GAST_rasimpl]
quoted_term_rect [definition, in GhostTT.autosubst.GAST_rasimpl]
quoted_subst_sind [definition, in GhostTT.autosubst.GAST_rasimpl]
quoted_subst_rec [definition, in GhostTT.autosubst.GAST_rasimpl]
quoted_subst_ind [definition, in GhostTT.autosubst.GAST_rasimpl]
quoted_subst_rect [definition, in GhostTT.autosubst.GAST_rasimpl]
quoted_term [inductive, in GhostTT.autosubst.GAST_rasimpl]
quoted_subst [inductive, in GhostTT.autosubst.GAST_rasimpl]
q0 [constructor, in GhostTT.autosubst.RAsimpl]

R

RAsimpl [library]
reflection [constructor, in GhostTT.RTyping]
relative_consistency [lemma, in GhostTT.Model]
relm [definition, in GhostTT.TermMode]
relv [definition, in GhostTT.Erasure]
RenNotations [module, in GhostTT.autosubst.unscoped]
⟨ _ ; _ ⟩ (fscope) [notation, in GhostTT.autosubst.unscoped]
⟨ _ ⟩ (fscope) [notation, in GhostTT.autosubst.unscoped]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in GhostTT.autosubst.unscoped]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in GhostTT.autosubst.unscoped]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [notation, in GhostTT.autosubst.unscoped]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in GhostTT.autosubst.unscoped]
_ ⟨ _ ⟩ (subst_scope) [notation, in GhostTT.autosubst.unscoped]
RenSimplification [record, in GhostTT.autosubst.RAsimpl]
ren1 [projection, in GhostTT.autosubst.unscoped]
Ren1 [record, in GhostTT.autosubst.unscoped]
ren1 [constructor, in GhostTT.autosubst.unscoped]
Ren1 [inductive, in GhostTT.autosubst.unscoped]
ren2 [projection, in GhostTT.autosubst.unscoped]
Ren2 [record, in GhostTT.autosubst.unscoped]
ren2 [constructor, in GhostTT.autosubst.unscoped]
Ren2 [inductive, in GhostTT.autosubst.unscoped]
ren3 [projection, in GhostTT.autosubst.unscoped]
Ren3 [record, in GhostTT.autosubst.unscoped]
ren3 [constructor, in GhostTT.autosubst.unscoped]
Ren3 [inductive, in GhostTT.autosubst.unscoped]
ren4 [projection, in GhostTT.autosubst.unscoped]
Ren4 [record, in GhostTT.autosubst.unscoped]
ren4 [constructor, in GhostTT.autosubst.unscoped]
Ren4 [inductive, in GhostTT.autosubst.unscoped]
ren5 [projection, in GhostTT.autosubst.unscoped]
Ren5 [record, in GhostTT.autosubst.unscoped]
ren5 [constructor, in GhostTT.autosubst.unscoped]
Ren5 [inductive, in GhostTT.autosubst.unscoped]
reveal_hide [constructor, in GhostTT.Typing]
Revival [library]
revive_typing_eq [lemma, in GhostTT.Param]
revive_conv_eq [lemma, in GhostTT.Param]
revive_scoping_eq [lemma, in GhostTT.Param]
revive_context [lemma, in GhostTT.Revival]
revive_typing [lemma, in GhostTT.Revival]
revive_ctx_var [lemma, in GhostTT.Revival]
revive_castrm_conv [lemma, in GhostTT.Revival]
revive_castrm [lemma, in GhostTT.Revival]
revive_conv [lemma, in GhostTT.Revival]
revive_subst [lemma, in GhostTT.Revival]
revive_ren [lemma, in GhostTT.Revival]
revive_scoping [lemma, in GhostTT.Revival]
revive_sc_var [lemma, in GhostTT.Revival]
revive_ng [lemma, in GhostTT.Revival]
revive_sc [definition, in GhostTT.Revival]
revive_ctx [definition, in GhostTT.Revival]
revive_term [definition, in GhostTT.Revival]
rev_subst [definition, in GhostTT.Revival]
rmctx [definition, in GhostTT.Potential]
rpm_lift_eq [lemma, in GhostTT.Param]
rpm_lift [definition, in GhostTT.Param]
rscoping [definition, in GhostTT.BasicMetaTheory]
rscoping_sscoping [lemma, in GhostTT.BasicMetaTheory]
rscoping_comp_upren [lemma, in GhostTT.BasicMetaTheory]
rscoping_comp_S [lemma, in GhostTT.BasicMetaTheory]
rscoping_comp [definition, in GhostTT.BasicMetaTheory]
rscoping_morphism [instance, in GhostTT.BasicMetaTheory]
rscoping_shift [lemma, in GhostTT.BasicMetaTheory]
rscoping_S [lemma, in GhostTT.BasicMetaTheory]
rscoping_comp_weak [lemma, in GhostTT.Erasure]
rscoping_upren [lemma, in GhostTT.Erasure]
rscoping_weak [lemma, in GhostTT.Erasure]
rtype_conv [constructor, in GhostTT.RTyping]
rtype_bot_elim [constructor, in GhostTT.RTyping]
rtype_bot [constructor, in GhostTT.RTyping]
rtype_ghrefl [constructor, in GhostTT.RTyping]
rtype_gheq [constructor, in GhostTT.RTyping]
rtype_fromRev [constructor, in GhostTT.RTyping]
rtype_toRev [constructor, in GhostTT.RTyping]
rtype_Reveal [constructor, in GhostTT.RTyping]
rtype_reveal [constructor, in GhostTT.RTyping]
rtype_hide [constructor, in GhostTT.RTyping]
rtype_erased [constructor, in GhostTT.RTyping]
rtype_app [constructor, in GhostTT.RTyping]
rtype_lam [constructor, in GhostTT.RTyping]
rtype_pi [constructor, in GhostTT.RTyping]
rtype_sort [constructor, in GhostTT.RTyping]
rtype_var [constructor, in GhostTT.RTyping]
rtyping [definition, in GhostTT.BasicMetaTheory]
RTyping [library]
rtyping_triv [lemma, in GhostTT.Examples]
rtyping_S [lemma, in GhostTT.BasicMetaTheory]
rtyping_shift [lemma, in GhostTT.BasicMetaTheory]
rtyping_scoping [lemma, in GhostTT.BasicMetaTheory]
rtyping_morphism [instance, in GhostTT.BasicMetaTheory]
rwf [inductive, in GhostTT.RTyping]
rwf_sind [definition, in GhostTT.RTyping]
rwf_rec [definition, in GhostTT.RTyping]
rwf_ind [definition, in GhostTT.RTyping]
rwf_rect [definition, in GhostTT.RTyping]
rwf_cons [constructor, in GhostTT.RTyping]
rwf_nil [constructor, in GhostTT.RTyping]

S

S [constructor, in GhostTT.TransNat]
sc [definition, in GhostTT.ContextDecl]
scons [definition, in GhostTT.autosubst.unscoped]
scons_morphism2 [instance, in GhostTT.autosubst.unscoped]
scons_morphism [instance, in GhostTT.autosubst.unscoped]
scons_comp' [lemma, in GhostTT.autosubst.unscoped]
scons_eta_id' [lemma, in GhostTT.autosubst.unscoped]
scons_eta' [lemma, in GhostTT.autosubst.unscoped]
scope [abbreviation, in GhostTT.ContextDecl]
scope_bot_elim [constructor, in GhostTT.Scoping]
scope_bot [constructor, in GhostTT.Scoping]
scope_vec_elim [constructor, in GhostTT.Scoping]
scope_vcons [constructor, in GhostTT.Scoping]
scope_vnil [constructor, in GhostTT.Scoping]
scope_vec [constructor, in GhostTT.Scoping]
scope_nat_elim [constructor, in GhostTT.Scoping]
scope_succ [constructor, in GhostTT.Scoping]
scope_zero [constructor, in GhostTT.Scoping]
scope_nat [constructor, in GhostTT.Scoping]
scope_if [constructor, in GhostTT.Scoping]
scope_false [constructor, in GhostTT.Scoping]
scope_true [constructor, in GhostTT.Scoping]
scope_bool [constructor, in GhostTT.Scoping]
scope_ghcast [constructor, in GhostTT.Scoping]
scope_ghrefl [constructor, in GhostTT.Scoping]
scope_gheq [constructor, in GhostTT.Scoping]
scope_fromRev [constructor, in GhostTT.Scoping]
scope_toRev [constructor, in GhostTT.Scoping]
scope_Reveal [constructor, in GhostTT.Scoping]
scope_reveal [constructor, in GhostTT.Scoping]
scope_hide [constructor, in GhostTT.Scoping]
scope_erased [constructor, in GhostTT.Scoping]
scope_app [constructor, in GhostTT.Scoping]
scope_lam [constructor, in GhostTT.Scoping]
scope_pi [constructor, in GhostTT.Scoping]
scope_var [constructor, in GhostTT.Scoping]
scope_top [lemma, in GhostTT.BasicMetaTheory]
scope_bot_elim_inv [lemma, in GhostTT.BasicMetaTheory]
scope_if_inv [lemma, in GhostTT.BasicMetaTheory]
scope_gheq_inv [lemma, in GhostTT.BasicMetaTheory]
scope_hide_inv [lemma, in GhostTT.BasicMetaTheory]
scope_erased_inv [lemma, in GhostTT.BasicMetaTheory]
scope_pi_inv [lemma, in GhostTT.BasicMetaTheory]
scope_sort_inv [lemma, in GhostTT.BasicMetaTheory]
scope_fromRev_inv [lemma, in GhostTT.BasicMetaTheory]
scope_toRev_inv [lemma, in GhostTT.BasicMetaTheory]
scope_Reveal_inv [lemma, in GhostTT.BasicMetaTheory]
scope_reveal_inv [lemma, in GhostTT.BasicMetaTheory]
scope_lam_inv [lemma, in GhostTT.BasicMetaTheory]
scope_app_inv [lemma, in GhostTT.BasicMetaTheory]
scope_cons [constructor, in GhostTT.BasicMetaTheory]
scope_nil [constructor, in GhostTT.BasicMetaTheory]
scoping [inductive, in GhostTT.Scoping]
Scoping [library]
scoping_functional [lemma, in GhostTT.TermMode]
scoping_md [lemma, in GhostTT.TermMode]
scoping_rpm_lift [lemma, in GhostTT.Param]
scoping_epm_lift [lemma, in GhostTT.Param]
scoping_er_sub_param [lemma, in GhostTT.Param]
scoping_rev_sub_param [lemma, in GhostTT.Param]
scoping_sind [definition, in GhostTT.Scoping]
scoping_ind [definition, in GhostTT.Scoping]
scoping_to_rev [lemma, in GhostTT.Revival]
scoping_sub_rev [lemma, in GhostTT.Revival]
scoping_castrm [lemma, in GhostTT.BasicMetaTheory]
scoping_subst [lemma, in GhostTT.BasicMetaTheory]
scoping_ren [lemma, in GhostTT.BasicMetaTheory]
scpoe_sort [constructor, in GhostTT.Scoping]
sc_rmctx [lemma, in GhostTT.Potential]
sc_urm_ctx [lemma, in GhostTT.Model]
SFalse [inductive, in GhostTT.FreeTheorem]
SFalse_sind [definition, in GhostTT.FreeTheorem]
SFalse_rec [definition, in GhostTT.FreeTheorem]
SFalse_ind [definition, in GhostTT.FreeTheorem]
SFalse_rect [definition, in GhostTT.FreeTheorem]
shift [definition, in GhostTT.autosubst.unscoped]
SI [constructor, in GhostTT.FreeTheorem]
sort_mode_inj [lemma, in GhostTT.Model]
sq [constructor, in GhostTT.TransVec]
squash [inductive, in GhostTT.TransVec]
squash_sind [definition, in GhostTT.TransVec]
sscoping [inductive, in GhostTT.BasicMetaTheory]
sscoping_urm [lemma, in GhostTT.Model]
sscoping_castrm [lemma, in GhostTT.BasicMetaTheory]
sscoping_comp_one [lemma, in GhostTT.BasicMetaTheory]
sscoping_comp_shift [lemma, in GhostTT.BasicMetaTheory]
sscoping_comp [definition, in GhostTT.BasicMetaTheory]
sscoping_one [lemma, in GhostTT.BasicMetaTheory]
sscoping_ids [lemma, in GhostTT.BasicMetaTheory]
sscoping_morphism [instance, in GhostTT.BasicMetaTheory]
sscoping_shift [lemma, in GhostTT.BasicMetaTheory]
sscoping_weak [lemma, in GhostTT.BasicMetaTheory]
sscoping_sind [definition, in GhostTT.BasicMetaTheory]
sscoping_ind [definition, in GhostTT.BasicMetaTheory]
star [definition, in GhostTT.Examples]
STrue [inductive, in GhostTT.FreeTheorem]
STrue_sind [definition, in GhostTT.FreeTheorem]
styping [inductive, in GhostTT.BasicMetaTheory]
styping_morphism [instance, in GhostTT.CCMetaTheory]
styping_one [lemma, in GhostTT.BasicMetaTheory]
styping_ids [lemma, in GhostTT.BasicMetaTheory]
styping_shift [lemma, in GhostTT.BasicMetaTheory]
styping_weak [lemma, in GhostTT.BasicMetaTheory]
styping_scoping [lemma, in GhostTT.BasicMetaTheory]
styping_morphism [instance, in GhostTT.BasicMetaTheory]
styping_sind [definition, in GhostTT.BasicMetaTheory]
styping_ind [definition, in GhostTT.BasicMetaTheory]
SubstNotations [module, in GhostTT.autosubst.unscoped]
SubstNotations [library]
_ [ _ ; _ ] (subst_scope) [notation, in GhostTT.autosubst.unscoped]
_ [ _ ] (subst_scope) [notation, in GhostTT.autosubst.unscoped]
SubstSimplification [record, in GhostTT.autosubst.GAST_rasimpl]
subst1 [projection, in GhostTT.autosubst.unscoped]
Subst1 [record, in GhostTT.autosubst.unscoped]
subst1 [constructor, in GhostTT.autosubst.unscoped]
Subst1 [inductive, in GhostTT.autosubst.unscoped]
subst2 [projection, in GhostTT.autosubst.unscoped]
Subst2 [record, in GhostTT.autosubst.unscoped]
subst2 [constructor, in GhostTT.autosubst.unscoped]
Subst2 [inductive, in GhostTT.autosubst.unscoped]
subst3 [projection, in GhostTT.autosubst.unscoped]
Subst3 [record, in GhostTT.autosubst.unscoped]
subst3 [constructor, in GhostTT.autosubst.unscoped]
Subst3 [inductive, in GhostTT.autosubst.unscoped]
subst4 [projection, in GhostTT.autosubst.unscoped]
Subst4 [record, in GhostTT.autosubst.unscoped]
subst4 [constructor, in GhostTT.autosubst.unscoped]
Subst4 [inductive, in GhostTT.autosubst.unscoped]
subst5 [projection, in GhostTT.autosubst.unscoped]
Subst5 [record, in GhostTT.autosubst.unscoped]
subst5 [constructor, in GhostTT.autosubst.unscoped]
Subst5 [inductive, in GhostTT.autosubst.unscoped]

T

TermMode [library]
TermNotations [library]
TermSimplification [record, in GhostTT.autosubst.GAST_rasimpl]
test_qsubst_ren_id [definition, in GhostTT.autosubst.CCAST_rasimpl]
test_qren_id [definition, in GhostTT.autosubst.RAsimpl]
test_qsubst_ren_id [definition, in GhostTT.autosubst.GAST_rasimpl]
top [abbreviation, in GhostTT.TermNotations]
TransNat [library]
TransVec [library]
tr_gheq [lemma, in GhostTT.ElimReflection]
tr_Reveal [lemma, in GhostTT.ElimReflection]
tr_var [lemma, in GhostTT.ElimReflection]
tr_hide [lemma, in GhostTT.ElimReflection]
tr_ren_lax [lemma, in GhostTT.ElimReflection]
tr_ren [lemma, in GhostTT.ElimReflection]
tr_app_lax [lemma, in GhostTT.ElimReflection]
tr_app [lemma, in GhostTT.ElimReflection]
tr_sort_lax [lemma, in GhostTT.ElimReflection]
tr_sort [lemma, in GhostTT.ElimReflection]
tr_erased [lemma, in GhostTT.ElimReflection]
tr_bot [lemma, in GhostTT.ElimReflection]
tr_pi [lemma, in GhostTT.ElimReflection]
tr_choice [lemma, in GhostTT.Potential]
tr_scoping [lemma, in GhostTT.Potential]
tr_cons [lemma, in GhostTT.Potential]
tr_bot_eq [lemma, in GhostTT.Potential]
tr_sort_inv [lemma, in GhostTT.Potential]
tr_sort_eq [lemma, in GhostTT.Potential]
tr_ty [definition, in GhostTT.Potential]
tr_ctx [definition, in GhostTT.Potential]
ty [inductive, in GhostTT.TransNat]
tyerr [constructor, in GhostTT.TransNat]
type_pi_opt [lemma, in GhostTT.Admissible]
type_conv_alt [lemma, in GhostTT.Admissible]
type_conv [lemma, in GhostTT.Admissible]
type_bot_elim [lemma, in GhostTT.Admissible]
type_if [lemma, in GhostTT.Admissible]
type_ghcast [lemma, in GhostTT.Admissible]
type_ghrefl [lemma, in GhostTT.Admissible]
type_gheq [lemma, in GhostTT.Admissible]
type_fromRev [lemma, in GhostTT.Admissible]
type_toRev [lemma, in GhostTT.Admissible]
type_Reveal [lemma, in GhostTT.Admissible]
type_reveal [lemma, in GhostTT.Admissible]
type_hide [lemma, in GhostTT.Admissible]
type_erased [lemma, in GhostTT.Admissible]
type_app [lemma, in GhostTT.Admissible]
type_lam [lemma, in GhostTT.Admissible]
type_pi [lemma, in GhostTT.Admissible]
type_discr [lemma, in GhostTT.Examples]
type_star_gen [lemma, in GhostTT.Examples]
type_star [lemma, in GhostTT.Examples]
type_gS [lemma, in GhostTT.Examples]
type_erased_nat_discrP_gen [lemma, in GhostTT.Examples]
type_erased_nat_discrP [lemma, in GhostTT.Examples]
type_discr_nat_gen [lemma, in GhostTT.Examples]
type_discr_nat [lemma, in GhostTT.Examples]
type_iszero_gen [lemma, in GhostTT.Examples]
type_iszero [lemma, in GhostTT.Examples]
type_discr_bool_gen [lemma, in GhostTT.Examples]
type_discr_bool [lemma, in GhostTT.Examples]
type_to_rev_eq [lemma, in GhostTT.Param]
type_pmPiNP_eq [lemma, in GhostTT.Param]
type_pmPiNP [lemma, in GhostTT.Param]
type_pProp [lemma, in GhostTT.Param]
type_pType [lemma, in GhostTT.Param]
type_pKind [lemma, in GhostTT.Param]
type_pmifK [lemma, in GhostTT.Param]
type_pmif [lemma, in GhostTT.Param]
type_perif [lemma, in GhostTT.Param]
type_pmPiP [lemma, in GhostTT.Param]
type_plam [lemma, in GhostTT.Param]
type_pPi [lemma, in GhostTT.Param]
type_pcastTG [lemma, in GhostTT.Param]
type_rpm_lift_eq [lemma, in GhostTT.Param]
type_rpm_lift [lemma, in GhostTT.Param]
type_epm_lift_eq [lemma, in GhostTT.Param]
type_epm_lift [lemma, in GhostTT.Param]
type_er_bool_cst [lemma, in GhostTT.FreeTheorem]
type_beq [lemma, in GhostTT.FreeTheorem]
type_to_rev [lemma, in GhostTT.Revival]
type_unique [lemma, in GhostTT.Model]
type_bot_elim_inv [lemma, in GhostTT.BasicMetaTheory]
type_bot_inv [lemma, in GhostTT.BasicMetaTheory]
type_vec_elim_inv [lemma, in GhostTT.BasicMetaTheory]
type_vcons_inv [lemma, in GhostTT.BasicMetaTheory]
type_vnil_inv [lemma, in GhostTT.BasicMetaTheory]
type_vec_inv [lemma, in GhostTT.BasicMetaTheory]
type_nat_elim_inv [lemma, in GhostTT.BasicMetaTheory]
type_succ_inv [lemma, in GhostTT.BasicMetaTheory]
type_zero_inv [lemma, in GhostTT.BasicMetaTheory]
type_nat_inv [lemma, in GhostTT.BasicMetaTheory]
type_if_inv [lemma, in GhostTT.BasicMetaTheory]
type_false_inv [lemma, in GhostTT.BasicMetaTheory]
type_true_inv [lemma, in GhostTT.BasicMetaTheory]
type_bool_inv [lemma, in GhostTT.BasicMetaTheory]
type_ghcast_inv [lemma, in GhostTT.BasicMetaTheory]
type_ghrefl_inv [lemma, in GhostTT.BasicMetaTheory]
type_gheq_inv [lemma, in GhostTT.BasicMetaTheory]
type_fromRev_inv [lemma, in GhostTT.BasicMetaTheory]
type_toRev_inv [lemma, in GhostTT.BasicMetaTheory]
type_Reveal_inv [lemma, in GhostTT.BasicMetaTheory]
type_reveal_inv [lemma, in GhostTT.BasicMetaTheory]
type_hide_inv [lemma, in GhostTT.BasicMetaTheory]
type_erased_inv [lemma, in GhostTT.BasicMetaTheory]
type_app_inv [lemma, in GhostTT.BasicMetaTheory]
type_lam_inv [lemma, in GhostTT.BasicMetaTheory]
type_pi_inv [lemma, in GhostTT.BasicMetaTheory]
type_sort_inv [lemma, in GhostTT.BasicMetaTheory]
type_var_inv [lemma, in GhostTT.BasicMetaTheory]
type_cons [constructor, in GhostTT.BasicMetaTheory]
type_nil [constructor, in GhostTT.BasicMetaTheory]
type_conv [constructor, in GhostTT.Typing]
type_bot_elim [constructor, in GhostTT.Typing]
type_bot [constructor, in GhostTT.Typing]
type_vec_elim [constructor, in GhostTT.Typing]
type_vcons [constructor, in GhostTT.Typing]
type_vnil [constructor, in GhostTT.Typing]
type_vec [constructor, in GhostTT.Typing]
type_nat_elim [constructor, in GhostTT.Typing]
type_succ [constructor, in GhostTT.Typing]
type_zero [constructor, in GhostTT.Typing]
type_nat [constructor, in GhostTT.Typing]
type_if [constructor, in GhostTT.Typing]
type_false [constructor, in GhostTT.Typing]
type_true [constructor, in GhostTT.Typing]
type_bool [constructor, in GhostTT.Typing]
type_ghcast [constructor, in GhostTT.Typing]
type_ghrefl [constructor, in GhostTT.Typing]
type_gheq [constructor, in GhostTT.Typing]
type_fromRev [constructor, in GhostTT.Typing]
type_toRev [constructor, in GhostTT.Typing]
type_Reveal [constructor, in GhostTT.Typing]
type_reveal [constructor, in GhostTT.Typing]
type_hide [constructor, in GhostTT.Typing]
type_erased [constructor, in GhostTT.Typing]
type_app [constructor, in GhostTT.Typing]
type_lam [constructor, in GhostTT.Typing]
type_pi [constructor, in GhostTT.Typing]
type_sort [constructor, in GhostTT.Typing]
type_var [constructor, in GhostTT.Typing]
typing [inductive, in GhostTT.Typing]
Typing [library]
typing_er_sub_param [lemma, in GhostTT.Param]
typing_rev_sub_param [lemma, in GhostTT.Param]
typing_sub_rev [lemma, in GhostTT.Revival]
typing_subst [lemma, in GhostTT.BasicMetaTheory]
typing_ren [lemma, in GhostTT.BasicMetaTheory]
typing_sind [definition, in GhostTT.Typing]
typing_ind [definition, in GhostTT.Typing]
tyval [constructor, in GhostTT.TransNat]
ty_sind [definition, in GhostTT.TransNat]
ty_rec [definition, in GhostTT.TransNat]
ty_ind [definition, in GhostTT.TransNat]
ty_rect [definition, in GhostTT.TransNat]

U

ueq [definition, in GhostTT.Univ]
ueq_Ghost_eq [lemma, in GhostTT.Univ]
ueq_Type_eq [lemma, in GhostTT.Univ]
ueq_Kind_eq [lemma, in GhostTT.Univ]
ueq_eq [lemma, in GhostTT.Univ]
umax [definition, in GhostTT.Univ]
Univ [library]
unquote_cterm [definition, in GhostTT.autosubst.CCAST_rasimpl]
unquote_subst [definition, in GhostTT.autosubst.CCAST_rasimpl]
unquote_ren [definition, in GhostTT.autosubst.RAsimpl]
unquote_nat [definition, in GhostTT.autosubst.RAsimpl]
unquote_term [definition, in GhostTT.autosubst.GAST_rasimpl]
unquote_subst [definition, in GhostTT.autosubst.GAST_rasimpl]
unscoped [library]
UnscopedNotations [module, in GhostTT.autosubst.unscoped]
↑ (subst_scope) [notation, in GhostTT.autosubst.unscoped]
_ .. (subst_scope) [notation, in GhostTT.autosubst.unscoped]
up_allfv [definition, in GhostTT.autosubst.unscoped]
up_ren_ren [lemma, in GhostTT.autosubst.unscoped]
up_ren [definition, in GhostTT.autosubst.unscoped]
urm [definition, in GhostTT.Model]
urm_conv_aux [lemma, in GhostTT.Model]
urm_cscoping [lemma, in GhostTT.Model]
urm_ctx [definition, in GhostTT.Model]
urm_scoping [lemma, in GhostTT.Model]
urm_subst [lemma, in GhostTT.Model]
urm_ren [lemma, in GhostTT.Model]
usup [definition, in GhostTT.Univ]
Util [library]

V

validity [lemma, in GhostTT.BasicMetaTheory]
Var [record, in GhostTT.autosubst.unscoped]
Var [inductive, in GhostTT.autosubst.unscoped]
var_zero [definition, in GhostTT.autosubst.unscoped]
vec_err [constructor, in GhostTT.TransVec]
vpar [definition, in GhostTT.Param]
vreg [definition, in GhostTT.Param]
vreg_vpar_dec [lemma, in GhostTT.Param]

W

WasGhost [constructor, in GhostTT.BasicAST]
WasKind [constructor, in GhostTT.BasicAST]
WasType [constructor, in GhostTT.BasicAST]
wf [inductive, in GhostTT.Typing]
wf_cons [lemma, in GhostTT.Admissible]
wf_sind [definition, in GhostTT.Typing]
wf_ind [definition, in GhostTT.Typing]
wf_cons [constructor, in GhostTT.Typing]
wf_nil [constructor, in GhostTT.Typing]
whenSome [definition, in GhostTT.Util]

other

_ .. (subst_scope) [notation, in GhostTT.SubstNotations]
↑ (subst_scope) [notation, in GhostTT.SubstNotations]
_ <[ _ ] (subst_scope) [notation, in GhostTT.SubstNotations]
_ ⋅ _ (subst_scope) [notation, in GhostTT.SubstNotations]
∑ _ .. _ , _ (type_scope) [notation, in GhostTT.Util]
_ ⊨ _ : _ ∈ ⟦ _ : _ ⟧x [notation, in GhostTT.Potential]
_ ⇒[ _ | _ / _ | _ ] _ [notation, in GhostTT.TermNotations]
_ ,,, _ [notation, in GhostTT.ContextDecl]
_ ,, _ [notation, in GhostTT.ContextDecl]
_ ⊢ᶜ _ : _ [notation, in GhostTT.CTyping]
_ ⊢ᶜ _ ≡ _ [notation, in GhostTT.CTyping]
_ ⇒[ _ ] _ [notation, in GhostTT.CTyping]
_ ⊢ _ ≈ _ [notation, in GhostTT.Model]
_ ⊢ _ ε≡ _ [notation, in GhostTT.BasicMetaTheory]
_ ⊢ _ : _ [notation, in GhostTT.Typing]
_ ⊢ _ ≡ _ [notation, in GhostTT.Typing]
_ ⊢ˣ _ : _ [notation, in GhostTT.RTyping]
list_map [notation, in GhostTT.autosubst.core]
#| _ | [notation, in GhostTT.Util]
ε| _ | [notation, in GhostTT.CastRemoval]
∙ [notation, in GhostTT.ContextDecl]
⟦ _ ⟧p [notation, in GhostTT.Param]
⟦ _ | _ ⟧p [notation, in GhostTT.Param]
⟦ _ | _ ⟧pv [notation, in GhostTT.Param]
⟦ _ | _ ⟧p∅ [notation, in GhostTT.Param]
⟦ _ | _ ⟧pτ [notation, in GhostTT.Param]
⟦ _ | _ ⟧pε [notation, in GhostTT.Param]
⟦ _ ⟧v [notation, in GhostTT.Revival]
⟦ _ | _ ⟧v [notation, in GhostTT.Revival]
⟦ _ ⟧ε [notation, in GhostTT.Erasure]
⟦ _ | _ ⟧∅ [notation, in GhostTT.Erasure]
⟦ _ | _ ⟧τ [notation, in GhostTT.Erasure]
⟦ _ | _ ⟧ε [notation, in GhostTT.Erasure]

Notation Index

C

_ >> _ (fscope) [in GhostTT.autosubst.unscoped]
_ .: _ (subst_scope) [in GhostTT.autosubst.unscoped]
[ _ ] (fscope) [in GhostTT.autosubst.GAST]
[ _ ] (fscope) [in GhostTT.autosubst.CCAST]
⟨ _ ⟩ (fscope) [in GhostTT.autosubst.GAST]
⟨ _ ⟩ (fscope) [in GhostTT.autosubst.CCAST]
_ __term (subst_scope) [in GhostTT.autosubst.GAST]
_ __term (subst_scope) [in GhostTT.autosubst.GAST]
var (subst_scope) [in GhostTT.autosubst.GAST]
_ ⟨ _ ⟩ (subst_scope) [in GhostTT.autosubst.GAST]
↑__term (subst_scope) [in GhostTT.autosubst.GAST]
↑__term (subst_scope) [in GhostTT.autosubst.GAST]
_ [ _ ] (subst_scope) [in GhostTT.autosubst.GAST]
_ __cterm (subst_scope) [in GhostTT.autosubst.CCAST]
_ __cterm (subst_scope) [in GhostTT.autosubst.CCAST]
var (subst_scope) [in GhostTT.autosubst.CCAST]
_ ⟨ _ ⟩ (subst_scope) [in GhostTT.autosubst.CCAST]
↑__cterm (subst_scope) [in GhostTT.autosubst.CCAST]
↑__cterm (subst_scope) [in GhostTT.autosubst.CCAST]
_ [ _ ] (subst_scope) [in GhostTT.autosubst.CCAST]

R

⟨ _ ; _ ⟩ (fscope) [in GhostTT.autosubst.unscoped]
⟨ _ ⟩ (fscope) [in GhostTT.autosubst.unscoped]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [in GhostTT.autosubst.unscoped]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [in GhostTT.autosubst.unscoped]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [in GhostTT.autosubst.unscoped]
_ ⟨ _ ; _ ⟩ (subst_scope) [in GhostTT.autosubst.unscoped]
_ ⟨ _ ⟩ (subst_scope) [in GhostTT.autosubst.unscoped]

S

_ [ _ ; _ ] (subst_scope) [in GhostTT.autosubst.unscoped]
_ [ _ ] (subst_scope) [in GhostTT.autosubst.unscoped]

U

↑ (subst_scope) [in GhostTT.autosubst.unscoped]
_ .. (subst_scope) [in GhostTT.autosubst.unscoped]

other

_ .. (subst_scope) [in GhostTT.SubstNotations]
↑ (subst_scope) [in GhostTT.SubstNotations]
_ <[ _ ] (subst_scope) [in GhostTT.SubstNotations]
_ ⋅ _ (subst_scope) [in GhostTT.SubstNotations]
∑ _ .. _ , _ (type_scope) [in GhostTT.Util]
_ ⊨ _ : _ ∈ ⟦ _ : _ ⟧x [in GhostTT.Potential]
_ ⇒[ _ | _ / _ | _ ] _ [in GhostTT.TermNotations]
_ ,,, _ [in GhostTT.ContextDecl]
_ ,, _ [in GhostTT.ContextDecl]
_ ⊢ᶜ _ : _ [in GhostTT.CTyping]
_ ⊢ᶜ _ ≡ _ [in GhostTT.CTyping]
_ ⇒[ _ ] _ [in GhostTT.CTyping]
_ ⊢ _ ≈ _ [in GhostTT.Model]
_ ⊢ _ ε≡ _ [in GhostTT.BasicMetaTheory]
_ ⊢ _ : _ [in GhostTT.Typing]
_ ⊢ _ ≡ _ [in GhostTT.Typing]
_ ⊢ˣ _ : _ [in GhostTT.RTyping]
list_map [in GhostTT.autosubst.core]
#| _ | [in GhostTT.Util]
ε| _ | [in GhostTT.CastRemoval]
∙ [in GhostTT.ContextDecl]
⟦ _ ⟧p [in GhostTT.Param]
⟦ _ | _ ⟧p [in GhostTT.Param]
⟦ _ | _ ⟧pv [in GhostTT.Param]
⟦ _ | _ ⟧p∅ [in GhostTT.Param]
⟦ _ | _ ⟧pτ [in GhostTT.Param]
⟦ _ | _ ⟧pε [in GhostTT.Param]
⟦ _ ⟧v [in GhostTT.Revival]
⟦ _ | _ ⟧v [in GhostTT.Revival]
⟦ _ ⟧ε [in GhostTT.Erasure]
⟦ _ | _ ⟧∅ [in GhostTT.Erasure]
⟦ _ | _ ⟧τ [in GhostTT.Erasure]
⟦ _ | _ ⟧ε [in GhostTT.Erasure]

Module Index

A

Allfv [in GhostTT.autosubst.GAST]
Allfv [in GhostTT.autosubst.CCAST]

C

CombineNotations [in GhostTT.autosubst.unscoped]
Core [in GhostTT.autosubst.GAST]
Core [in GhostTT.autosubst.CCAST]

E

Extra [in GhostTT.autosubst.GAST]
Extra [in GhostTT.autosubst.CCAST]

I

interface [in GhostTT.autosubst.GAST]
interface [in GhostTT.autosubst.CCAST]

R

RenNotations [in GhostTT.autosubst.unscoped]

S

SubstNotations [in GhostTT.autosubst.unscoped]

U

UnscopedNotations [in GhostTT.autosubst.unscoped]

Variable Index

M

Mode.dummy [in GhostTT.TermMode]

Library Index

A

Admissible
Assumptions

B

BasicAST
BasicMetaTheory

C

CastRemoval
CCAST
CCAST_rasimpl
CCMetaTheory
ContextDecl
core
CScoping
CTyping

E

ElimReflection
Erasure
Examples

F

G

GAST
GAST_rasimpl

M

Model

P

Param
Potential

R

RAsimpl
Revival
RTyping

S

Scoping
SubstNotations

T

TermMode
TermNotations
TransNat
TransVec
Typing

U

Univ
unscoped
Util

Lemma Index

A

Allfv.upAllfvImpl_term_term [in GhostTT.autosubst.GAST]
Allfv.upAllfvImpl_cterm_cterm [in GhostTT.autosubst.CCAST]
Allfv.upAllfvRenL_term_term [in GhostTT.autosubst.GAST]
Allfv.upAllfvRenL_cterm_cterm [in GhostTT.autosubst.CCAST]
Allfv.upAllfvRenR_term_term [in GhostTT.autosubst.GAST]
Allfv.upAllfvRenR_cterm_cterm [in GhostTT.autosubst.CCAST]
Allfv.upAllfvTriv_term_term [in GhostTT.autosubst.GAST]
Allfv.upAllfvTriv_cterm_cterm [in GhostTT.autosubst.CCAST]
Allfv.upAllfv_term_term [in GhostTT.autosubst.GAST]
Allfv.upAllfv_cterm_cterm [in GhostTT.autosubst.CCAST]
apply_subst_sound [in GhostTT.autosubst.CCAST_rasimpl]
apply_ren_sound [in GhostTT.autosubst.RAsimpl]
apply_subst_sound [in GhostTT.autosubst.GAST_rasimpl]
autosubst_simpl_cstyping [in GhostTT.CCMetaTheory]
autosubst_simpl_crtyping [in GhostTT.CCMetaTheory]
autosubst_simpl_csscoping [in GhostTT.CCMetaTheory]
autosubst_simpl_crscoping [in GhostTT.CCMetaTheory]
autosubst_simpl_cterm_subst [in GhostTT.autosubst.CCAST_rasimpl]
autosubst_simpl_cterm_ren [in GhostTT.autosubst.CCAST_rasimpl]
autosubst_simpl_term_subst [in GhostTT.autosubst.GAST_rasimpl]
autosubst_simpl_term_ren [in GhostTT.autosubst.GAST_rasimpl]
autosubst_simpl_styping [in GhostTT.BasicMetaTheory]
autosubst_simpl_rtyping [in GhostTT.BasicMetaTheory]
autosubst_simpl_sscoping [in GhostTT.BasicMetaTheory]
autosubst_simpl_rscoping [in GhostTT.BasicMetaTheory]

C

castrm_subst [in GhostTT.BasicMetaTheory]
castrm_ren [in GhostTT.BasicMetaTheory]
ccmeta_conv [in GhostTT.CCMetaTheory]
ccmeta_refl [in GhostTT.Erasure]
ccong_pmPi [in GhostTT.Param]
ccong_pmifK [in GhostTT.Param]
ccong_pmif [in GhostTT.Param]
ccong_perif [in GhostTT.Param]
ccong_rpm_lift [in GhostTT.Param]
ccong_epm_lift [in GhostTT.Param]
ccong_plam [in GhostTT.Param]
ccong_pPi [in GhostTT.Param]
cconv_close [in GhostTT.CCMetaTheory]
cconv_subst [in GhostTT.CCMetaTheory]
cconv_ren [in GhostTT.CCMetaTheory]
cconv_ty_lift [in GhostTT.Erasure]
cmeta_conv_trans_r [in GhostTT.CCMetaTheory]
cmeta_conv_trans_l [in GhostTT.CCMetaTheory]
cmeta_conv [in GhostTT.CCMetaTheory]
cmeta_ctx_conv [in GhostTT.Param]
conservativity [in GhostTT.ElimReflection]
consistency [in GhostTT.ElimReflection]
constant_free_theorem [in GhostTT.FreeTheorem]
conv_to_rev [in GhostTT.Revival]
conv_upto [in GhostTT.Model]
conv_meta_refl [in GhostTT.Model]
conv_urm [in GhostTT.Model]
conv_subst [in GhostTT.BasicMetaTheory]
conv_ren [in GhostTT.BasicMetaTheory]
conv_md [in GhostTT.BasicMetaTheory]
Core.congr_bot_elim [in GhostTT.autosubst.GAST]
Core.congr_bot [in GhostTT.autosubst.GAST]
Core.congr_tvec_elim [in GhostTT.autosubst.GAST]
Core.congr_tvcons [in GhostTT.autosubst.GAST]
Core.congr_tvnil [in GhostTT.autosubst.GAST]
Core.congr_tvec [in GhostTT.autosubst.GAST]
Core.congr_tnat_elim [in GhostTT.autosubst.GAST]
Core.congr_tsucc [in GhostTT.autosubst.GAST]
Core.congr_tzero [in GhostTT.autosubst.GAST]
Core.congr_tnat [in GhostTT.autosubst.GAST]
Core.congr_tif [in GhostTT.autosubst.GAST]
Core.congr_tfalse [in GhostTT.autosubst.GAST]
Core.congr_ttrue [in GhostTT.autosubst.GAST]
Core.congr_tbool [in GhostTT.autosubst.GAST]
Core.congr_ghcast [in GhostTT.autosubst.GAST]
Core.congr_ghrefl [in GhostTT.autosubst.GAST]
Core.congr_gheq [in GhostTT.autosubst.GAST]
Core.congr_fromRev [in GhostTT.autosubst.GAST]
Core.congr_toRev [in GhostTT.autosubst.GAST]
Core.congr_Reveal [in GhostTT.autosubst.GAST]
Core.congr_reveal [in GhostTT.autosubst.GAST]
Core.congr_hide [in GhostTT.autosubst.GAST]
Core.congr_Erased [in GhostTT.autosubst.GAST]
Core.congr_app [in GhostTT.autosubst.GAST]
Core.congr_lam [in GhostTT.autosubst.GAST]
Core.congr_Pi [in GhostTT.autosubst.GAST]
Core.congr_Sort [in GhostTT.autosubst.GAST]
Core.congr_pvec_elimP [in GhostTT.autosubst.CCAST]
Core.congr_pvec_elimG [in GhostTT.autosubst.CCAST]
Core.congr_pvec_elim [in GhostTT.autosubst.CCAST]
Core.congr_pvcons [in GhostTT.autosubst.CCAST]
Core.congr_pvnil [in GhostTT.autosubst.CCAST]
Core.congr_pvec [in GhostTT.autosubst.CCAST]
Core.congr_evec_elim [in GhostTT.autosubst.CCAST]
Core.congr_evcons [in GhostTT.autosubst.CCAST]
Core.congr_evnil [in GhostTT.autosubst.CCAST]
Core.congr_evec [in GhostTT.autosubst.CCAST]
Core.congr_pnat_elimP [in GhostTT.autosubst.CCAST]
Core.congr_pnat_elim [in GhostTT.autosubst.CCAST]
Core.congr_psucc [in GhostTT.autosubst.CCAST]
Core.congr_pzero [in GhostTT.autosubst.CCAST]
Core.congr_pnat [in GhostTT.autosubst.CCAST]
Core.congr_enat_elim [in GhostTT.autosubst.CCAST]
Core.congr_esucc [in GhostTT.autosubst.CCAST]
Core.congr_ezero [in GhostTT.autosubst.CCAST]
Core.congr_enat [in GhostTT.autosubst.CCAST]
Core.congr_pif [in GhostTT.autosubst.CCAST]
Core.congr_pfalse [in GhostTT.autosubst.CCAST]
Core.congr_ptrue [in GhostTT.autosubst.CCAST]
Core.congr_pbool [in GhostTT.autosubst.CCAST]
Core.congr_eif [in GhostTT.autosubst.CCAST]
Core.congr_bool_err [in GhostTT.autosubst.CCAST]
Core.congr_efalse [in GhostTT.autosubst.CCAST]
Core.congr_etrue [in GhostTT.autosubst.CCAST]
Core.congr_ebool [in GhostTT.autosubst.CCAST]
Core.congr_tJ [in GhostTT.autosubst.CCAST]
Core.congr_trefl [in GhostTT.autosubst.CCAST]
Core.congr_teq [in GhostTT.autosubst.CCAST]
Core.congr_sq_elim [in GhostTT.autosubst.CCAST]
Core.congr_sq [in GhostTT.autosubst.CCAST]
Core.congr_squash [in GhostTT.autosubst.CCAST]
Core.congr_cErr [in GhostTT.autosubst.CCAST]
Core.congr_cEl [in GhostTT.autosubst.CCAST]
Core.congr_ctyerr [in GhostTT.autosubst.CCAST]
Core.congr_ctyval [in GhostTT.autosubst.CCAST]
Core.congr_cty [in GhostTT.autosubst.CCAST]
Core.congr_cbot_elim [in GhostTT.autosubst.CCAST]
Core.congr_cbot [in GhostTT.autosubst.CCAST]
Core.congr_cstar [in GhostTT.autosubst.CCAST]
Core.congr_ctop [in GhostTT.autosubst.CCAST]
Core.congr_ctt [in GhostTT.autosubst.CCAST]
Core.congr_cunit [in GhostTT.autosubst.CCAST]
Core.congr_capp [in GhostTT.autosubst.CCAST]
Core.congr_clam [in GhostTT.autosubst.CCAST]
Core.congr_cPi [in GhostTT.autosubst.CCAST]
Core.congr_cSort [in GhostTT.autosubst.CCAST]
Core.instId'_term_pointwise [in GhostTT.autosubst.GAST]
Core.instId'_term [in GhostTT.autosubst.GAST]
Core.instId'_cterm_pointwise [in GhostTT.autosubst.CCAST]
Core.instId'_cterm [in GhostTT.autosubst.CCAST]
Core.renRen_term [in GhostTT.autosubst.GAST]
Core.renRen_cterm [in GhostTT.autosubst.CCAST]
Core.renRen'_term_pointwise [in GhostTT.autosubst.GAST]
Core.renRen'_cterm_pointwise [in GhostTT.autosubst.CCAST]
Core.renSubst_term_pointwise [in GhostTT.autosubst.GAST]
Core.renSubst_term [in GhostTT.autosubst.GAST]
Core.renSubst_cterm_pointwise [in GhostTT.autosubst.CCAST]
Core.renSubst_cterm [in GhostTT.autosubst.CCAST]
Core.rinstId'_term_pointwise [in GhostTT.autosubst.GAST]
Core.rinstId'_term [in GhostTT.autosubst.GAST]
Core.rinstId'_cterm_pointwise [in GhostTT.autosubst.CCAST]
Core.rinstId'_cterm [in GhostTT.autosubst.CCAST]
Core.rinstInst_up_term_term [in GhostTT.autosubst.GAST]
Core.rinstInst_up_cterm_cterm [in GhostTT.autosubst.CCAST]
Core.rinstInst'_term_pointwise [in GhostTT.autosubst.GAST]
Core.rinstInst'_term [in GhostTT.autosubst.GAST]
Core.rinstInst'_cterm_pointwise [in GhostTT.autosubst.CCAST]
Core.rinstInst'_cterm [in GhostTT.autosubst.CCAST]
Core.substRen_term_pointwise [in GhostTT.autosubst.GAST]
Core.substRen_term [in GhostTT.autosubst.GAST]
Core.substRen_cterm_pointwise [in GhostTT.autosubst.CCAST]
Core.substRen_cterm [in GhostTT.autosubst.CCAST]
Core.substSubst_term_pointwise [in GhostTT.autosubst.GAST]
Core.substSubst_term [in GhostTT.autosubst.GAST]
Core.substSubst_cterm_pointwise [in GhostTT.autosubst.CCAST]
Core.substSubst_cterm [in GhostTT.autosubst.CCAST]
Core.upExtRen_term_term [in GhostTT.autosubst.GAST]
Core.upExtRen_cterm_cterm [in GhostTT.autosubst.CCAST]
Core.upExt_term_term [in GhostTT.autosubst.GAST]
Core.upExt_cterm_cterm [in GhostTT.autosubst.CCAST]
Core.upId_term_term [in GhostTT.autosubst.GAST]
Core.upId_cterm_cterm [in GhostTT.autosubst.CCAST]
Core.upRen_term_term [in GhostTT.autosubst.GAST]
Core.upRen_cterm_cterm [in GhostTT.autosubst.CCAST]
Core.up_subst_subst_term_term [in GhostTT.autosubst.GAST]
Core.up_subst_ren_term_term [in GhostTT.autosubst.GAST]
Core.up_ren_subst_term_term [in GhostTT.autosubst.GAST]
Core.up_ren_ren_term_term [in GhostTT.autosubst.GAST]
Core.up_term_term [in GhostTT.autosubst.GAST]
Core.up_subst_subst_cterm_cterm [in GhostTT.autosubst.CCAST]
Core.up_subst_ren_cterm_cterm [in GhostTT.autosubst.CCAST]
Core.up_ren_subst_cterm_cterm [in GhostTT.autosubst.CCAST]
Core.up_ren_ren_cterm_cterm [in GhostTT.autosubst.CCAST]
Core.up_cterm_cterm [in GhostTT.autosubst.CCAST]
Core.varLRen'_term_pointwise [in GhostTT.autosubst.GAST]
Core.varLRen'_term [in GhostTT.autosubst.GAST]
Core.varLRen'_cterm_pointwise [in GhostTT.autosubst.CCAST]
Core.varLRen'_cterm [in GhostTT.autosubst.CCAST]
Core.varL'_term_pointwise [in GhostTT.autosubst.GAST]
Core.varL'_term [in GhostTT.autosubst.GAST]
Core.varL'_cterm_pointwise [in GhostTT.autosubst.CCAST]
Core.varL'_cterm [in GhostTT.autosubst.CCAST]
crscoping_sscoping [in GhostTT.CCMetaTheory]
crscoping_shift_none [in GhostTT.CCMetaTheory]
crscoping_shift [in GhostTT.CCMetaTheory]
crscoping_plus [in GhostTT.CCMetaTheory]
crscoping_S [in GhostTT.CCMetaTheory]
crscoping_comp [in GhostTT.Revival]
crtyping_typing [in GhostTT.CCMetaTheory]
crtyping_S [in GhostTT.CCMetaTheory]
crtyping_upren_none [in GhostTT.CCMetaTheory]
crtyping_shift [in GhostTT.CCMetaTheory]
crtyping_cscoping [in GhostTT.CCMetaTheory]
crtyping_shift_eq [in GhostTT.Param]
crtyping_comp [in GhostTT.Erasure]
cscope_ignore [in GhostTT.CCMetaTheory]
cscope_close [in GhostTT.CCMetaTheory]
cscope_ty_lift [in GhostTT.Erasure]
cscoping_subst [in GhostTT.CCMetaTheory]
cscoping_ren [in GhostTT.CCMetaTheory]
csc_param_ctx [in GhostTT.Param]
csscoping_nones [in GhostTT.CCMetaTheory]
csscoping_one_none [in GhostTT.CCMetaTheory]
csscoping_one [in GhostTT.CCMetaTheory]
csscoping_ids [in GhostTT.CCMetaTheory]
csscoping_shift [in GhostTT.CCMetaTheory]
csscoping_weak [in GhostTT.CCMetaTheory]
cstyping_nones [in GhostTT.CCMetaTheory]
cstyping_one_none [in GhostTT.CCMetaTheory]
cstyping_one [in GhostTT.CCMetaTheory]
cstyping_ids [in GhostTT.CCMetaTheory]
cstyping_shift_none [in GhostTT.CCMetaTheory]
cstyping_shift [in GhostTT.CCMetaTheory]
cstyping_weak_none [in GhostTT.CCMetaTheory]
cstyping_weak [in GhostTT.CCMetaTheory]
cstyping_cscoping [in GhostTT.CCMetaTheory]
cstyping_shift_eq [in GhostTT.Param]
ctype_ignore [in GhostTT.CCMetaTheory]
ctype_close [in GhostTT.CCMetaTheory]
ctype_ty_lift [in GhostTT.Erasure]
ctyping_subst [in GhostTT.CCMetaTheory]
ctyping_ren [in GhostTT.CCMetaTheory]

D

div2_vpar [in GhostTT.Param]
div2_vreg [in GhostTT.Param]
div2_SS [in GhostTT.Param]

E

elim_ctx [in GhostTT.ElimReflection]
elim_reflection [in GhostTT.ElimReflection]
epm_lift_eq [in GhostTT.Param]
eq_subst_on_up [in GhostTT.CCMetaTheory]
erase_typing_eq [in GhostTT.Param]
erase_conv_eq [in GhostTT.Param]
erase_scoping_eq [in GhostTT.Param]
erase_rev_subst [in GhostTT.Revival]
erase_context [in GhostTT.Erasure]
erase_typing [in GhostTT.Erasure]
erase_typing_Err [in GhostTT.Erasure]
erase_typing_El [in GhostTT.Erasure]
erase_castrm_conv [in GhostTT.Erasure]
erase_castrm [in GhostTT.Erasure]
erase_conv [in GhostTT.Erasure]
erase_subst [in GhostTT.Erasure]
erase_ren [in GhostTT.Erasure]
erase_scoping [in GhostTT.Erasure]
erase_ctx_var [in GhostTT.Erasure]
erase_sc_var [in GhostTT.Erasure]
erase_irr [in GhostTT.Erasure]
err_nat_elim_S [in GhostTT.TransNat]
err_nat_elim_O [in GhostTT.TransNat]
err_nat_elim [in GhostTT.TransNat]
err_length_eq [in GhostTT.TransVec]
err_vec_elim_vcons [in GhostTT.TransVec]
err_vec_elim_vnil [in GhostTT.TransVec]
err_vec_elim [in GhostTT.TransVec]
eval_ren_sound [in GhostTT.autosubst.RAsimpl]
ext_cterm_scoped [in GhostTT.CCMetaTheory]

F

funcomp_assoc [in GhostTT.autosubst.core]

G

goal [in GhostTT.FreeTheorem]

I

isGhost_eq [in GhostTT.TermMode]
isKind_eq [in GhostTT.TermMode]
isProp_eq [in GhostTT.TermMode]
isType_eq [in GhostTT.TermMode]

M

md_subst [in GhostTT.BasicMetaTheory]
md_ren [in GhostTT.BasicMetaTheory]
md_castrm [in GhostTT.BasicMetaTheory]
meta_ccscoping_conv [in GhostTT.Param]
meta_ctx_param_conv [in GhostTT.Param]
meta_ctx_conv_conv [in GhostTT.Param]
meta_conv_refl [in GhostTT.BasicMetaTheory]
meta_conv_trans_r [in GhostTT.BasicMetaTheory]
meta_conv_trans_l [in GhostTT.BasicMetaTheory]
meta_conv [in GhostTT.BasicMetaTheory]
mode_coherence [in GhostTT.Model]

N

nth_app_r [in GhostTT.Util]
nth_error_skipn [in GhostTT.Util]
nth_skipn [in GhostTT.Util]
nth_error_app_r [in GhostTT.Util]
nth_error_param_vpar [in GhostTT.Param]
nth_error_param_vreg [in GhostTT.Param]
nth_nth_error [in GhostTT.BasicMetaTheory]

O

odd_vpar [in GhostTT.Param]
odd_vreg [in GhostTT.Param]

P

param_context [in GhostTT.Param]
param_pTypeGhost [in GhostTT.Param]
param_typing [in GhostTT.Param]
param_erase_typing_eq [in GhostTT.Param]
param_pKind_eq [in GhostTT.Param]
param_pKind [in GhostTT.Param]
param_pGhost_eq [in GhostTT.Param]
param_pGhost [in GhostTT.Param]
param_pType_eq [in GhostTT.Param]
param_pType [in GhostTT.Param]
param_pProp [in GhostTT.Param]
param_erase_err [in GhostTT.Param]
param_erase_ty [in GhostTT.Param]
param_erase_ty_tm [in GhostTT.Param]
param_revive_typing [in GhostTT.Param]
param_erase_typing [in GhostTT.Param]
param_ctx_vpar [in GhostTT.Param]
param_ctx_vreg [in GhostTT.Param]
param_castrm_conv [in GhostTT.Param]
param_castrm [in GhostTT.Param]
param_conv [in GhostTT.Param]
param_subst [in GhostTT.Param]
param_ren [in GhostTT.Param]
param_scoping [in GhostTT.Param]
pm_nat_elim_Prop [in GhostTT.TransNat]
pm_nat_elim [in GhostTT.TransNat]
pm_vec_elim_Prop [in GhostTT.TransVec]
pm_vec_elimG [in GhostTT.TransVec]
pm_vec_elim [in GhostTT.TransVec]
pointwise_forall [in GhostTT.autosubst.core]
pPi_scoping [in GhostTT.Param]
pren_plus [in GhostTT.Param]
pren_S_pw [in GhostTT.Param]
pren_S [in GhostTT.Param]
pren_rpm_lift [in GhostTT.Param]
pren_epm_lift [in GhostTT.Param]
pren_id [in GhostTT.Param]
pren_comp_S [in GhostTT.Param]
pren_SS [in GhostTT.Param]
pren_odd [in GhostTT.Param]
pren_even [in GhostTT.Param]
pscoping_revive [in GhostTT.Param]
pscoping_erase_err [in GhostTT.Param]
pscoping_erase_type [in GhostTT.Param]
pscoping_erase_term [in GhostTT.Param]
psubst_SS_id [in GhostTT.Param]
psubst_rpm_lift [in GhostTT.Param]
psubst_epm_lift [in GhostTT.Param]
psubst_SS' [in GhostTT.Param]
psubst_SS [in GhostTT.Param]

R

relative_consistency [in GhostTT.Model]
revive_typing_eq [in GhostTT.Param]
revive_conv_eq [in GhostTT.Param]
revive_scoping_eq [in GhostTT.Param]
revive_context [in GhostTT.Revival]
revive_typing [in GhostTT.Revival]
revive_ctx_var [in GhostTT.Revival]
revive_castrm_conv [in GhostTT.Revival]
revive_castrm [in GhostTT.Revival]
revive_conv [in GhostTT.Revival]
revive_subst [in GhostTT.Revival]
revive_ren [in GhostTT.Revival]
revive_scoping [in GhostTT.Revival]
revive_sc_var [in GhostTT.Revival]
revive_ng [in GhostTT.Revival]
rpm_lift_eq [in GhostTT.Param]
rscoping_sscoping [in GhostTT.BasicMetaTheory]
rscoping_comp_upren [in GhostTT.BasicMetaTheory]
rscoping_comp_S [in GhostTT.BasicMetaTheory]
rscoping_shift [in GhostTT.BasicMetaTheory]
rscoping_S [in GhostTT.BasicMetaTheory]
rscoping_comp_weak [in GhostTT.Erasure]
rscoping_upren [in GhostTT.Erasure]
rscoping_weak [in GhostTT.Erasure]
rtyping_triv [in GhostTT.Examples]
rtyping_S [in GhostTT.BasicMetaTheory]
rtyping_shift [in GhostTT.BasicMetaTheory]
rtyping_scoping [in GhostTT.BasicMetaTheory]

S

scons_comp' [in GhostTT.autosubst.unscoped]
scons_eta_id' [in GhostTT.autosubst.unscoped]
scons_eta' [in GhostTT.autosubst.unscoped]
scope_top [in GhostTT.BasicMetaTheory]
scope_bot_elim_inv [in GhostTT.BasicMetaTheory]
scope_if_inv [in GhostTT.BasicMetaTheory]
scope_gheq_inv [in GhostTT.BasicMetaTheory]
scope_hide_inv [in GhostTT.BasicMetaTheory]
scope_erased_inv [in GhostTT.BasicMetaTheory]
scope_pi_inv [in GhostTT.BasicMetaTheory]
scope_sort_inv [in GhostTT.BasicMetaTheory]
scope_fromRev_inv [in GhostTT.BasicMetaTheory]
scope_toRev_inv [in GhostTT.BasicMetaTheory]
scope_Reveal_inv [in GhostTT.BasicMetaTheory]
scope_reveal_inv [in GhostTT.BasicMetaTheory]
scope_lam_inv [in GhostTT.BasicMetaTheory]
scope_app_inv [in GhostTT.BasicMetaTheory]
scoping_functional [in GhostTT.TermMode]
scoping_md [in GhostTT.TermMode]
scoping_rpm_lift [in GhostTT.Param]
scoping_epm_lift [in GhostTT.Param]
scoping_er_sub_param [in GhostTT.Param]
scoping_rev_sub_param [in GhostTT.Param]
scoping_to_rev [in GhostTT.Revival]
scoping_sub_rev [in GhostTT.Revival]
scoping_castrm [in GhostTT.BasicMetaTheory]
scoping_subst [in GhostTT.BasicMetaTheory]
scoping_ren [in GhostTT.BasicMetaTheory]
sc_rmctx [in GhostTT.Potential]
sc_urm_ctx [in GhostTT.Model]
sort_mode_inj [in GhostTT.Model]
sscoping_urm [in GhostTT.Model]
sscoping_castrm [in GhostTT.BasicMetaTheory]
sscoping_comp_one [in GhostTT.BasicMetaTheory]
sscoping_comp_shift [in GhostTT.BasicMetaTheory]
sscoping_one [in GhostTT.BasicMetaTheory]
sscoping_ids [in GhostTT.BasicMetaTheory]
sscoping_shift [in GhostTT.BasicMetaTheory]
sscoping_weak [in GhostTT.BasicMetaTheory]
styping_one [in GhostTT.BasicMetaTheory]
styping_ids [in GhostTT.BasicMetaTheory]
styping_shift [in GhostTT.BasicMetaTheory]
styping_weak [in GhostTT.BasicMetaTheory]
styping_scoping [in GhostTT.BasicMetaTheory]

T

tr_gheq [in GhostTT.ElimReflection]
tr_Reveal [in GhostTT.ElimReflection]
tr_var [in GhostTT.ElimReflection]
tr_hide [in GhostTT.ElimReflection]
tr_ren_lax [in GhostTT.ElimReflection]
tr_ren [in GhostTT.ElimReflection]
tr_app_lax [in GhostTT.ElimReflection]
tr_app [in GhostTT.ElimReflection]
tr_sort_lax [in GhostTT.ElimReflection]
tr_sort [in GhostTT.ElimReflection]
tr_erased [in GhostTT.ElimReflection]
tr_bot [in GhostTT.ElimReflection]
tr_pi [in GhostTT.ElimReflection]
tr_choice [in GhostTT.Potential]
tr_scoping [in GhostTT.Potential]
tr_cons [in GhostTT.Potential]
tr_bot_eq [in GhostTT.Potential]
tr_sort_inv [in GhostTT.Potential]
tr_sort_eq [in GhostTT.Potential]
type_pi_opt [in GhostTT.Admissible]
type_conv_alt [in GhostTT.Admissible]
type_conv [in GhostTT.Admissible]
type_bot_elim [in GhostTT.Admissible]
type_if [in GhostTT.Admissible]
type_ghcast [in GhostTT.Admissible]
type_ghrefl [in GhostTT.Admissible]
type_gheq [in GhostTT.Admissible]
type_fromRev [in GhostTT.Admissible]
type_toRev [in GhostTT.Admissible]
type_Reveal [in GhostTT.Admissible]
type_reveal [in GhostTT.Admissible]
type_hide [in GhostTT.Admissible]
type_erased [in GhostTT.Admissible]
type_app [in GhostTT.Admissible]
type_lam [in GhostTT.Admissible]
type_pi [in GhostTT.Admissible]
type_discr [in GhostTT.Examples]
type_star_gen [in GhostTT.Examples]
type_star [in GhostTT.Examples]
type_gS [in GhostTT.Examples]
type_erased_nat_discrP_gen [in GhostTT.Examples]
type_erased_nat_discrP [in GhostTT.Examples]
type_discr_nat_gen [in GhostTT.Examples]
type_discr_nat [in GhostTT.Examples]
type_iszero_gen [in GhostTT.Examples]
type_iszero [in GhostTT.Examples]
type_discr_bool_gen [in GhostTT.Examples]
type_discr_bool [in GhostTT.Examples]
type_to_rev_eq [in GhostTT.Param]
type_pmPiNP_eq [in GhostTT.Param]
type_pmPiNP [in GhostTT.Param]
type_pProp [in GhostTT.Param]
type_pType [in GhostTT.Param]
type_pKind [in GhostTT.Param]
type_pmifK [in GhostTT.Param]
type_pmif [in GhostTT.Param]
type_perif [in GhostTT.Param]
type_pmPiP [in GhostTT.Param]
type_plam [in GhostTT.Param]
type_pPi [in GhostTT.Param]
type_pcastTG [in GhostTT.Param]
type_rpm_lift_eq [in GhostTT.Param]
type_rpm_lift [in GhostTT.Param]
type_epm_lift_eq [in GhostTT.Param]
type_epm_lift [in GhostTT.Param]
type_er_bool_cst [in GhostTT.FreeTheorem]
type_beq [in GhostTT.FreeTheorem]
type_to_rev [in GhostTT.Revival]
type_unique [in GhostTT.Model]
type_bot_elim_inv [in GhostTT.BasicMetaTheory]
type_bot_inv [in GhostTT.BasicMetaTheory]
type_vec_elim_inv [in GhostTT.BasicMetaTheory]
type_vcons_inv [in GhostTT.BasicMetaTheory]
type_vnil_inv [in GhostTT.BasicMetaTheory]
type_vec_inv [in GhostTT.BasicMetaTheory]
type_nat_elim_inv [in GhostTT.BasicMetaTheory]
type_succ_inv [in GhostTT.BasicMetaTheory]
type_zero_inv [in GhostTT.BasicMetaTheory]
type_nat_inv [in GhostTT.BasicMetaTheory]
type_if_inv [in GhostTT.BasicMetaTheory]
type_false_inv [in GhostTT.BasicMetaTheory]
type_true_inv [in GhostTT.BasicMetaTheory]
type_bool_inv [in GhostTT.BasicMetaTheory]
type_ghcast_inv [in GhostTT.BasicMetaTheory]
type_ghrefl_inv [in GhostTT.BasicMetaTheory]
type_gheq_inv [in GhostTT.BasicMetaTheory]
type_fromRev_inv [in GhostTT.BasicMetaTheory]
type_toRev_inv [in GhostTT.BasicMetaTheory]
type_Reveal_inv [in GhostTT.BasicMetaTheory]
type_reveal_inv [in GhostTT.BasicMetaTheory]
type_hide_inv [in GhostTT.BasicMetaTheory]
type_erased_inv [in GhostTT.BasicMetaTheory]
type_app_inv [in GhostTT.BasicMetaTheory]
type_lam_inv [in GhostTT.BasicMetaTheory]
type_pi_inv [in GhostTT.BasicMetaTheory]
type_sort_inv [in GhostTT.BasicMetaTheory]
type_var_inv [in GhostTT.BasicMetaTheory]
typing_er_sub_param [in GhostTT.Param]
typing_rev_sub_param [in GhostTT.Param]
typing_sub_rev [in GhostTT.Revival]
typing_subst [in GhostTT.BasicMetaTheory]
typing_ren [in GhostTT.BasicMetaTheory]

U

ueq_Ghost_eq [in GhostTT.Univ]
ueq_Type_eq [in GhostTT.Univ]
ueq_Kind_eq [in GhostTT.Univ]
ueq_eq [in GhostTT.Univ]
up_ren_ren [in GhostTT.autosubst.unscoped]
urm_conv_aux [in GhostTT.Model]
urm_cscoping [in GhostTT.Model]
urm_scoping [in GhostTT.Model]
urm_subst [in GhostTT.Model]
urm_ren [in GhostTT.Model]

V

validity [in GhostTT.BasicMetaTheory]
vreg_vpar_dec [in GhostTT.Param]

W

wf_cons [in GhostTT.Admissible]

Constructor Index

A

Any [in GhostTT.BasicAST]

C

ccong_pvec_elimP [in GhostTT.CTyping]
ccong_pvec_elimG [in GhostTT.CTyping]
ccong_pvec_elim [in GhostTT.CTyping]
ccong_pvcons [in GhostTT.CTyping]
ccong_pvnil [in GhostTT.CTyping]
ccong_pvec [in GhostTT.CTyping]
ccong_evec_elim [in GhostTT.CTyping]
ccong_evcons [in GhostTT.CTyping]
ccong_evnil [in GhostTT.CTyping]
ccong_evec [in GhostTT.CTyping]
ccong_pnat_elimP [in GhostTT.CTyping]
ccong_pnat_elim [in GhostTT.CTyping]
ccong_psucc [in GhostTT.CTyping]
ccong_enat_elim [in GhostTT.CTyping]
ccong_esucc [in GhostTT.CTyping]
ccong_pif [in GhostTT.CTyping]
ccong_eif [in GhostTT.CTyping]
ccong_tJ [in GhostTT.CTyping]
ccong_trefl [in GhostTT.CTyping]
ccong_teq [in GhostTT.CTyping]
ccong_squash [in GhostTT.CTyping]
ccong_Err [in GhostTT.CTyping]
ccong_El [in GhostTT.CTyping]
ccong_tyval [in GhostTT.CTyping]
ccong_bot_elim [in GhostTT.CTyping]
ccong_app [in GhostTT.CTyping]
ccong_clam [in GhostTT.CTyping]
ccong_Pi [in GhostTT.CTyping]
ccong_Prop [in GhostTT.CTyping]
cconv_irr [in GhostTT.CTyping]
cconv_trans [in GhostTT.CTyping]
cconv_sym [in GhostTT.CTyping]
cconv_refl [in GhostTT.CTyping]
cconv_evec_elim_cons [in GhostTT.CTyping]
cconv_evec_elim_nil [in GhostTT.CTyping]
cconv_enat_elim_succ [in GhostTT.CTyping]
cconv_enat_elim_zero [in GhostTT.CTyping]
cconv_pif_false [in GhostTT.CTyping]
cconv_pif_true [in GhostTT.CTyping]
cconv_if_err [in GhostTT.CTyping]
cconv_if_false [in GhostTT.CTyping]
cconv_if_true [in GhostTT.CTyping]
cconv_J_refl [in GhostTT.CTyping]
cconv_Err_err [in GhostTT.CTyping]
cconv_El_err [in GhostTT.CTyping]
cconv_Err_val [in GhostTT.CTyping]
cconv_El_val [in GhostTT.CTyping]
cconv_beta [in GhostTT.CTyping]
cong_bot_elim [in GhostTT.Typing]
cong_vec_elim [in GhostTT.Typing]
cong_vcons [in GhostTT.Typing]
cong_vnil [in GhostTT.Typing]
cong_vec [in GhostTT.Typing]
cong_nat_elim [in GhostTT.Typing]
cong_succ [in GhostTT.Typing]
cong_if [in GhostTT.Typing]
cong_gheq [in GhostTT.Typing]
cong_Reveal [in GhostTT.Typing]
cong_reveal [in GhostTT.Typing]
cong_hide [in GhostTT.Typing]
cong_Erased [in GhostTT.Typing]
cong_app [in GhostTT.Typing]
cong_lam [in GhostTT.Typing]
cong_Pi [in GhostTT.Typing]
cong_Prop [in GhostTT.Typing]
conv_irr [in GhostTT.Typing]
conv_trans [in GhostTT.Typing]
conv_sym [in GhostTT.Typing]
conv_refl [in GhostTT.Typing]
conv_vec_elim_cons [in GhostTT.Typing]
conv_vec_elim_nil [in GhostTT.Typing]
conv_nat_elim_succ [in GhostTT.Typing]
conv_nat_elim_zero [in GhostTT.Typing]
conv_if_false [in GhostTT.Typing]
conv_if_true [in GhostTT.Typing]
conv_beta [in GhostTT.Typing]
Core.app [in GhostTT.autosubst.GAST]
Core.bool_err [in GhostTT.autosubst.CCAST]
Core.bot [in GhostTT.autosubst.GAST]
Core.bot_elim [in GhostTT.autosubst.GAST]
Core.capp [in GhostTT.autosubst.CCAST]
Core.cbot [in GhostTT.autosubst.CCAST]
Core.cbot_elim [in GhostTT.autosubst.CCAST]
Core.cEl [in GhostTT.autosubst.CCAST]
Core.cErr [in GhostTT.autosubst.CCAST]
Core.clam [in GhostTT.autosubst.CCAST]
Core.cPi [in GhostTT.autosubst.CCAST]
Core.cSort [in GhostTT.autosubst.CCAST]
Core.cstar [in GhostTT.autosubst.CCAST]
Core.ctop [in GhostTT.autosubst.CCAST]
Core.ctt [in GhostTT.autosubst.CCAST]
Core.cty [in GhostTT.autosubst.CCAST]
Core.ctyerr [in GhostTT.autosubst.CCAST]
Core.ctyval [in GhostTT.autosubst.CCAST]
Core.cunit [in GhostTT.autosubst.CCAST]
Core.cvar [in GhostTT.autosubst.CCAST]
Core.ebool [in GhostTT.autosubst.CCAST]
Core.efalse [in GhostTT.autosubst.CCAST]
Core.eif [in GhostTT.autosubst.CCAST]
Core.enat [in GhostTT.autosubst.CCAST]
Core.enat_elim [in GhostTT.autosubst.CCAST]
Core.Erased [in GhostTT.autosubst.GAST]
Core.esucc [in GhostTT.autosubst.CCAST]
Core.etrue [in GhostTT.autosubst.CCAST]
Core.evcons [in GhostTT.autosubst.CCAST]
Core.evec [in GhostTT.autosubst.CCAST]
Core.evec_elim [in GhostTT.autosubst.CCAST]
Core.evnil [in GhostTT.autosubst.CCAST]
Core.ezero [in GhostTT.autosubst.CCAST]
Core.fromRev [in GhostTT.autosubst.GAST]
Core.ghcast [in GhostTT.autosubst.GAST]
Core.gheq [in GhostTT.autosubst.GAST]
Core.ghrefl [in GhostTT.autosubst.GAST]
Core.hide [in GhostTT.autosubst.GAST]
Core.lam [in GhostTT.autosubst.GAST]
Core.pbool [in GhostTT.autosubst.CCAST]
Core.pfalse [in GhostTT.autosubst.CCAST]
Core.Pi [in GhostTT.autosubst.GAST]
Core.pif [in GhostTT.autosubst.CCAST]
Core.pnat [in GhostTT.autosubst.CCAST]
Core.pnat_elimP [in GhostTT.autosubst.CCAST]
Core.pnat_elim [in GhostTT.autosubst.CCAST]
Core.psucc [in GhostTT.autosubst.CCAST]
Core.ptrue [in GhostTT.autosubst.CCAST]
Core.pvcons [in GhostTT.autosubst.CCAST]
Core.pvec [in GhostTT.autosubst.CCAST]
Core.pvec_elimP [in GhostTT.autosubst.CCAST]
Core.pvec_elimG [in GhostTT.autosubst.CCAST]
Core.pvec_elim [in GhostTT.autosubst.CCAST]
Core.pvnil [in GhostTT.autosubst.CCAST]
Core.pzero [in GhostTT.autosubst.CCAST]
Core.Reveal [in GhostTT.autosubst.GAST]
Core.reveal [in GhostTT.autosubst.GAST]
Core.Sort [in GhostTT.autosubst.GAST]
Core.sq [in GhostTT.autosubst.CCAST]
Core.squash [in GhostTT.autosubst.CCAST]
Core.sq_elim [in GhostTT.autosubst.CCAST]
Core.tbool [in GhostTT.autosubst.GAST]
Core.teq [in GhostTT.autosubst.CCAST]
Core.tfalse [in GhostTT.autosubst.GAST]
Core.tif [in GhostTT.autosubst.GAST]
Core.tJ [in GhostTT.autosubst.CCAST]
Core.tnat [in GhostTT.autosubst.GAST]
Core.tnat_elim [in GhostTT.autosubst.GAST]
Core.toRev [in GhostTT.autosubst.GAST]
Core.trefl [in GhostTT.autosubst.CCAST]
Core.tsucc [in GhostTT.autosubst.GAST]
Core.ttrue [in GhostTT.autosubst.GAST]
Core.tvcons [in GhostTT.autosubst.GAST]
Core.tvec [in GhostTT.autosubst.GAST]
Core.tvec_elim [in GhostTT.autosubst.GAST]
Core.tvnil [in GhostTT.autosubst.GAST]
Core.tzero [in GhostTT.autosubst.GAST]
Core.up_term [in GhostTT.autosubst.GAST]
Core.up_cterm [in GhostTT.autosubst.CCAST]
Core.var [in GhostTT.autosubst.GAST]
cProp [in GhostTT.BasicAST]
cscope_cons [in GhostTT.CCMetaTheory]
cscope_nil [in GhostTT.CCMetaTheory]
cscope_pvec_elimP [in GhostTT.CScoping]
cscope_pvec_elimG [in GhostTT.CScoping]
cscope_pvec_elim [in GhostTT.CScoping]
cscope_pvcons [in GhostTT.CScoping]
cscope_pvnil [in GhostTT.CScoping]
cscope_pvec [in GhostTT.CScoping]
cscope_evec_elim [in GhostTT.CScoping]
cscope_evcons [in GhostTT.CScoping]
cscope_evnil [in GhostTT.CScoping]
cscope_evec [in GhostTT.CScoping]
cscope_pnat_elimP [in GhostTT.CScoping]
cscope_pnat_elim [in GhostTT.CScoping]
cscope_psucc [in GhostTT.CScoping]
cscope_pzero [in GhostTT.CScoping]
cscope_pnat [in GhostTT.CScoping]
cscope_enat_elim [in GhostTT.CScoping]
cscope_esucc [in GhostTT.CScoping]
cscope_ezero [in GhostTT.CScoping]
cscope_enat [in GhostTT.CScoping]
cscope_pif [in GhostTT.CScoping]
cscope_pfalse [in GhostTT.CScoping]
cscope_ptrue [in GhostTT.CScoping]
cscope_pbool [in GhostTT.CScoping]
cscope_eif [in GhostTT.CScoping]
cscope_bool_err [in GhostTT.CScoping]
cscope_efalse [in GhostTT.CScoping]
cscope_etrue [in GhostTT.CScoping]
cscope_ebool [in GhostTT.CScoping]
cscope_tJ [in GhostTT.CScoping]
cscope_trefl [in GhostTT.CScoping]
cscope_teq [in GhostTT.CScoping]
cscope_sq_elim [in GhostTT.CScoping]
cscope_sq [in GhostTT.CScoping]
cscope_squash [in GhostTT.CScoping]
cscope_Err [in GhostTT.CScoping]
cscope_El [in GhostTT.CScoping]
cscope_tyerr [in GhostTT.CScoping]
cscope_tyval [in GhostTT.CScoping]
cscope_ty [in GhostTT.CScoping]
cscope_bot_elim [in GhostTT.CScoping]
cscope_bot [in GhostTT.CScoping]
cscope_star [in GhostTT.CScoping]
cscope_top [in GhostTT.CScoping]
cscope_tt [in GhostTT.CScoping]
cscope_unit [in GhostTT.CScoping]
cscope_app [in GhostTT.CScoping]
cscope_lam [in GhostTT.CScoping]
cscope_pi [in GhostTT.CScoping]
cscope_sort [in GhostTT.CScoping]
cscope_var [in GhostTT.CScoping]
cType [in GhostTT.BasicAST]
ctype_cons [in GhostTT.CCMetaTheory]
ctype_nil [in GhostTT.CCMetaTheory]
ctype_cumul [in GhostTT.CTyping]
ctype_conv [in GhostTT.CTyping]
ctype_pvec_elimP [in GhostTT.CTyping]
ctype_pvec_elimG [in GhostTT.CTyping]
ctype_pvec_elim [in GhostTT.CTyping]
ctype_pvcons [in GhostTT.CTyping]
ctype_pvnil [in GhostTT.CTyping]
ctype_pvec [in GhostTT.CTyping]
ctype_evec_elim [in GhostTT.CTyping]
ctype_evcons [in GhostTT.CTyping]
ctype_evnil [in GhostTT.CTyping]
ctype_evec [in GhostTT.CTyping]
ctype_pnat_elimP [in GhostTT.CTyping]
ctype_pnat_elim [in GhostTT.CTyping]
ctype_psucc [in GhostTT.CTyping]
ctype_pzero [in GhostTT.CTyping]
ctype_pnat [in GhostTT.CTyping]
ctype_enat_elim [in GhostTT.CTyping]
ctype_esucc [in GhostTT.CTyping]
ctype_ezero [in GhostTT.CTyping]
ctype_enat [in GhostTT.CTyping]
ctype_pif [in GhostTT.CTyping]
ctype_pfalse [in GhostTT.CTyping]
ctype_ptrue [in GhostTT.CTyping]
ctype_pbool [in GhostTT.CTyping]
ctype_eif [in GhostTT.CTyping]
ctype_bool_err [in GhostTT.CTyping]
ctype_efalse [in GhostTT.CTyping]
ctype_etrue [in GhostTT.CTyping]
ctype_ebool [in GhostTT.CTyping]
ctype_tJ [in GhostTT.CTyping]
ctype_trefl [in GhostTT.CTyping]
ctype_teq [in GhostTT.CTyping]
ctype_sq_elim [in GhostTT.CTyping]
ctype_sq [in GhostTT.CTyping]
ctype_squash [in GhostTT.CTyping]
ctype_Err [in GhostTT.CTyping]
ctype_El [in GhostTT.CTyping]
ctype_tyerr [in GhostTT.CTyping]
ctype_tyval [in GhostTT.CTyping]
ctype_ty [in GhostTT.CTyping]
ctype_bot_elim [in GhostTT.CTyping]
ctype_bot [in GhostTT.CTyping]
ctype_star [in GhostTT.CTyping]
ctype_top [in GhostTT.CTyping]
ctype_tt [in GhostTT.CTyping]
ctype_unit [in GhostTT.CTyping]
ctype_app [in GhostTT.CTyping]
ctype_lam [in GhostTT.CTyping]
ctype_pi [in GhostTT.CTyping]
ctype_sort [in GhostTT.CTyping]
ctype_var [in GhostTT.CTyping]
cwf_cons [in GhostTT.CTyping]
cwf_nil [in GhostTT.CTyping]

E

err [in GhostTT.FreeTheorem]
err_S [in GhostTT.TransNat]
err_O [in GhostTT.TransNat]
err_vcons [in GhostTT.TransVec]
err_vnil [in GhostTT.TransVec]
err_false [in GhostTT.FreeTheorem]
err_true [in GhostTT.FreeTheorem]
ers_other [in GhostTT.autosubst.CCAST_rasimpl]
ers_ren_r [in GhostTT.autosubst.CCAST_rasimpl]
ers_cons_r [in GhostTT.autosubst.CCAST_rasimpl]
ers_rcomp_r [in GhostTT.autosubst.CCAST_rasimpl]
ers_compr_r [in GhostTT.autosubst.CCAST_rasimpl]
ers_comp_r [in GhostTT.autosubst.CCAST_rasimpl]
ers_id_r [in GhostTT.autosubst.CCAST_rasimpl]
ers_id_l [in GhostTT.autosubst.CCAST_rasimpl]
ers_other [in GhostTT.autosubst.GAST_rasimpl]
ers_ren_r [in GhostTT.autosubst.GAST_rasimpl]
ers_cons_r [in GhostTT.autosubst.GAST_rasimpl]
ers_rcomp_r [in GhostTT.autosubst.GAST_rasimpl]
ers_compr_r [in GhostTT.autosubst.GAST_rasimpl]
ers_comp_r [in GhostTT.autosubst.GAST_rasimpl]
ers_id_r [in GhostTT.autosubst.GAST_rasimpl]
ers_id_l [in GhostTT.autosubst.GAST_rasimpl]
esr_other [in GhostTT.autosubst.CCAST_rasimpl]
esr_cons_shift [in GhostTT.autosubst.CCAST_rasimpl]
esr_ren_l [in GhostTT.autosubst.CCAST_rasimpl]
esr_cons_r [in GhostTT.autosubst.CCAST_rasimpl]
esr_comp_r [in GhostTT.autosubst.CCAST_rasimpl]
esr_id_r [in GhostTT.autosubst.CCAST_rasimpl]
esr_id_l [in GhostTT.autosubst.CCAST_rasimpl]
esr_other [in GhostTT.autosubst.GAST_rasimpl]
esr_cons_shift [in GhostTT.autosubst.GAST_rasimpl]
esr_ren_l [in GhostTT.autosubst.GAST_rasimpl]
esr_cons_r [in GhostTT.autosubst.GAST_rasimpl]
esr_comp_r [in GhostTT.autosubst.GAST_rasimpl]
esr_id_r [in GhostTT.autosubst.GAST_rasimpl]
esr_id_l [in GhostTT.autosubst.GAST_rasimpl]
es_other [in GhostTT.autosubst.CCAST_rasimpl]
es_ren_r [in GhostTT.autosubst.CCAST_rasimpl]
es_ren_l [in GhostTT.autosubst.CCAST_rasimpl]
es_cons_r [in GhostTT.autosubst.CCAST_rasimpl]
es_rcomp_r [in GhostTT.autosubst.CCAST_rasimpl]
es_compr_r [in GhostTT.autosubst.CCAST_rasimpl]
es_comp_r [in GhostTT.autosubst.CCAST_rasimpl]
es_id_r [in GhostTT.autosubst.CCAST_rasimpl]
es_id_l [in GhostTT.autosubst.CCAST_rasimpl]
es_other [in GhostTT.autosubst.GAST_rasimpl]
es_ren_r [in GhostTT.autosubst.GAST_rasimpl]
es_ren_l [in GhostTT.autosubst.GAST_rasimpl]
es_cons_r [in GhostTT.autosubst.GAST_rasimpl]
es_rcomp_r [in GhostTT.autosubst.GAST_rasimpl]
es_compr_r [in GhostTT.autosubst.GAST_rasimpl]
es_comp_r [in GhostTT.autosubst.GAST_rasimpl]
es_id_r [in GhostTT.autosubst.GAST_rasimpl]
es_id_l [in GhostTT.autosubst.GAST_rasimpl]
eval_ren_comp_other [in GhostTT.autosubst.RAsimpl]
eval_ren_cons_r [in GhostTT.autosubst.RAsimpl]
eval_ren_comp_r [in GhostTT.autosubst.RAsimpl]
eval_ren_cons_shift [in GhostTT.autosubst.RAsimpl]
eval_ren_id_r [in GhostTT.autosubst.RAsimpl]
eval_ren_id_l [in GhostTT.autosubst.RAsimpl]

I

ids [in GhostTT.autosubst.unscoped]
is_qsubst_id [in GhostTT.autosubst.CCAST_rasimpl]
is_qsubst_ren [in GhostTT.autosubst.CCAST_rasimpl]
is_qren_id [in GhostTT.autosubst.RAsimpl]
is_qsubst_id [in GhostTT.autosubst.GAST_rasimpl]
is_qsubst_ren [in GhostTT.autosubst.GAST_rasimpl]

M

mGhost [in GhostTT.BasicAST]
mKind [in GhostTT.BasicAST]
mProp [in GhostTT.BasicAST]
mType [in GhostTT.BasicAST]

N

nat_err [in GhostTT.TransNat]
not_qsubst_ren_id [in GhostTT.autosubst.CCAST_rasimpl]
not_qren_id [in GhostTT.autosubst.RAsimpl]
not_qsubst_ren_id [in GhostTT.autosubst.GAST_rasimpl]

O

O [in GhostTT.TransNat]

P

pm_S [in GhostTT.TransNat]
pm_O [in GhostTT.TransNat]
pm_vcons [in GhostTT.TransVec]
pm_vnil [in GhostTT.TransVec]
pm_false [in GhostTT.FreeTheorem]
pm_true [in GhostTT.FreeTheorem]

Q

qatom [in GhostTT.autosubst.CCAST_rasimpl]
qatom [in GhostTT.autosubst.GAST_rasimpl]
qnat_atom [in GhostTT.autosubst.RAsimpl]
qren [in GhostTT.autosubst.CCAST_rasimpl]
qren [in GhostTT.autosubst.GAST_rasimpl]
qren_shift [in GhostTT.autosubst.RAsimpl]
qren_id [in GhostTT.autosubst.RAsimpl]
qren_cons [in GhostTT.autosubst.RAsimpl]
qren_comp [in GhostTT.autosubst.RAsimpl]
qren_atom [in GhostTT.autosubst.RAsimpl]
qS [in GhostTT.autosubst.RAsimpl]
qsubst [in GhostTT.autosubst.CCAST_rasimpl]
qsubst [in GhostTT.autosubst.GAST_rasimpl]
qsubst_ren [in GhostTT.autosubst.CCAST_rasimpl]
qsubst_id [in GhostTT.autosubst.CCAST_rasimpl]
qsubst_cons [in GhostTT.autosubst.CCAST_rasimpl]
qsubst_rcomp [in GhostTT.autosubst.CCAST_rasimpl]
qsubst_compr [in GhostTT.autosubst.CCAST_rasimpl]
qsubst_comp [in GhostTT.autosubst.CCAST_rasimpl]
qsubst_atom [in GhostTT.autosubst.CCAST_rasimpl]
qsubst_ren [in GhostTT.autosubst.GAST_rasimpl]
qsubst_id [in GhostTT.autosubst.GAST_rasimpl]
qsubst_cons [in GhostTT.autosubst.GAST_rasimpl]
qsubst_rcomp [in GhostTT.autosubst.GAST_rasimpl]
qsubst_compr [in GhostTT.autosubst.GAST_rasimpl]
qsubst_comp [in GhostTT.autosubst.GAST_rasimpl]
qsubst_atom [in GhostTT.autosubst.GAST_rasimpl]
q0 [in GhostTT.autosubst.RAsimpl]

R

reflection [in GhostTT.RTyping]
ren1 [in GhostTT.autosubst.unscoped]
ren2 [in GhostTT.autosubst.unscoped]
ren3 [in GhostTT.autosubst.unscoped]
ren4 [in GhostTT.autosubst.unscoped]
ren5 [in GhostTT.autosubst.unscoped]
reveal_hide [in GhostTT.Typing]
rtype_conv [in GhostTT.RTyping]
rtype_bot_elim [in GhostTT.RTyping]
rtype_bot [in GhostTT.RTyping]
rtype_ghrefl [in GhostTT.RTyping]
rtype_gheq [in GhostTT.RTyping]
rtype_fromRev [in GhostTT.RTyping]
rtype_toRev [in GhostTT.RTyping]
rtype_Reveal [in GhostTT.RTyping]
rtype_reveal [in GhostTT.RTyping]
rtype_hide [in GhostTT.RTyping]
rtype_erased [in GhostTT.RTyping]
rtype_app [in GhostTT.RTyping]
rtype_lam [in GhostTT.RTyping]
rtype_pi [in GhostTT.RTyping]
rtype_sort [in GhostTT.RTyping]
rtype_var [in GhostTT.RTyping]
rwf_cons [in GhostTT.RTyping]
rwf_nil [in GhostTT.RTyping]

S

S [in GhostTT.TransNat]
scope_bot_elim [in GhostTT.Scoping]
scope_bot [in GhostTT.Scoping]
scope_vec_elim [in GhostTT.Scoping]
scope_vcons [in GhostTT.Scoping]
scope_vnil [in GhostTT.Scoping]
scope_vec [in GhostTT.Scoping]
scope_nat_elim [in GhostTT.Scoping]
scope_succ [in GhostTT.Scoping]
scope_zero [in GhostTT.Scoping]
scope_nat [in GhostTT.Scoping]
scope_if [in GhostTT.Scoping]
scope_false [in GhostTT.Scoping]
scope_true [in GhostTT.Scoping]
scope_bool [in GhostTT.Scoping]
scope_ghcast [in GhostTT.Scoping]
scope_ghrefl [in GhostTT.Scoping]
scope_gheq [in GhostTT.Scoping]
scope_fromRev [in GhostTT.Scoping]
scope_toRev [in GhostTT.Scoping]
scope_Reveal [in GhostTT.Scoping]
scope_reveal [in GhostTT.Scoping]
scope_hide [in GhostTT.Scoping]
scope_erased [in GhostTT.Scoping]
scope_app [in GhostTT.Scoping]
scope_lam [in GhostTT.Scoping]
scope_pi [in GhostTT.Scoping]
scope_var [in GhostTT.Scoping]
scope_cons [in GhostTT.BasicMetaTheory]
scope_nil [in GhostTT.BasicMetaTheory]
scpoe_sort [in GhostTT.Scoping]
SI [in GhostTT.FreeTheorem]
sq [in GhostTT.TransVec]
subst1 [in GhostTT.autosubst.unscoped]
subst2 [in GhostTT.autosubst.unscoped]
subst3 [in GhostTT.autosubst.unscoped]
subst4 [in GhostTT.autosubst.unscoped]
subst5 [in GhostTT.autosubst.unscoped]

T

tyerr [in GhostTT.TransNat]
type_cons [in GhostTT.BasicMetaTheory]
type_nil [in GhostTT.BasicMetaTheory]
type_conv [in GhostTT.Typing]
type_bot_elim [in GhostTT.Typing]
type_bot [in GhostTT.Typing]
type_vec_elim [in GhostTT.Typing]
type_vcons [in GhostTT.Typing]
type_vnil [in GhostTT.Typing]
type_vec [in GhostTT.Typing]
type_nat_elim [in GhostTT.Typing]
type_succ [in GhostTT.Typing]
type_zero [in GhostTT.Typing]
type_nat [in GhostTT.Typing]
type_if [in GhostTT.Typing]
type_false [in GhostTT.Typing]
type_true [in GhostTT.Typing]
type_bool [in GhostTT.Typing]
type_ghcast [in GhostTT.Typing]
type_ghrefl [in GhostTT.Typing]
type_gheq [in GhostTT.Typing]
type_fromRev [in GhostTT.Typing]
type_toRev [in GhostTT.Typing]
type_Reveal [in GhostTT.Typing]
type_reveal [in GhostTT.Typing]
type_hide [in GhostTT.Typing]
type_erased [in GhostTT.Typing]
type_app [in GhostTT.Typing]
type_lam [in GhostTT.Typing]
type_pi [in GhostTT.Typing]
type_sort [in GhostTT.Typing]
type_var [in GhostTT.Typing]
tyval [in GhostTT.TransNat]

V

vec_err [in GhostTT.TransVec]

W

WasGhost [in GhostTT.BasicAST]
WasKind [in GhostTT.BasicAST]
WasType [in GhostTT.BasicAST]
wf_cons [in GhostTT.Typing]
wf_nil [in GhostTT.Typing]

Axiom Index

C

ctyval_inj [in GhostTT.Model]

P

pi_inj [in GhostTT.Model]

Inductive Index

C

ccscoping [in GhostTT.CScoping]
cmode [in GhostTT.BasicAST]
conversion [in GhostTT.CTyping]
conversion [in GhostTT.Typing]
Core.cterm [in GhostTT.autosubst.CCAST]
Core.term [in GhostTT.autosubst.GAST]
Core.Up_term [in GhostTT.autosubst.GAST]
Core.Up_cterm [in GhostTT.autosubst.CCAST]
csscoping [in GhostTT.CCMetaTheory]
cstyping [in GhostTT.CCMetaTheory]
ctyping [in GhostTT.CTyping]
cwf [in GhostTT.CTyping]

E

err_nat [in GhostTT.TransNat]
err_vec [in GhostTT.TransVec]
err_bool [in GhostTT.FreeTheorem]
eval_subst_rcomp_view [in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_compr_view [in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_comp_view [in GhostTT.autosubst.CCAST_rasimpl]
eval_ren_comp_view [in GhostTT.autosubst.RAsimpl]
eval_subst_rcomp_view [in GhostTT.autosubst.GAST_rasimpl]
eval_subst_compr_view [in GhostTT.autosubst.GAST_rasimpl]
eval_subst_comp_view [in GhostTT.autosubst.GAST_rasimpl]

G

grtyping [in GhostTT.RTyping]

M

mark [in GhostTT.BasicAST]
mode [in GhostTT.BasicAST]

N

nat [in GhostTT.TransNat]

P

pm_nat [in GhostTT.TransNat]
pm_vec [in GhostTT.TransVec]
pm_bool [in GhostTT.FreeTheorem]

Q

qren_id_view [in GhostTT.autosubst.RAsimpl]
qsubst_ren_id_view [in GhostTT.autosubst.CCAST_rasimpl]
qsubst_ren_id_view [in GhostTT.autosubst.GAST_rasimpl]
quoted_cterm [in GhostTT.autosubst.CCAST_rasimpl]
quoted_subst [in GhostTT.autosubst.CCAST_rasimpl]
quoted_ren [in GhostTT.autosubst.RAsimpl]
quoted_nat [in GhostTT.autosubst.RAsimpl]
quoted_term [in GhostTT.autosubst.GAST_rasimpl]
quoted_subst [in GhostTT.autosubst.GAST_rasimpl]

R

Ren1 [in GhostTT.autosubst.unscoped]
Ren2 [in GhostTT.autosubst.unscoped]
Ren3 [in GhostTT.autosubst.unscoped]
Ren4 [in GhostTT.autosubst.unscoped]
Ren5 [in GhostTT.autosubst.unscoped]
rwf [in GhostTT.RTyping]

S

scoping [in GhostTT.Scoping]
SFalse [in GhostTT.FreeTheorem]
squash [in GhostTT.TransVec]
sscoping [in GhostTT.BasicMetaTheory]
STrue [in GhostTT.FreeTheorem]
styping [in GhostTT.BasicMetaTheory]
Subst1 [in GhostTT.autosubst.unscoped]
Subst2 [in GhostTT.autosubst.unscoped]
Subst3 [in GhostTT.autosubst.unscoped]
Subst4 [in GhostTT.autosubst.unscoped]
Subst5 [in GhostTT.autosubst.unscoped]

T

ty [in GhostTT.TransNat]
typing [in GhostTT.Typing]

V

Var [in GhostTT.autosubst.unscoped]

W

wf [in GhostTT.Typing]

Projection Index

A

autosubst_simpl_csubst [in GhostTT.autosubst.CCAST_rasimpl]
autosubst_simpl_cterm [in GhostTT.autosubst.CCAST_rasimpl]
autosubst_simpl_ren [in GhostTT.autosubst.RAsimpl]
autosubst_simpl_csubst [in GhostTT.autosubst.GAST_rasimpl]
autosubst_simpl_term [in GhostTT.autosubst.GAST_rasimpl]

C

Core.up_term [in GhostTT.autosubst.GAST]
Core.up_cterm [in GhostTT.autosubst.CCAST]

I

ids [in GhostTT.autosubst.unscoped]

R

ren1 [in GhostTT.autosubst.unscoped]
ren2 [in GhostTT.autosubst.unscoped]
ren3 [in GhostTT.autosubst.unscoped]
ren4 [in GhostTT.autosubst.unscoped]
ren5 [in GhostTT.autosubst.unscoped]

S

subst1 [in GhostTT.autosubst.unscoped]
subst2 [in GhostTT.autosubst.unscoped]
subst3 [in GhostTT.autosubst.unscoped]
subst4 [in GhostTT.autosubst.unscoped]
subst5 [in GhostTT.autosubst.unscoped]

Section Index

A

Admissible [in GhostTT.Admissible]

I

Inb [in GhostTT.Util]

M

Mode [in GhostTT.TermMode]

Instance Index

C

Core.ren_term_morphism2 [in GhostTT.autosubst.GAST]
Core.ren_term_morphism [in GhostTT.autosubst.GAST]
Core.Ren_term [in GhostTT.autosubst.GAST]
Core.ren_cterm_morphism2 [in GhostTT.autosubst.CCAST]
Core.ren_cterm_morphism [in GhostTT.autosubst.CCAST]
Core.Ren_cterm [in GhostTT.autosubst.CCAST]
Core.subst_term_morphism2 [in GhostTT.autosubst.GAST]
Core.subst_term_morphism [in GhostTT.autosubst.GAST]
Core.Subst_term [in GhostTT.autosubst.GAST]
Core.subst_cterm_morphism2 [in GhostTT.autosubst.CCAST]
Core.subst_cterm_morphism [in GhostTT.autosubst.CCAST]
Core.Subst_cterm [in GhostTT.autosubst.CCAST]
Core.Up_term_term [in GhostTT.autosubst.GAST]
Core.Up_cterm_cterm [in GhostTT.autosubst.CCAST]
Core.VarInstance_term [in GhostTT.autosubst.GAST]
Core.VarInstance_cterm [in GhostTT.autosubst.CCAST]
crscoping_morphism [in GhostTT.CCMetaTheory]
crtyping_morphism [in GhostTT.CCMetaTheory]
csscoping_morphism [in GhostTT.CCMetaTheory]

F

funcomp_morphism2 [in GhostTT.autosubst.core]
funcomp_morphism [in GhostTT.autosubst.core]

I

idsRen [in GhostTT.autosubst.unscoped]

R

rscoping_morphism [in GhostTT.BasicMetaTheory]
rtyping_morphism [in GhostTT.BasicMetaTheory]

S

scons_morphism2 [in GhostTT.autosubst.unscoped]
scons_morphism [in GhostTT.autosubst.unscoped]
sscoping_morphism [in GhostTT.BasicMetaTheory]
styping_morphism [in GhostTT.CCMetaTheory]
styping_morphism [in GhostTT.BasicMetaTheory]

Abbreviation Index

C

ccontext [in GhostTT.ContextDecl]
ccxscoping [in GhostTT.CScoping]
cdecl [in GhostTT.ContextDecl]
context [in GhostTT.ContextDecl]
cscope [in GhostTT.ContextDecl]
cscoping [in GhostTT.Scoping]

D

decl [in GhostTT.ContextDecl]

M

mdc [in GhostTT.TermMode]

S

scope [in GhostTT.ContextDecl]

T

top [in GhostTT.TermNotations]

Definition Index

A

Allfv.allfvImpl_term [in GhostTT.autosubst.GAST]
Allfv.allfvImpl_cterm [in GhostTT.autosubst.CCAST]
Allfv.allfvRenL_term [in GhostTT.autosubst.GAST]
Allfv.allfvRenL_cterm [in GhostTT.autosubst.CCAST]
Allfv.allfvRenR_term [in GhostTT.autosubst.GAST]
Allfv.allfvRenR_cterm [in GhostTT.autosubst.CCAST]
Allfv.allfvTriv_term [in GhostTT.autosubst.GAST]
Allfv.allfvTriv_cterm [in GhostTT.autosubst.CCAST]
Allfv.allfv_term [in GhostTT.autosubst.GAST]
Allfv.allfv_cterm [in GhostTT.autosubst.CCAST]
ap [in GhostTT.autosubst.unscoped]
apc [in GhostTT.autosubst.unscoped]
apply_subst [in GhostTT.autosubst.CCAST_rasimpl]
apply_ren [in GhostTT.autosubst.RAsimpl]
apply_subst [in GhostTT.autosubst.GAST_rasimpl]

B

beq [in GhostTT.FreeTheorem]

C

capps [in GhostTT.CTyping]
castrm [in GhostTT.CastRemoval]
ccscoping_sind [in GhostTT.CScoping]
ccscoping_ind [in GhostTT.CScoping]
cc_consistency [in GhostTT.Model]
cDummy [in GhostTT.Erasure]
close [in GhostTT.CCMetaTheory]
cmode_sind [in GhostTT.BasicAST]
cmode_rec [in GhostTT.BasicAST]
cmode_ind [in GhostTT.BasicAST]
cmode_rect [in GhostTT.BasicAST]
conversion_sind [in GhostTT.CTyping]
conversion_ind [in GhostTT.CTyping]
conversion_sind [in GhostTT.Typing]
conversion_ind [in GhostTT.Typing]
Core.compRenRen_term [in GhostTT.autosubst.GAST]
Core.compRenRen_cterm [in GhostTT.autosubst.CCAST]
Core.compRenSubst_term [in GhostTT.autosubst.GAST]
Core.compRenSubst_cterm [in GhostTT.autosubst.CCAST]
Core.compSubstRen_term [in GhostTT.autosubst.GAST]
Core.compSubstRen_cterm [in GhostTT.autosubst.CCAST]
Core.compSubstSubst_term [in GhostTT.autosubst.GAST]
Core.compSubstSubst_cterm [in GhostTT.autosubst.CCAST]
Core.cterm_sind [in GhostTT.autosubst.CCAST]
Core.cterm_rec [in GhostTT.autosubst.CCAST]
Core.cterm_ind [in GhostTT.autosubst.CCAST]
Core.cterm_rect [in GhostTT.autosubst.CCAST]
Core.extRen_term [in GhostTT.autosubst.GAST]
Core.extRen_cterm [in GhostTT.autosubst.CCAST]
Core.ext_term [in GhostTT.autosubst.GAST]
Core.ext_cterm [in GhostTT.autosubst.CCAST]
Core.idSubst_term [in GhostTT.autosubst.GAST]
Core.idSubst_cterm [in GhostTT.autosubst.CCAST]
Core.ren_term [in GhostTT.autosubst.GAST]
Core.ren_cterm [in GhostTT.autosubst.CCAST]
Core.rinst_inst_term [in GhostTT.autosubst.GAST]
Core.rinst_inst_cterm [in GhostTT.autosubst.CCAST]
Core.subst_term [in GhostTT.autosubst.GAST]
Core.subst_cterm [in GhostTT.autosubst.CCAST]
Core.term_sind [in GhostTT.autosubst.GAST]
Core.term_rec [in GhostTT.autosubst.GAST]
Core.term_ind [in GhostTT.autosubst.GAST]
Core.term_rect [in GhostTT.autosubst.GAST]
crscoping [in GhostTT.CCMetaTheory]
crtyping [in GhostTT.CCMetaTheory]
csc [in GhostTT.ContextDecl]
csscoping_sind [in GhostTT.CCMetaTheory]
csscoping_ind [in GhostTT.CCMetaTheory]
cstyping_sind [in GhostTT.CCMetaTheory]
cstyping_ind [in GhostTT.CCMetaTheory]
cst_ty [in GhostTT.FreeTheorem]
ctyping_sind [in GhostTT.CTyping]
ctyping_ind [in GhostTT.CTyping]
cty_lift [in GhostTT.Erasure]
cumax [in GhostTT.CTyping]
cusup [in GhostTT.CTyping]
cwf_sind [in GhostTT.CTyping]
cwf_ind [in GhostTT.CTyping]

D

discr [in GhostTT.Examples]
discr_nat [in GhostTT.Examples]
discr_bool [in GhostTT.Examples]

E

El [in GhostTT.TransNat]
elength [in GhostTT.CTyping]
epm_lift [in GhostTT.Param]
eq_subst_on [in GhostTT.CCMetaTheory]
erased_nat_discrP [in GhostTT.Examples]
erase_S [in GhostTT.TransNat]
erase_O [in GhostTT.TransNat]
erase_nat [in GhostTT.TransNat]
erase_sc [in GhostTT.Erasure]
erase_ctx [in GhostTT.Erasure]
erase_term [in GhostTT.Erasure]
Err [in GhostTT.TransNat]
err_nat_sind [in GhostTT.TransNat]
err_nat_rec [in GhostTT.TransNat]
err_nat_ind [in GhostTT.TransNat]
err_nat_rect [in GhostTT.TransNat]
err_length [in GhostTT.TransVec]
err_vec_sind [in GhostTT.TransVec]
err_vec_rec [in GhostTT.TransVec]
err_vec_ind [in GhostTT.TransVec]
err_vec_rect [in GhostTT.TransVec]
err_bool_sind [in GhostTT.FreeTheorem]
err_bool_rec [in GhostTT.FreeTheorem]
err_bool_ind [in GhostTT.FreeTheorem]
err_bool_rect [in GhostTT.FreeTheorem]
er_bool_cst [in GhostTT.FreeTheorem]
eval_cterm_sound [in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_sound [in GhostTT.autosubst.CCAST_rasimpl]
eval_cterm [in GhostTT.autosubst.CCAST_rasimpl]
eval_subst [in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_rcomp_c [in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_rcomp_view_sind [in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_rcomp_view_rec [in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_rcomp_view_ind [in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_rcomp_view_rect [in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_compr_c [in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_compr_view_sind [in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_compr_view_rec [in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_compr_view_ind [in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_compr_view_rect [in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_comp_c [in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_comp_view_sind [in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_comp_view_rec [in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_comp_view_ind [in GhostTT.autosubst.CCAST_rasimpl]
eval_subst_comp_view_rect [in GhostTT.autosubst.CCAST_rasimpl]
eval_ren [in GhostTT.autosubst.RAsimpl]
eval_ren_comp_c [in GhostTT.autosubst.RAsimpl]
eval_ren_comp_view_sind [in GhostTT.autosubst.RAsimpl]
eval_ren_comp_view_rec [in GhostTT.autosubst.RAsimpl]
eval_ren_comp_view_ind [in GhostTT.autosubst.RAsimpl]
eval_ren_comp_view_rect [in GhostTT.autosubst.RAsimpl]
eval_term_sound [in GhostTT.autosubst.GAST_rasimpl]
eval_subst_sound [in GhostTT.autosubst.GAST_rasimpl]
eval_term [in GhostTT.autosubst.GAST_rasimpl]
eval_subst [in GhostTT.autosubst.GAST_rasimpl]
eval_subst_rcomp_c [in GhostTT.autosubst.GAST_rasimpl]
eval_subst_rcomp_view_sind [in GhostTT.autosubst.GAST_rasimpl]
eval_subst_rcomp_view_rec [in GhostTT.autosubst.GAST_rasimpl]
eval_subst_rcomp_view_ind [in GhostTT.autosubst.GAST_rasimpl]
eval_subst_rcomp_view_rect [in GhostTT.autosubst.GAST_rasimpl]
eval_subst_compr_c [in GhostTT.autosubst.GAST_rasimpl]
eval_subst_compr_view_sind [in GhostTT.autosubst.GAST_rasimpl]
eval_subst_compr_view_rec [in GhostTT.autosubst.GAST_rasimpl]
eval_subst_compr_view_ind [in GhostTT.autosubst.GAST_rasimpl]
eval_subst_compr_view_rect [in GhostTT.autosubst.GAST_rasimpl]
eval_subst_comp_c [in GhostTT.autosubst.GAST_rasimpl]
eval_subst_comp_view_sind [in GhostTT.autosubst.GAST_rasimpl]
eval_subst_comp_view_rec [in GhostTT.autosubst.GAST_rasimpl]
eval_subst_comp_view_ind [in GhostTT.autosubst.GAST_rasimpl]
eval_subst_comp_view_rect [in GhostTT.autosubst.GAST_rasimpl]

F

funcomp [in GhostTT.autosubst.core]

G

ghv [in GhostTT.Revival]
glength [in GhostTT.Typing]
grtt_consistency [in GhostTT.ElimReflection]
grtyping_sind [in GhostTT.RTyping]
grtyping_rec [in GhostTT.RTyping]
grtyping_ind [in GhostTT.RTyping]
grtyping_rect [in GhostTT.RTyping]
gS [in GhostTT.Typing]
gtt_consistency [in GhostTT.Model]

I

id [in GhostTT.autosubst.unscoped]
ignore [in GhostTT.CCMetaTheory]
inb [in GhostTT.Util]
inclb [in GhostTT.Util]
inscope [in GhostTT.CCMetaTheory]
inv [in GhostTT.FreeTheorem]
iscProp [in GhostTT.CTyping]
isGhost [in GhostTT.TermMode]
isKind [in GhostTT.TermMode]
isProp [in GhostTT.TermMode]
isType [in GhostTT.TermMode]
isType [in GhostTT.CTyping]
iszero [in GhostTT.Examples]

L

level [in GhostTT.BasicAST]
list_comp [in GhostTT.autosubst.core]
list_id [in GhostTT.autosubst.core]
list_ext [in GhostTT.autosubst.core]

M

mark_sind [in GhostTT.BasicAST]
mark_rec [in GhostTT.BasicAST]
mark_ind [in GhostTT.BasicAST]
mark_rect [in GhostTT.BasicAST]
md [in GhostTT.TermMode]
mdmk [in GhostTT.Erasure]
mode_eqb [in GhostTT.TermMode]
mode_sind [in GhostTT.BasicAST]
mode_rec [in GhostTT.BasicAST]
mode_ind [in GhostTT.BasicAST]
mode_rect [in GhostTT.BasicAST]

N

nat_sind [in GhostTT.TransNat]
nat_rec [in GhostTT.TransNat]
nat_ind [in GhostTT.TransNat]
nat_rect [in GhostTT.TransNat]
nones [in GhostTT.CCMetaTheory]

O

option_bind [in GhostTT.Util]
option_comp [in GhostTT.autosubst.core]
option_ext [in GhostTT.autosubst.core]
option_id [in GhostTT.autosubst.core]
option_map [in GhostTT.autosubst.core]

P

param_sc [in GhostTT.Param]
param_ctx [in GhostTT.Param]
param_term [in GhostTT.Param]
pbool_bool_err_inv [in GhostTT.Param]
pcastP [in GhostTT.Param]
pcastTG [in GhostTT.Param]
perif [in GhostTT.Param]
pKind [in GhostTT.Param]
plam [in GhostTT.Param]
pmif [in GhostTT.Param]
pmifK [in GhostTT.Param]
pmPi [in GhostTT.Param]
pmPiNP [in GhostTT.Param]
pmPiP [in GhostTT.Param]
pm_nat_sind [in GhostTT.TransNat]
pm_vec_sind [in GhostTT.TransVec]
pm_bool_sind [in GhostTT.FreeTheorem]
pPi [in GhostTT.Param]
pProp [in GhostTT.Param]
pren [in GhostTT.Param]
prod_comp [in GhostTT.autosubst.core]
prod_ext [in GhostTT.autosubst.core]
prod_id [in GhostTT.autosubst.core]
prod_map [in GhostTT.autosubst.core]
psubst [in GhostTT.Param]
ptype [in GhostTT.Param]
pType [in GhostTT.Param]

Q

qren_id_view_sind [in GhostTT.autosubst.RAsimpl]
qren_id_view_rec [in GhostTT.autosubst.RAsimpl]
qren_id_view_ind [in GhostTT.autosubst.RAsimpl]
qren_id_view_rect [in GhostTT.autosubst.RAsimpl]
qsubst_ren_id_view_sind [in GhostTT.autosubst.CCAST_rasimpl]
qsubst_ren_id_view_rec [in GhostTT.autosubst.CCAST_rasimpl]
qsubst_ren_id_view_ind [in GhostTT.autosubst.CCAST_rasimpl]
qsubst_ren_id_view_rect [in GhostTT.autosubst.CCAST_rasimpl]
qsubst_ren_id_view_sind [in GhostTT.autosubst.GAST_rasimpl]
qsubst_ren_id_view_rec [in GhostTT.autosubst.GAST_rasimpl]
qsubst_ren_id_view_ind [in GhostTT.autosubst.GAST_rasimpl]
qsubst_ren_id_view_rect [in GhostTT.autosubst.GAST_rasimpl]
quoted_cterm_sind [in GhostTT.autosubst.CCAST_rasimpl]
quoted_cterm_rec [in GhostTT.autosubst.CCAST_rasimpl]
quoted_cterm_ind [in GhostTT.autosubst.CCAST_rasimpl]
quoted_cterm_rect [in GhostTT.autosubst.CCAST_rasimpl]
quoted_subst_sind [in GhostTT.autosubst.CCAST_rasimpl]
quoted_subst_rec [in GhostTT.autosubst.CCAST_rasimpl]
quoted_subst_ind [in GhostTT.autosubst.CCAST_rasimpl]
quoted_subst_rect [in GhostTT.autosubst.CCAST_rasimpl]
quoted_ren_sind [in GhostTT.autosubst.RAsimpl]
quoted_ren_rec [in GhostTT.autosubst.RAsimpl]
quoted_ren_ind [in GhostTT.autosubst.RAsimpl]
quoted_ren_rect [in GhostTT.autosubst.RAsimpl]
quoted_nat_sind [in GhostTT.autosubst.RAsimpl]
quoted_nat_rec [in GhostTT.autosubst.RAsimpl]
quoted_nat_ind [in GhostTT.autosubst.RAsimpl]
quoted_nat_rect [in GhostTT.autosubst.RAsimpl]
quoted_term_sind [in GhostTT.autosubst.GAST_rasimpl]
quoted_term_rec [in GhostTT.autosubst.GAST_rasimpl]
quoted_term_ind [in GhostTT.autosubst.GAST_rasimpl]
quoted_term_rect [in GhostTT.autosubst.GAST_rasimpl]
quoted_subst_sind [in GhostTT.autosubst.GAST_rasimpl]
quoted_subst_rec [in GhostTT.autosubst.GAST_rasimpl]
quoted_subst_ind [in GhostTT.autosubst.GAST_rasimpl]
quoted_subst_rect [in GhostTT.autosubst.GAST_rasimpl]

R

relm [in GhostTT.TermMode]
relv [in GhostTT.Erasure]
revive_sc [in GhostTT.Revival]
revive_ctx [in GhostTT.Revival]
revive_term [in GhostTT.Revival]
rev_subst [in GhostTT.Revival]
rmctx [in GhostTT.Potential]
rpm_lift [in GhostTT.Param]
rscoping [in GhostTT.BasicMetaTheory]
rscoping_comp [in GhostTT.BasicMetaTheory]
rtyping [in GhostTT.BasicMetaTheory]
rwf_sind [in GhostTT.RTyping]
rwf_rec [in GhostTT.RTyping]
rwf_ind [in GhostTT.RTyping]
rwf_rect [in GhostTT.RTyping]

S

sc [in GhostTT.ContextDecl]
scons [in GhostTT.autosubst.unscoped]
scoping_sind [in GhostTT.Scoping]
scoping_ind [in GhostTT.Scoping]
SFalse_sind [in GhostTT.FreeTheorem]
SFalse_rec [in GhostTT.FreeTheorem]
SFalse_ind [in GhostTT.FreeTheorem]
SFalse_rect [in GhostTT.FreeTheorem]
shift [in GhostTT.autosubst.unscoped]
squash_sind [in GhostTT.TransVec]
sscoping_comp [in GhostTT.BasicMetaTheory]
sscoping_sind [in GhostTT.BasicMetaTheory]
sscoping_ind [in GhostTT.BasicMetaTheory]
star [in GhostTT.Examples]
STrue_sind [in GhostTT.FreeTheorem]
styping_sind [in GhostTT.BasicMetaTheory]
styping_ind [in GhostTT.BasicMetaTheory]

T

test_qsubst_ren_id [in GhostTT.autosubst.CCAST_rasimpl]
test_qren_id [in GhostTT.autosubst.RAsimpl]
test_qsubst_ren_id [in GhostTT.autosubst.GAST_rasimpl]
tr_ty [in GhostTT.Potential]
tr_ctx [in GhostTT.Potential]
typing_sind [in GhostTT.Typing]
typing_ind [in GhostTT.Typing]
ty_sind [in GhostTT.TransNat]
ty_rec [in GhostTT.TransNat]
ty_ind [in GhostTT.TransNat]
ty_rect [in GhostTT.TransNat]

U

ueq [in GhostTT.Univ]
umax [in GhostTT.Univ]
unquote_cterm [in GhostTT.autosubst.CCAST_rasimpl]
unquote_subst [in GhostTT.autosubst.CCAST_rasimpl]
unquote_ren [in GhostTT.autosubst.RAsimpl]
unquote_nat [in GhostTT.autosubst.RAsimpl]
unquote_term [in GhostTT.autosubst.GAST_rasimpl]
unquote_subst [in GhostTT.autosubst.GAST_rasimpl]
up_allfv [in GhostTT.autosubst.unscoped]
up_ren [in GhostTT.autosubst.unscoped]
urm [in GhostTT.Model]
urm_ctx [in GhostTT.Model]
usup [in GhostTT.Univ]

V

var_zero [in GhostTT.autosubst.unscoped]
vpar [in GhostTT.Param]
vreg [in GhostTT.Param]

W

wf_sind [in GhostTT.Typing]
wf_ind [in GhostTT.Typing]
whenSome [in GhostTT.Util]

Record Index

C

Core.Up_term [in GhostTT.autosubst.GAST]
Core.Up_cterm [in GhostTT.autosubst.CCAST]
CSubstSimplification [in GhostTT.autosubst.CCAST_rasimpl]
CTermSimplification [in GhostTT.autosubst.CCAST_rasimpl]

R

RenSimplification [in GhostTT.autosubst.RAsimpl]
Ren1 [in GhostTT.autosubst.unscoped]
Ren2 [in GhostTT.autosubst.unscoped]
Ren3 [in GhostTT.autosubst.unscoped]
Ren4 [in GhostTT.autosubst.unscoped]
Ren5 [in GhostTT.autosubst.unscoped]

S

SubstSimplification [in GhostTT.autosubst.GAST_rasimpl]
Subst1 [in GhostTT.autosubst.unscoped]
Subst2 [in GhostTT.autosubst.unscoped]
Subst3 [in GhostTT.autosubst.unscoped]
Subst4 [in GhostTT.autosubst.unscoped]
Subst5 [in GhostTT.autosubst.unscoped]

T

TermSimplification [in GhostTT.autosubst.GAST_rasimpl]

V

Var [in GhostTT.autosubst.unscoped]

Global Index

H

J

K

X

Y

Z

_

(1572 entries)

Notation Index

A

B

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

T

V

W

X

Y

Z

_

(64 entries)

Module Index

B

D

F

G

H

J

K

L

M

N

O

P

Q

T

V

W

X

Y

Z

_

other

(12 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1 entry)

Library Index

D

H

I

J

K

L

N

O

Q

V

W

X

Y

Z

_

other

(34 entries)

Lemma Index

B

H

J

K

L

Q

X

Y

Z

_

other

(523 entries)

Constructor Index

B

D

F

G

H

J

K

L

U

X

Y

Z

_

other

(479 entries)

Axiom Index

A

B

D

E

F

G

H

I

J

K

L

M

N

O

Q

R

S

T

U

V

W

X

Y

Z

_

other

(2 entries)

Inductive Index

A

B

D

F

H

I

J

K

L

O

U

X

Y

Z

_

other

(59 entries)

Projection Index

B

D

E

F

G

H

J

K

L

M

N

O

P

Q

T

U

V

W

X

Y

Z

_

other

(18 entries)

Section Index

B

C

D

E

F

G

H

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(3 entries)

Instance Index

A

B

D

E

G

H

J

K

L

M

N

O

P

Q

T

U

V

W

X

Y

Z

_

other

(29 entries)

Abbreviation Index

A

B

E

F

G

H

I

J

K

L

N

O

P

Q

R

U

V

W

X

Y

Z

_

other

(10 entries)

Definition Index

H

J

K

X

Y

Z

_

other

(320 entries)

Record Index

A

B

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

U

W

X

Y

Z

_

other

(18 entries)

This page has been generated by coqdoc