| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (154 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (62 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (33 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (9 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (18 entries) |
Global Index
A
alpha [definition, in Top.IE_Property]Ax1 [axiom, in Top.Sn_Axiomatic]
Ax2 [axiom, in Top.Sn_Axiomatic]
Ax2_bisl [lemma, in Top.Sn_Axiomatic]
Ax2_stars_eta [lemma, in Top.Sn_Axiomatic]
Ax2_stars_sn [lemma, in Top.Sn_Axiomatic]
Ax2_stars [axiom, in Top.Sn_Axiomatic]
B
build_list [definition, in Top.list_subst]C
commut_lift_subst [lemma, in Top.Terme]commut_lift_subst_rec [lemma, in Top.Terme]
commut_lift_subst_list [lemma, in Top.list_subst]
commut_lift_subst_list_aux [lemma, in Top.list_subst]
D
DB [constructor, in Top.reduction]db [inductive, in Top.reduction]
db_to_list_substT [lemma, in Top.reduction]
db_to_subst [lemma, in Top.reduction]
DB_App [constructor, in Top.reduction]
DB_Lam [constructor, in Top.reduction]
E
equiv [library]eta [axiom, in Top.Sn_Axiomatic]
eta_subst_eq [axiom, in Top.Sn_Axiomatic]
F
free_lift [lemma, in Top.Terme]fv [definition, in Top.list_subst]
fv_rec [definition, in Top.list_subst]
f_cp [definition, in Top.IE_Property]
G
GC [constructor, in Top.reduction]gc [inductive, in Top.reduction]
gc_to_list_substT [lemma, in Top.reduction]
gc_to_subst [lemma, in Top.reduction]
GC_Term [constructor, in Top.reduction]
I
IEProp [lemma, in Top.IE_Property]IE_Property [library]
is_free [definition, in Top.Terme]
L
lemme1 [lemma, in Top.reduction]lemme2 [lemma, in Top.reduction]
lemme2' [lemma, in Top.reduction]
lex [inductive, in Top.IE_Property]
lift [definition, in Top.Terme]
lift_commut_of_succ [lemma, in Top.Terme]
lift_commut [lemma, in Top.Terme]
lift_var_lt [lemma, in Top.Terme]
lift_var_ge [lemma, in Top.Terme]
lift_rec0 [lemma, in Top.Terme]
lift_rec [definition, in Top.Terme]
lift_subst [lemma, in Top.list_subst]
lift0 [lemma, in Top.Terme]
list_substT [definition, in Top.list_subst]
list_substV [definition, in Top.list_subst]
list_subst [library]
LS [constructor, in Top.reduction]
ls [definition, in Top.reduction]
LSA [constructor, in Top.reduction]
lsa [inductive, in Top.reduction]
lsa_red [lemma, in Top.equiv]
lsa_red' [lemma, in Top.equiv]
lsa_Hyp1 [lemma, in Top.equiv]
LSA_RET [constructor, in Top.equiv]
lsa_ret [inductive, in Top.equiv]
LSA_SubInt1 [constructor, in Top.equiv]
LSA_SubExt1 [constructor, in Top.equiv]
LSA_AppRight1 [constructor, in Top.equiv]
LSA_AppLeft1 [constructor, in Top.equiv]
LSA_Lam1 [constructor, in Top.equiv]
LSA_Var1 [constructor, in Top.equiv]
lsa_d_ret [inductive, in Top.equiv]
lsa_to_list_substT [lemma, in Top.reduction]
lsa_to_subst [lemma, in Top.reduction]
lsa_Hyp [lemma, in Top.reduction]
LSA_SubInt [constructor, in Top.reduction]
LSA_SubExt [constructor, in Top.reduction]
LSA_AppRight [constructor, in Top.reduction]
LSA_AppLeft [constructor, in Top.reduction]
LSA_Lam [constructor, in Top.reduction]
LSA_Var [constructor, in Top.reduction]
lsa_def [inductive, in Top.reduction]
ls_equivalence [lemma, in Top.equiv]
ls_to_list_subst [lemma, in Top.reduction]
ls_to_subst [lemma, in Top.reduction]
lt_G [constructor, in Top.IE_Property]
lt_L [constructor, in Top.IE_Property]
N
NatOrderInv [module, in Top.list_subst]NatOrderInv.leb [definition, in Top.list_subst]
NatOrderInv.leb_total [lemma, in Top.list_subst]
NatOrderInv.t [definition, in Top.list_subst]
_ <=? _ [notation, in Top.list_subst]
NatSort [module, in Top.list_subst]
no_subst_gen [lemma, in Top.equiv]
no_occ_of_x [lemma, in Top.Terme]
num_occ [definition, in Top.Terme]
O
One_step_ls [lemma, in Top.IE_Property]R
red [inductive, in Top.reduction]RedContextSubExt [constructor, in Top.reduction]
RedContextSubInt [constructor, in Top.reduction]
RedContextTAbs [constructor, in Top.reduction]
RedContextTAppLeft [constructor, in Top.reduction]
RedContextTAppRight [constructor, in Top.reduction]
reduction [library]
red_to_list_substT [lemma, in Top.reduction]
red_sub [lemma, in Top.reduction]
red_app [lemma, in Top.reduction]
red_star_RedContextSubInt [lemma, in Top.reduction]
red_star_RedContextSubExt [lemma, in Top.reduction]
red_star_RedContextTAppRight [lemma, in Top.reduction]
red_star_RedContextTAppLeft [lemma, in Top.reduction]
red_star_ContextTAbs [lemma, in Top.reduction]
red_star_gc [lemma, in Top.reduction]
red_star_ls [lemma, in Top.reduction]
red_star_db [lemma, in Top.reduction]
red_to_star [lemma, in Top.reduction]
red_star_step [constructor, in Top.reduction]
red_star_eq [constructor, in Top.reduction]
red_star [inductive, in Top.reduction]
renommage [axiom, in Top.Sn_Axiomatic]
renommage_subst [axiom, in Top.Sn_Axiomatic]
S
shift [definition, in Top.Terme]shift_commut [lemma, in Top.Terme]
shift_subst [lemma, in Top.list_subst]
simpl_lift [lemma, in Top.Terme]
simpl_lift_rec [lemma, in Top.Terme]
sn [axiom, in Top.Sn_Axiomatic]
SN [definition, in Top.Sn_Axiomatic]
sn_and_eta [lemma, in Top.Sn_Axiomatic]
sn_ind [axiom, in Top.IE_Property]
Sn_Axiomatic [library]
substFree_eq [lemma, in Top.Terme]
subst_var_diff [lemma, in Top.Terme]
subst_nothing [lemma, in Top.Terme]
subst_nothing' [lemma, in Top.Terme]
subst_rec [definition, in Top.Terme]
subst_var_eta [lemma, in Top.IE_Property]
subst_var_0_eta [lemma, in Top.IE_Property]
subs_recbis [definition, in Top.Terme]
T
TAbs [constructor, in Top.Terme]TApp [constructor, in Top.Terme]
term [inductive, in Top.Terme]
Terme [library]
Th2 [lemma, in Top.Sn_Axiomatic]
Th3 [lemma, in Top.Sn_Axiomatic]
TSub [constructor, in Top.Terme]
TVar [constructor, in Top.Terme]
V
var_occ [lemma, in Top.Terme]other
_ -->* _ [notation, in Top.reduction]_ --> _ [notation, in Top.reduction]
_ -->gc _ [notation, in Top.reduction]
_ -->ls _ [notation, in Top.reduction]
_ -->db _ [notation, in Top.reduction]
_ =? _ [notation, in Top.Sn_Axiomatic]
_ { _ := _ } [notation, in Top.Terme]
_ @ _ [notation, in Top.Terme]
_ [ _ ] [notation, in Top.Terme]
_
[ _ ; .. ; _ ] [notation, in Top.list_subst]
[ ] [notation, in Top.list_subst]
\ [notation, in Top.Terme]
Notation Index
N
_ <=? _ [in Top.list_subst]other
_ -->* _ [in Top.reduction]_ --> _ [in Top.reduction]
_ -->gc _ [in Top.reduction]
_ -->ls _ [in Top.reduction]
_ -->db _ [in Top.reduction]
_ =? _ [in Top.Sn_Axiomatic]
_ { _ := _ } [in Top.Terme]
_ @ _ [in Top.Terme]
_ [ _ ] [in Top.Terme]
_
[ _ ; .. ; _ ] [in Top.list_subst]
[ ] [in Top.list_subst]
\ [in Top.Terme]
Module Index
N
NatOrderInv [in Top.list_subst]NatSort [in Top.list_subst]
Library Index
E
equivI
IE_PropertyL
list_substR
reductionS
Sn_AxiomaticT
TermeLemma Index
A
Ax2_bisl [in Top.Sn_Axiomatic]Ax2_stars_eta [in Top.Sn_Axiomatic]
Ax2_stars_sn [in Top.Sn_Axiomatic]
C
commut_lift_subst [in Top.Terme]commut_lift_subst_rec [in Top.Terme]
commut_lift_subst_list [in Top.list_subst]
commut_lift_subst_list_aux [in Top.list_subst]
D
db_to_list_substT [in Top.reduction]db_to_subst [in Top.reduction]
F
free_lift [in Top.Terme]G
gc_to_list_substT [in Top.reduction]gc_to_subst [in Top.reduction]
I
IEProp [in Top.IE_Property]L
lemme1 [in Top.reduction]lemme2 [in Top.reduction]
lemme2' [in Top.reduction]
lift_commut_of_succ [in Top.Terme]
lift_commut [in Top.Terme]
lift_var_lt [in Top.Terme]
lift_var_ge [in Top.Terme]
lift_rec0 [in Top.Terme]
lift_subst [in Top.list_subst]
lift0 [in Top.Terme]
lsa_red [in Top.equiv]
lsa_red' [in Top.equiv]
lsa_Hyp1 [in Top.equiv]
lsa_to_list_substT [in Top.reduction]
lsa_to_subst [in Top.reduction]
lsa_Hyp [in Top.reduction]
ls_equivalence [in Top.equiv]
ls_to_list_subst [in Top.reduction]
ls_to_subst [in Top.reduction]
N
NatOrderInv.leb_total [in Top.list_subst]no_subst_gen [in Top.equiv]
no_occ_of_x [in Top.Terme]
O
One_step_ls [in Top.IE_Property]R
red_to_list_substT [in Top.reduction]red_sub [in Top.reduction]
red_app [in Top.reduction]
red_star_RedContextSubInt [in Top.reduction]
red_star_RedContextSubExt [in Top.reduction]
red_star_RedContextTAppRight [in Top.reduction]
red_star_RedContextTAppLeft [in Top.reduction]
red_star_ContextTAbs [in Top.reduction]
red_star_gc [in Top.reduction]
red_star_ls [in Top.reduction]
red_star_db [in Top.reduction]
red_to_star [in Top.reduction]
S
shift_commut [in Top.Terme]shift_subst [in Top.list_subst]
simpl_lift [in Top.Terme]
simpl_lift_rec [in Top.Terme]
sn_and_eta [in Top.Sn_Axiomatic]
substFree_eq [in Top.Terme]
subst_var_diff [in Top.Terme]
subst_nothing [in Top.Terme]
subst_nothing' [in Top.Terme]
subst_var_eta [in Top.IE_Property]
subst_var_0_eta [in Top.IE_Property]
T
Th2 [in Top.Sn_Axiomatic]Th3 [in Top.Sn_Axiomatic]
V
var_occ [in Top.Terme]Constructor Index
D
DB [in Top.reduction]DB_App [in Top.reduction]
DB_Lam [in Top.reduction]
G
GC [in Top.reduction]GC_Term [in Top.reduction]
L
LS [in Top.reduction]LSA [in Top.reduction]
LSA_RET [in Top.equiv]
LSA_SubInt1 [in Top.equiv]
LSA_SubExt1 [in Top.equiv]
LSA_AppRight1 [in Top.equiv]
LSA_AppLeft1 [in Top.equiv]
LSA_Lam1 [in Top.equiv]
LSA_Var1 [in Top.equiv]
LSA_SubInt [in Top.reduction]
LSA_SubExt [in Top.reduction]
LSA_AppRight [in Top.reduction]
LSA_AppLeft [in Top.reduction]
LSA_Lam [in Top.reduction]
LSA_Var [in Top.reduction]
lt_G [in Top.IE_Property]
lt_L [in Top.IE_Property]
R
RedContextSubExt [in Top.reduction]RedContextSubInt [in Top.reduction]
RedContextTAbs [in Top.reduction]
RedContextTAppLeft [in Top.reduction]
RedContextTAppRight [in Top.reduction]
red_star_step [in Top.reduction]
red_star_eq [in Top.reduction]
T
TAbs [in Top.Terme]TApp [in Top.Terme]
TSub [in Top.Terme]
TVar [in Top.Terme]
Axiom Index
A
Ax1 [in Top.Sn_Axiomatic]Ax2 [in Top.Sn_Axiomatic]
Ax2_stars [in Top.Sn_Axiomatic]
E
eta [in Top.Sn_Axiomatic]eta_subst_eq [in Top.Sn_Axiomatic]
R
renommage [in Top.Sn_Axiomatic]renommage_subst [in Top.Sn_Axiomatic]
S
sn [in Top.Sn_Axiomatic]sn_ind [in Top.IE_Property]
Inductive Index
D
db [in Top.reduction]G
gc [in Top.reduction]L
lex [in Top.IE_Property]lsa [in Top.reduction]
lsa_ret [in Top.equiv]
lsa_d_ret [in Top.equiv]
lsa_def [in Top.reduction]
R
red [in Top.reduction]red_star [in Top.reduction]
T
term [in Top.Terme]Definition Index
A
alpha [in Top.IE_Property]B
build_list [in Top.list_subst]F
fv [in Top.list_subst]fv_rec [in Top.list_subst]
f_cp [in Top.IE_Property]
I
is_free [in Top.Terme]L
lift [in Top.Terme]lift_rec [in Top.Terme]
list_substT [in Top.list_subst]
list_substV [in Top.list_subst]
ls [in Top.reduction]
N
NatOrderInv.leb [in Top.list_subst]NatOrderInv.t [in Top.list_subst]
num_occ [in Top.Terme]
S
shift [in Top.Terme]SN [in Top.Sn_Axiomatic]
subst_rec [in Top.Terme]
subs_recbis [in Top.Terme]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (154 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (62 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (33 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (9 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (18 entries) |
This page has been generated by coqdoc