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 | _ | (329 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 | _ | (9 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 | _ | (137 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 | _ | (97 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 | _ | (38 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 | _ | (42 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 | _ | (6 entries) |

# Global Index

## A

App [constructor, in compilation]App [constructor, in semantics]

append_assoc [lemma, in traces]

append_trace_traceinf [definition, in traces]

## B

Bottom [constructor, in densem]## C

Clos [constructor, in compilation]closed [definition, in cps]

closed_App_inv [lemma, in cps]

closed_eval [lemma, in cps]

closed_subst [lemma, in cps]

code [definition, in compilation]

coeval [inductive, in compilation]

coeval [inductive, in semantics]

coeval_app [constructor, in semantics]

coeval_App [constructor, in compilation]

coeval_app_inv [lemma, in typing]

coeval_Const [constructor, in compilation]

coeval_const [constructor, in semantics]

coeval_const_inv [lemma, in typing]

coeval_cored [lemma, in semantics]

coeval_cps_characterization [lemma, in cps]

coeval_eval_or_evalinf [lemma, in semantics]

coeval_filinski_aux [lemma, in typing]

coeval_fun [constructor, in semantics]

coeval_Fun [constructor, in compilation]

coeval_fun_inv1 [lemma, in typing]

coeval_fun_inv2 [lemma, in typing]

coeval_noteval_evalinf [lemma, in semantics]

coeval_omega [lemma, in semantics]

coeval_value [lemma, in semantics]

coeval_value_or_red1 [lemma, in semantics]

coeval_Var [constructor, in compilation]

coeval_zerofun_omega [lemma, in semantics]

compilation [library]

compile [definition, in compilation]

compile_coeval [lemma, in compilation]

compile_coeval_aux [lemma, in compilation]

compile_env [definition, in compilation]

compile_eval [lemma, in compilation]

compile_evalinf [lemma, in compilation]

compile_evalinf_aux [lemma, in compilation]

compile_value [definition, in compilation]

compute [definition, in densem]

compute_converges [lemma, in densem]

compute_diverges [lemma, in densem]

compute_gets_stuck [lemma, in densem]

compute_increasing [lemma, in densem]

const [axiom, in semantics]

const [axiom, in compilation]

Const [constructor, in compilation]

Const [constructor, in semantics]

cons_right [definition, in traces]

cons_right_app [lemma, in traces]

converges_eval [lemma, in densem]

cored [inductive, in semantics]

cored_notred_redinf [lemma, in semantics]

cored_red_or_redinf [lemma, in semantics]

cored_refl [constructor, in semantics]

cored_step [constructor, in semantics]

cored_trans [lemma, in semantics]

cotrans [inductive, in compilation]

cotransN [inductive, in compilation]

cotransN_cotrans [lemma, in compilation]

cotransN_perform [constructor, in compilation]

cotransN_trans [constructor, in compilation]

cotrans_refl [constructor, in compilation]

cotrans_step [constructor, in compilation]

cps [library]

## D

decompose_cotransN [lemma, in compilation]decompose_traceinf [lemma, in traces]

decompose_transinfN [lemma, in compilation]

delta [definition, in traces]

delta [definition, in semantics]

densem [library]

diverges_evalinf [lemma, in densem]

## E

env [definition, in compilation]env_empty [axiom, in typing]

env_exten [axiom, in typing]

env_get [axiom, in typing]

env_get_empty [axiom, in typing]

env_get_set [axiom, in typing]

env_get_set_other [lemma, in typing]

env_get_set_same [lemma, in typing]

env_set [axiom, in typing]

Error [constructor, in densem]

eval [inductive, in semantics]

eval [inductive, in compilation]

evalinf [inductive, in semantics]

evalinf [inductive, in compilation]

evalinf_App_f [constructor, in compilation]

evalinf_app_f [constructor, in semantics]

evalinf_app_l [constructor, in semantics]

evalinf_App_l [constructor, in compilation]

evalinf_app_r [constructor, in semantics]

evalinf_App_r [constructor, in compilation]

evalinf_coeval_cps [lemma, in cps]

evalinf_diverges [lemma, in densem]

evalinf_omega [lemma, in semantics]

evalinf_omega_1 [definition, in semantics]

evalinf_progress [lemma, in typing]

evalinf_redinf [lemma, in semantics]

evalinf_red1 [lemma, in semantics]

evaluates [definition, in densem]

evaluates_compute_either [lemma, in densem]

evaluates_limsup [lemma, in densem]

evaluates_total [lemma, in densem]

evaluates_unique [lemma, in densem]

eval_app [constructor, in semantics]

eval_App [constructor, in compilation]

eval_atom [lemma, in cps]

eval_atom_inv [lemma, in cps]

eval_body_atom [lemma, in cps]

eval_body_fun [lemma, in cps]

eval_coeval [lemma, in semantics]

eval_coeval_deterministic [lemma, in semantics]

eval_const [constructor, in semantics]

eval_Const [constructor, in compilation]

eval_converges [lemma, in densem]

eval_deterministic [lemma, in semantics]

eval_evalinf_exclusive [lemma, in semantics]

eval_Fun [constructor, in compilation]

eval_fun [constructor, in semantics]

eval_isvalue [lemma, in semantics]

eval_or_not_eval [lemma, in typing]

eval_preservation [lemma, in typing]

eval_red [lemma, in semantics]

eval_value [lemma, in semantics]

eval_Var [constructor, in compilation]

## F

filinski [definition, in typing]filinski1 [definition, in typing]

filinski2 [definition, in typing]

find_var_match [lemma, in compilation]

Fun [constructor, in semantics]

Fun [constructor, in compilation]

## H

has_type [inductive, in typing]has_type_app [constructor, in typing]

has_type_const [constructor, in typing]

has_type_fun [constructor, in typing]

has_type_subst [lemma, in typing]

has_type_var [constructor, in typing]

has_type_weaken [lemma, in typing]

height_term [definition, in typing]

## I

IApp [constructor, in compilation]IClosure [constructor, in compilation]

IConst [constructor, in compilation]

infinite_progress_redinf [lemma, in semantics]

INop [constructor, in compilation]

instr [inductive, in compilation]

Int [constructor, in compilation]

IReturn [constructor, in compilation]

isatom [inductive, in cps]

isatom_const [constructor, in cps]

isatom_fun [constructor, in cps]

isatom_var [constructor, in cps]

isbody [inductive, in cps]

isbody_app [constructor, in cps]

isbody_atom [constructor, in cps]

isbody_subst [lemma, in cps]

isfree [definition, in cps]

isfree_subst [lemma, in cps]

isvalue [inductive, in semantics]

isvalue_const [constructor, in semantics]

isvalue_dec [lemma, in traces]

isvalue_fun [constructor, in semantics]

isvalue_reduce1 [lemma, in traces]

IVar [constructor, in compilation]

## L

left_app_height [definition, in compilation]## M

MClos [constructor, in compilation]menv [definition, in compilation]

MInt [constructor, in compilation]

mvalue [inductive, in compilation]

## N

notred [definition, in semantics]not_coeval_filinski [lemma, in typing]

not_cored_coeval [lemma, in semantics]

not_evalinf_atom [lemma, in cps]

not_evalinf_coeval [lemma, in semantics]

not_eval_omega [lemma, in semantics]

not_eval_omega [lemma, in traces]

## O

Omega [definition, in cps]omega [definition, in semantics]

omega [definition, in traces]

omegatrace [definition, in traces]

## R

red [inductive, in semantics]redinf [inductive, in semantics]

redinf_app_l [lemma, in semantics]

redinf_app_r [lemma, in semantics]

redinf_cored [lemma, in semantics]

redinf_evalinf [lemma, in traces]

redinf_evalinf [lemma, in semantics]

redinf_intro [constructor, in semantics]

redinf_tredinf_aux [lemma, in traces]

reduce1 [definition, in traces]

red1 [inductive, in semantics]

red1_app_l [constructor, in semantics]

red1_app_r [constructor, in semantics]

red1_beta [constructor, in semantics]

red1_deterministic [lemma, in semantics]

red1_eval [lemma, in semantics]

red1_preservation [lemma, in typing]

red1_progress [lemma, in typing]

red1_reduce1 [lemma, in traces]

red_app_l [lemma, in semantics]

red_app_r [lemma, in semantics]

red_cored [lemma, in semantics]

red_eval [lemma, in semantics]

red_one [lemma, in semantics]

red_or_redinf [lemma, in semantics]

red_preservation [lemma, in typing]

red_refl [constructor, in semantics]

red_step [constructor, in semantics]

red_trans [lemma, in semantics]

red_tred [lemma, in traces]

result [inductive, in densem]

Result [constructor, in densem]

result_le [inductive, in densem]

result_le_bot [constructor, in densem]

result_le_refl [constructor, in densem]

## S

safered [inductive, in typing]safered_step [constructor, in typing]

safered_value [constructor, in typing]

semantics [library]

slot [inductive, in compilation]

Slot_return [constructor, in compilation]

Slot_value [constructor, in compilation]

soundness1 [lemma, in typing]

soundness2 [lemma, in typing]

soundness3 [lemma, in typing]

soundness4 [lemma, in typing]

soundness5 [lemma, in typing]

stack [definition, in compilation]

step [definition, in densem]

step_increasing [lemma, in densem]

subst [definition, in semantics]

## T

Tarrow [constructor, in typing]Tcons [constructor, in traces]

term [inductive, in semantics]

term [inductive, in compilation]

teval [inductive, in traces]

tevalinf [inductive, in traces]

tevalinf_app_f [constructor, in traces]

tevalinf_app_l [constructor, in traces]

tevalinf_app_r [constructor, in traces]

tevalinf_deterministic [lemma, in traces]

tevalinf_omega [lemma, in traces]

tevalinf_tredinf [lemma, in traces]

tevalinf_tredinf' [lemma, in traces]

tevalinf_tred1 [lemma, in traces]

teval_app [constructor, in traces]

teval_const [constructor, in traces]

teval_deterministic [lemma, in traces]

teval_fun [constructor, in traces]

teval_isvalue [lemma, in traces]

teval_tred [lemma, in traces]

teval_value [lemma, in traces]

Tint [constructor, in typing]

trace [definition, in traces]

traceinf [inductive, in traces]

traceinf_app_l [definition, in traces]

traceinf_app_r [definition, in traces]

traceinf_for [definition, in traces]

traceinf_sim [inductive, in traces]

traceinf_sim_intro [constructor, in traces]

traceinf_sim_refl [lemma, in traces]

traceinf_sim_sym [lemma, in traces]

traceinf_sim_trans [lemma, in traces]

traces [library]

trace_app_l [definition, in traces]

trace_app_r [definition, in traces]

trans [inductive, in compilation]

transinf [inductive, in compilation]

transinfN [inductive, in compilation]

transinfN_perform [constructor, in compilation]

transinfN_stutter [constructor, in compilation]

transinfN_transinf [lemma, in compilation]

transinf_intro [constructor, in compilation]

transition [inductive, in compilation]

transplus [inductive, in compilation]

transplus_base [constructor, in compilation]

transplus_step [constructor, in compilation]

transplus_trans [lemma, in compilation]

transplus_transitive [lemma, in compilation]

trans_IApp [constructor, in compilation]

trans_IClosure [constructor, in compilation]

trans_IConst [constructor, in compilation]

trans_INop [constructor, in compilation]

trans_IReturn [constructor, in compilation]

trans_IVar [constructor, in compilation]

trans_refl [constructor, in compilation]

trans_step [constructor, in compilation]

tred [inductive, in traces]

tredinf [inductive, in traces]

tredinf' [inductive, in traces]

tredinf'_intro [constructor, in traces]

tredinf'_tredinf [lemma, in traces]

tredinf_app_l [lemma, in traces]

tredinf_app_l_1 [lemma, in traces]

tredinf_app_l_2 [lemma, in traces]

tredinf_app_r [lemma, in traces]

tredinf_app_r_1 [lemma, in traces]

tredinf_app_r_2 [lemma, in traces]

tredinf_decompose [lemma, in traces]

tredinf_deterministic [lemma, in traces]

tredinf_intro [constructor, in traces]

tred1_teval [lemma, in traces]

tred_app_l [lemma, in traces]

tred_app_r [lemma, in traces]

tred_one [lemma, in traces]

tred_or_redinf [lemma, in traces]

tred_or_tredinf [lemma, in traces]

tred_red [lemma, in traces]

tred_refl [constructor, in traces]

tred_step [constructor, in traces]

tred_teval [lemma, in traces]

tred_trans [lemma, in traces]

type [inductive, in typing]

typenv [axiom, in typing]

typing [library]

## V

value [inductive, in compilation]value_notred [lemma, in semantics]

var [definition, in semantics]

Var [constructor, in semantics]

Var [constructor, in compilation]

var_eq [lemma, in semantics]

vf [definition, in typing]

vg [definition, in typing]

vx [definition, in traces]

vx [definition, in semantics]

vy [definition, in typing]

## Y

Y [definition, in typing]# Axiom Index

## C

const [in semantics]const [in compilation]

## E

env_empty [in typing]env_exten [in typing]

env_get [in typing]

env_get_empty [in typing]

env_get_set [in typing]

env_set [in typing]

## T

typenv [in typing]# Lemma Index

## A

append_assoc [in traces]## C

closed_App_inv [in cps]closed_eval [in cps]

closed_subst [in cps]

coeval_app_inv [in typing]

coeval_const_inv [in typing]

coeval_cored [in semantics]

coeval_cps_characterization [in cps]

coeval_eval_or_evalinf [in semantics]

coeval_filinski_aux [in typing]

coeval_fun_inv1 [in typing]

coeval_fun_inv2 [in typing]

coeval_noteval_evalinf [in semantics]

coeval_omega [in semantics]

coeval_value [in semantics]

coeval_value_or_red1 [in semantics]

coeval_zerofun_omega [in semantics]

compile_coeval [in compilation]

compile_coeval_aux [in compilation]

compile_eval [in compilation]

compile_evalinf [in compilation]

compile_evalinf_aux [in compilation]

compute_converges [in densem]

compute_diverges [in densem]

compute_gets_stuck [in densem]

compute_increasing [in densem]

cons_right_app [in traces]

converges_eval [in densem]

cored_notred_redinf [in semantics]

cored_red_or_redinf [in semantics]

cored_trans [in semantics]

cotransN_cotrans [in compilation]

## D

decompose_cotransN [in compilation]decompose_traceinf [in traces]

decompose_transinfN [in compilation]

diverges_evalinf [in densem]

## E

env_get_set_other [in typing]env_get_set_same [in typing]

evalinf_coeval_cps [in cps]

evalinf_diverges [in densem]

evalinf_omega [in semantics]

evalinf_progress [in typing]

evalinf_redinf [in semantics]

evalinf_red1 [in semantics]

evaluates_compute_either [in densem]

evaluates_limsup [in densem]

evaluates_total [in densem]

evaluates_unique [in densem]

eval_atom [in cps]

eval_atom_inv [in cps]

eval_body_atom [in cps]

eval_body_fun [in cps]

eval_coeval [in semantics]

eval_coeval_deterministic [in semantics]

eval_converges [in densem]

eval_deterministic [in semantics]

eval_evalinf_exclusive [in semantics]

eval_isvalue [in semantics]

eval_or_not_eval [in typing]

eval_preservation [in typing]

eval_red [in semantics]

eval_value [in semantics]

## F

find_var_match [in compilation]## H

has_type_subst [in typing]has_type_weaken [in typing]

## I

infinite_progress_redinf [in semantics]isbody_subst [in cps]

isfree_subst [in cps]

isvalue_dec [in traces]

isvalue_reduce1 [in traces]

## N

not_coeval_filinski [in typing]not_cored_coeval [in semantics]

not_evalinf_atom [in cps]

not_evalinf_coeval [in semantics]

not_eval_omega [in semantics]

not_eval_omega [in traces]

## R

redinf_app_l [in semantics]redinf_app_r [in semantics]

redinf_cored [in semantics]

redinf_evalinf [in traces]

redinf_evalinf [in semantics]

redinf_tredinf_aux [in traces]

red1_deterministic [in semantics]

red1_eval [in semantics]

red1_preservation [in typing]

red1_progress [in typing]

red1_reduce1 [in traces]

red_app_l [in semantics]

red_app_r [in semantics]

red_cored [in semantics]

red_eval [in semantics]

red_one [in semantics]

red_or_redinf [in semantics]

red_preservation [in typing]

red_trans [in semantics]

red_tred [in traces]

## S

soundness1 [in typing]soundness2 [in typing]

soundness3 [in typing]

soundness4 [in typing]

soundness5 [in typing]

step_increasing [in densem]

## T

tevalinf_deterministic [in traces]tevalinf_omega [in traces]

tevalinf_tredinf [in traces]

tevalinf_tredinf' [in traces]

tevalinf_tred1 [in traces]

teval_deterministic [in traces]

teval_isvalue [in traces]

teval_tred [in traces]

teval_value [in traces]

traceinf_sim_refl [in traces]

traceinf_sim_sym [in traces]

traceinf_sim_trans [in traces]

transinfN_transinf [in compilation]

transplus_trans [in compilation]

transplus_transitive [in compilation]

tredinf'_tredinf [in traces]

tredinf_app_l [in traces]

tredinf_app_l_1 [in traces]

tredinf_app_l_2 [in traces]

tredinf_app_r [in traces]

tredinf_app_r_1 [in traces]

tredinf_app_r_2 [in traces]

tredinf_decompose [in traces]

tredinf_deterministic [in traces]

tred1_teval [in traces]

tred_app_l [in traces]

tred_app_r [in traces]

tred_one [in traces]

tred_or_redinf [in traces]

tred_or_tredinf [in traces]

tred_red [in traces]

tred_teval [in traces]

tred_trans [in traces]

## V

value_notred [in semantics]var_eq [in semantics]

# Constructor Index

## A

App [in compilation]App [in semantics]

## B

Bottom [in densem]## C

Clos [in compilation]coeval_app [in semantics]

coeval_App [in compilation]

coeval_Const [in compilation]

coeval_const [in semantics]

coeval_fun [in semantics]

coeval_Fun [in compilation]

coeval_Var [in compilation]

Const [in compilation]

Const [in semantics]

cored_refl [in semantics]

cored_step [in semantics]

cotransN_perform [in compilation]

cotransN_trans [in compilation]

cotrans_refl [in compilation]

cotrans_step [in compilation]

## E

Error [in densem]evalinf_App_f [in compilation]

evalinf_app_f [in semantics]

evalinf_app_l [in semantics]

evalinf_App_l [in compilation]

evalinf_app_r [in semantics]

evalinf_App_r [in compilation]

eval_app [in semantics]

eval_App [in compilation]

eval_const [in semantics]

eval_Const [in compilation]

eval_Fun [in compilation]

eval_fun [in semantics]

eval_Var [in compilation]

## F

Fun [in semantics]Fun [in compilation]

## H

has_type_app [in typing]has_type_const [in typing]

has_type_fun [in typing]

has_type_var [in typing]

## I

IApp [in compilation]IClosure [in compilation]

IConst [in compilation]

INop [in compilation]

Int [in compilation]

IReturn [in compilation]

isatom_const [in cps]

isatom_fun [in cps]

isatom_var [in cps]

isbody_app [in cps]

isbody_atom [in cps]

isvalue_const [in semantics]

isvalue_fun [in semantics]

IVar [in compilation]

## M

MClos [in compilation]MInt [in compilation]

## R

redinf_intro [in semantics]red1_app_l [in semantics]

red1_app_r [in semantics]

red1_beta [in semantics]

red_refl [in semantics]

red_step [in semantics]

Result [in densem]

result_le_bot [in densem]

result_le_refl [in densem]

## S

safered_step [in typing]safered_value [in typing]

Slot_return [in compilation]

Slot_value [in compilation]

## T

Tarrow [in typing]Tcons [in traces]

tevalinf_app_f [in traces]

tevalinf_app_l [in traces]

tevalinf_app_r [in traces]

teval_app [in traces]

teval_const [in traces]

teval_fun [in traces]

Tint [in typing]

traceinf_sim_intro [in traces]

transinfN_perform [in compilation]

transinfN_stutter [in compilation]

transinf_intro [in compilation]

transplus_base [in compilation]

transplus_step [in compilation]

trans_IApp [in compilation]

trans_IClosure [in compilation]

trans_IConst [in compilation]

trans_INop [in compilation]

trans_IReturn [in compilation]

trans_IVar [in compilation]

trans_refl [in compilation]

trans_step [in compilation]

tredinf'_intro [in traces]

tredinf_intro [in traces]

tred_refl [in traces]

tred_step [in traces]

## V

Var [in semantics]Var [in compilation]

# Inductive Index

## C

coeval [in compilation]coeval [in semantics]

cored [in semantics]

cotrans [in compilation]

cotransN [in compilation]

## E

eval [in semantics]eval [in compilation]

evalinf [in semantics]

evalinf [in compilation]

## H

has_type [in typing]## I

instr [in compilation]isatom [in cps]

isbody [in cps]

isvalue [in semantics]

## M

mvalue [in compilation]## R

red [in semantics]redinf [in semantics]

red1 [in semantics]

result [in densem]

result_le [in densem]

## S

safered [in typing]slot [in compilation]

## T

term [in semantics]term [in compilation]

teval [in traces]

tevalinf [in traces]

traceinf [in traces]

traceinf_sim [in traces]

trans [in compilation]

transinf [in compilation]

transinfN [in compilation]

transition [in compilation]

transplus [in compilation]

tred [in traces]

tredinf [in traces]

tredinf' [in traces]

type [in typing]

## V

value [in compilation]# Definition Index

## A

append_trace_traceinf [in traces]## C

closed [in cps]code [in compilation]

compile [in compilation]

compile_env [in compilation]

compile_value [in compilation]

compute [in densem]

cons_right [in traces]

## D

delta [in traces]delta [in semantics]

## E

env [in compilation]evalinf_omega_1 [in semantics]

evaluates [in densem]

## F

filinski [in typing]filinski1 [in typing]

filinski2 [in typing]

## H

height_term [in typing]## I

isfree [in cps]## L

left_app_height [in compilation]## M

menv [in compilation]## N

notred [in semantics]## O

Omega [in cps]omega [in semantics]

omega [in traces]

omegatrace [in traces]

## R

reduce1 [in traces]## S

stack [in compilation]step [in densem]

subst [in semantics]

## T

trace [in traces]traceinf_app_l [in traces]

traceinf_app_r [in traces]

traceinf_for [in traces]

trace_app_l [in traces]

trace_app_r [in traces]

## V

var [in semantics]vf [in typing]

vg [in typing]

vx [in traces]

vx [in semantics]

vy [in typing]

## Y

Y [in typing]# Library Index

## C

compilationcps

## D

densem## S

semantics## T

tracestyping

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 | _ | (329 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 | _ | (9 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 | _ | (137 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 | _ | (97 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 | _ | (38 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 | _ | (42 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 | _ | (6 entries) |

This page has been generated by coqdoc