| 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 | (1157 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 | (22 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 | (3 entries) |
| Variable 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 | (67 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 | (21 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 | (562 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 | (189 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 | (20 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 | (31 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (32 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 | (192 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
Global Index
A
AC [constructor, in Rocoma.Coma]aligned [definition, in Rocoma.Recipes_logrel]
aligned_jstack [lemma, in Rocoma.Recipes_joker]
aligned_type_void2 [lemma, in Rocoma.Recipes_logrel]
aligned_closed_appl2 [lemma, in Rocoma.Recipes_logrel]
aligned_hsubst [lemma, in Rocoma.Recipes_logrel]
aligned_neu [lemma, in Rocoma.Recipes_logrel]
aligned_cons_t [lemma, in Rocoma.Recipes_logrel]
aligned_cons_r [lemma, in Rocoma.Recipes_logrel]
aligned_complete [lemma, in Rocoma.Recipes_logrel]
aligned_type_void [lemma, in Rocoma.Recipes_logrel]
allzbb [definition, in Rocoma.Recipes_neuneu]
allzbb_hsubst [lemma, in Rocoma.Recipes_neuneu]
allzbb_subst_var [lemma, in Rocoma.Recipes_neuneu]
allzbb_subst_var_n [lemma, in Rocoma.Recipes_neuneu]
allzbb_neu [lemma, in Rocoma.Recipes_neuneu]
all_params [definition, in Rocoma.VCgen]
all3 [inductive, in Rocoma.Recipes_fusion]
all3_fusion_refl_neu [lemma, in Rocoma.Recipes_fusion]
all3_sind [definition, in Rocoma.Recipes_fusion]
all3_ind [definition, in Rocoma.Recipes_fusion]
all3_cons_t [constructor, in Rocoma.Recipes_fusion]
all3_cons_r [constructor, in Rocoma.Recipes_fusion]
all3_nil [constructor, in Rocoma.Recipes_fusion]
And [constructor, in Rocoma.Recipes]
App [constructor, in Rocoma.Recipes]
appl [definition, in Rocoma.Recipes_stacks]
appl_hsubst [lemma, in Rocoma.Recipes_stacks]
appl_one_stept [lemma, in Rocoma.Recipes_stacks]
appl_one_step [lemma, in Rocoma.Recipes_stacks]
appl_not_tlam [lemma, in Rocoma.Recipes_stacks]
appl_not_neu [lemma, in Rocoma.Recipes_stacks]
appl_not_box [lemma, in Rocoma.Recipes_stacks]
appl_not_and [lemma, in Rocoma.Recipes_stacks]
appl_not_imp [lemma, in Rocoma.Recipes_stacks]
appl_not_lam [lemma, in Rocoma.Recipes_stacks]
appl_not_top [lemma, in Rocoma.Recipes_stacks]
appl_not_zero [lemma, in Rocoma.Recipes_stacks]
appl_not_var [lemma, in Rocoma.Recipes_stacks]
arg [inductive, in Rocoma.Coma]
args [definition, in Rocoma.Coma]
args_ty_sind [definition, in Rocoma.Coma]
args_ty_ind [definition, in Rocoma.Coma]
args_ty_c [constructor, in Rocoma.Coma]
args_ty_t [constructor, in Rocoma.Coma]
args_ty_nil [constructor, in Rocoma.Coma]
args_ty [inductive, in Rocoma.Coma]
arg_ren [definition, in Rocoma.Coma]
arg_sind [definition, in Rocoma.Coma]
arg_rec [definition, in Rocoma.Coma]
arg_ind [definition, in Rocoma.Coma]
arg_rect [definition, in Rocoma.Coma]
arg_of_sind [definition, in Rocoma.Recipes]
arg_of_ind [definition, in Rocoma.Recipes]
arg_tarr [constructor, in Rocoma.Recipes]
arg_arr [constructor, in Rocoma.Recipes]
arg_here [constructor, in Rocoma.Recipes]
arg_of [inductive, in Rocoma.Recipes]
Arr [constructor, in Rocoma.Recipes]
AT [constructor, in Rocoma.Coma]
AutosubstSsr [library]
Autosubst_FreeVars [library]
B
barrier [inductive, in Rocoma.Coma]barrier_sind [definition, in Rocoma.Coma]
barrier_rec [definition, in Rocoma.Coma]
barrier_ind [definition, in Rocoma.Coma]
barrier_rect [definition, in Rocoma.Coma]
Both [section, in Rocoma.Lib.Autosubst_FreeVars]
Both.A [variable, in Rocoma.Lib.Autosubst_FreeVars]
Both.B [variable, in Rocoma.Lib.Autosubst_FreeVars]
Both.HSubstLemmas_AB [variable, in Rocoma.Lib.Autosubst_FreeVars]
Both.HSubst_AB [variable, in Rocoma.Lib.Autosubst_FreeVars]
Both.IdsLemmas_B [variable, in Rocoma.Lib.Autosubst_FreeVars]
Both.IdsLemmas_A [variable, in Rocoma.Lib.Autosubst_FreeVars]
Both.Ids_B [variable, in Rocoma.Lib.Autosubst_FreeVars]
Both.Ids_A [variable, in Rocoma.Lib.Autosubst_FreeVars]
Both.Rename_B [variable, in Rocoma.Lib.Autosubst_FreeVars]
Both.Rename_A [variable, in Rocoma.Lib.Autosubst_FreeVars]
Both.SubstHSubstComp_AB [variable, in Rocoma.Lib.Autosubst_FreeVars]
Both.SubstLemmas_B [variable, in Rocoma.Lib.Autosubst_FreeVars]
Both.SubstLemmas_A [variable, in Rocoma.Lib.Autosubst_FreeVars]
Both.Subst_B [variable, in Rocoma.Lib.Autosubst_FreeVars]
Both.Subst_A [variable, in Rocoma.Lib.Autosubst_FreeVars]
Box [constructor, in Rocoma.Recipes]
box_rel3_box_ids [lemma, in Rocoma.Recipes_fusion]
box_rel3_type_det13 [lemma, in Rocoma.Recipes_fusion]
box_rel3_type_det12 [lemma, in Rocoma.Recipes_fusion]
box_rel3_preserved_hsubst0 [lemma, in Rocoma.Recipes_fusion]
box_rel3_preserved_hsubst [lemma, in Rocoma.Recipes_fusion]
box_rel3_preserved_ren [lemma, in Rocoma.Recipes_fusion]
box_rel3_preserved_subst0 [lemma, in Rocoma.Recipes_fusion]
box_rel3_preserved_subst [lemma, in Rocoma.Recipes_fusion]
box_rel3_preserved_neu [lemma, in Rocoma.Recipes_fusion]
box_rel3_nobox [lemma, in Rocoma.Recipes_fusion]
box_rel3_sind [definition, in Rocoma.Recipes_fusion]
box_rel3_ind [definition, in Rocoma.Recipes_fusion]
box_rel3_and [constructor, in Rocoma.Recipes_fusion]
box_rel3_app [constructor, in Rocoma.Recipes_fusion]
box_rel3_zeror [constructor, in Rocoma.Recipes_fusion]
box_rel3_zerol [constructor, in Rocoma.Recipes_fusion]
box_rel3_zeroz [constructor, in Rocoma.Recipes_fusion]
box_rel3_top [constructor, in Rocoma.Recipes_fusion]
box_rel3_var [constructor, in Rocoma.Recipes_fusion]
box_rel3_tapp [constructor, in Rocoma.Recipes_fusion]
box_rel3_lam [constructor, in Rocoma.Recipes_fusion]
box_rel3_imp [constructor, in Rocoma.Recipes_fusion]
box_rel3_neu [constructor, in Rocoma.Recipes_fusion]
box_rel3_tall [constructor, in Rocoma.Recipes_fusion]
box_rel3_tlam [constructor, in Rocoma.Recipes_fusion]
box_rel3_box [constructor, in Rocoma.Recipes_fusion]
box_rel3 [inductive, in Rocoma.Recipes_fusion]
box_rel2_nobox [lemma, in Rocoma.Recipes_box_rel]
box_rel2_box_ids [lemma, in Rocoma.Recipes_box_rel]
box_rel2_type_det [lemma, in Rocoma.Recipes_box_rel]
box_rel2_preserved_hsubst0 [lemma, in Rocoma.Recipes_box_rel]
box_rel2_preserved_hsubst [lemma, in Rocoma.Recipes_box_rel]
box_rel2_preserved_ren [lemma, in Rocoma.Recipes_box_rel]
box_rel2_preserved_subst0 [lemma, in Rocoma.Recipes_box_rel]
box_rel2_preserved_subst [lemma, in Rocoma.Recipes_box_rel]
box_rel2_preserved_neu [lemma, in Rocoma.Recipes_box_rel]
box_rel2_weight_eq [lemma, in Rocoma.Recipes_box_rel]
box_rel2_sind [definition, in Rocoma.Recipes_box_rel]
box_rel2_ind [definition, in Rocoma.Recipes_box_rel]
box_rel2_and [constructor, in Rocoma.Recipes_box_rel]
box_rel2_app [constructor, in Rocoma.Recipes_box_rel]
box_rel2_zero [constructor, in Rocoma.Recipes_box_rel]
box_rel2_top [constructor, in Rocoma.Recipes_box_rel]
box_rel2_var [constructor, in Rocoma.Recipes_box_rel]
box_rel2_tapp [constructor, in Rocoma.Recipes_box_rel]
box_rel2_lam [constructor, in Rocoma.Recipes_box_rel]
box_rel2_imp [constructor, in Rocoma.Recipes_box_rel]
box_rel2_neu [constructor, in Rocoma.Recipes_box_rel]
box_rel2_tall [constructor, in Rocoma.Recipes_box_rel]
box_rel2_tlam [constructor, in Rocoma.Recipes_box_rel]
box_rel2_box [constructor, in Rocoma.Recipes_box_rel]
box_rel2 [inductive, in Rocoma.Recipes_box_rel]
box_rel_nobox [lemma, in Rocoma.Recipes_box_rel]
box_rel_box_ids [lemma, in Rocoma.Recipes_box_rel]
box_rel_preserved_neu [lemma, in Rocoma.Recipes_box_rel]
box_rel_preserved_hsubst0 [lemma, in Rocoma.Recipes_box_rel]
box_rel_preserved_hsubst [lemma, in Rocoma.Recipes_box_rel]
box_rel_preserved_ren [lemma, in Rocoma.Recipes_box_rel]
box_rel_preserved_subst0 [lemma, in Rocoma.Recipes_box_rel]
box_rel_preserved_subst [lemma, in Rocoma.Recipes_box_rel]
box_rel_sind [definition, in Rocoma.Recipes_box_rel]
box_rel_ind [definition, in Rocoma.Recipes_box_rel]
box_rel_and [constructor, in Rocoma.Recipes_box_rel]
box_rel_app [constructor, in Rocoma.Recipes_box_rel]
box_rel_zero [constructor, in Rocoma.Recipes_box_rel]
box_rel_top [constructor, in Rocoma.Recipes_box_rel]
box_rel_var [constructor, in Rocoma.Recipes_box_rel]
box_rel_tapp [constructor, in Rocoma.Recipes_box_rel]
box_rel_lam [constructor, in Rocoma.Recipes_box_rel]
box_rel_imp [constructor, in Rocoma.Recipes_box_rel]
box_rel_neu [constructor, in Rocoma.Recipes_box_rel]
box_rel_tall [constructor, in Rocoma.Recipes_box_rel]
box_rel_tlam [constructor, in Rocoma.Recipes_box_rel]
box_rel_box [constructor, in Rocoma.Recipes_box_rel]
box_rel [inductive, in Rocoma.Recipes_box_rel]
b1 [lemma, in Rocoma.Recipes_neuneu]
C
cabs [inductive, in Rocoma.Coma]cabs_cty [lemma, in Rocoma.Coma]
cabs_mut [definition, in Rocoma.Coma]
cabs_sind [definition, in Rocoma.Coma]
cabs_ind [definition, in Rocoma.Coma]
cabs_c [constructor, in Rocoma.Coma]
cabs_t [constructor, in Rocoma.Coma]
cabs_void [constructor, in Rocoma.Coma]
closed [definition, in Rocoma.Lib.Autosubst_FreeVars]
closedh [definition, in Rocoma.Lib.Autosubst_FreeVars]
closedh_jokerT [lemma, in Rocoma.Recipes_joker]
closedh_joker [lemma, in Rocoma.Recipes_joker]
closedh_ids [lemma, in Rocoma.Lib.Autosubst_FreeVars]
closedh_eq [lemma, in Rocoma.Lib.Autosubst_FreeVars]
closedh_fvh [lemma, in Rocoma.Recipes_fv_lemmas]
closedh_hsubst [lemma, in Rocoma.Recipes_fv_lemmas]
closedh_sneu2 [lemma, in Rocoma.Recipes_fv_lemmas]
closedh_sneu [lemma, in Rocoma.Recipes_fv_lemmas]
closedh_tall1 [lemma, in Rocoma.Recipes_fv_lemmas]
closedh_tlam1 [lemma, in Rocoma.Recipes_fv_lemmas]
closedh_imp [lemma, in Rocoma.Recipes_fv_lemmas]
closedh_tapp [lemma, in Rocoma.Recipes_fv_lemmas]
closedh_box1 [lemma, in Rocoma.Recipes_fv_lemmas]
closedh_box [lemma, in Rocoma.Recipes_fv_lemmas]
closedh_neu1 [lemma, in Rocoma.Recipes_fv_lemmas]
closedh_neu [lemma, in Rocoma.Recipes_fv_lemmas]
closedh_lam [lemma, in Rocoma.Recipes_fv_lemmas]
closedh_and [lemma, in Rocoma.Recipes_fv_lemmas]
closedh_app [lemma, in Rocoma.Recipes_fv_lemmas]
closedh_top [lemma, in Rocoma.Recipes_fv_lemmas]
closed_jokerT [lemma, in Rocoma.Recipes_joker]
closed_call [lemma, in Rocoma.Recipes_joker]
closed_joker [lemma, in Rocoma.Recipes_joker]
closed_subst_closed [lemma, in Rocoma.VCgen]
closed_ids [lemma, in Rocoma.Lib.Autosubst_FreeVars]
closed_eq [lemma, in Rocoma.Lib.Autosubst_FreeVars]
closed_fv [lemma, in Rocoma.Recipes_fv_lemmas]
closed_unaffectedh [lemma, in Rocoma.Recipes_fv_lemmas]
closed_unaffected_term [lemma, in Rocoma.Recipes_fv_lemmas]
closed_subst [lemma, in Rocoma.Recipes_fv_lemmas]
closed_unaffected [lemma, in Rocoma.Recipes_fv_lemmas]
closed_sneu2 [lemma, in Rocoma.Recipes_fv_lemmas]
closed_sneu [lemma, in Rocoma.Recipes_fv_lemmas]
closed_tall1 [lemma, in Rocoma.Recipes_fv_lemmas]
closed_tall [lemma, in Rocoma.Recipes_fv_lemmas]
closed_tlam1 [lemma, in Rocoma.Recipes_fv_lemmas]
closed_tlam [lemma, in Rocoma.Recipes_fv_lemmas]
closed_imp1 [lemma, in Rocoma.Recipes_fv_lemmas]
closed_imp [lemma, in Rocoma.Recipes_fv_lemmas]
closed_tapp1 [lemma, in Rocoma.Recipes_fv_lemmas]
closed_tapp [lemma, in Rocoma.Recipes_fv_lemmas]
closed_box1 [lemma, in Rocoma.Recipes_fv_lemmas]
closed_box [lemma, in Rocoma.Recipes_fv_lemmas]
closed_neu1 [lemma, in Rocoma.Recipes_fv_lemmas]
closed_neu [lemma, in Rocoma.Recipes_fv_lemmas]
closed_lam1 [lemma, in Rocoma.Recipes_fv_lemmas]
closed_lam [lemma, in Rocoma.Recipes_fv_lemmas]
closed_and1 [lemma, in Rocoma.Recipes_fv_lemmas]
closed_and [lemma, in Rocoma.Recipes_fv_lemmas]
closed_app1 [lemma, in Rocoma.Recipes_fv_lemmas]
closed_app [lemma, in Rocoma.Recipes_fv_lemmas]
closed_top [lemma, in Rocoma.Recipes_fv_lemmas]
closed_has_ty_weak [lemma, in Rocoma.Recipes_typing]
closed_has_ty_contr [lemma, in Rocoma.Recipes_typing]
closed_stack_hsubst [lemma, in Rocoma.Recipes_stacks]
closed_stack_in [lemma, in Rocoma.Recipes_stacks]
closed_appl_neu_stack [lemma, in Rocoma.Recipes_stacks]
closed_appl_neu_head [lemma, in Rocoma.Recipes_stacks]
closed_appl_inv_strong [lemma, in Rocoma.Recipes_stacks]
closed_appl [lemma, in Rocoma.Recipes_stacks]
closed_stack_sind [definition, in Rocoma.Recipes_stacks]
closed_stack_ind [definition, in Rocoma.Recipes_stacks]
closed_stack_term [constructor, in Rocoma.Recipes_stacks]
closed_stack_recipe [constructor, in Rocoma.Recipes_stacks]
closed_stack_empty [constructor, in Rocoma.Recipes_stacks]
closed_stack [inductive, in Rocoma.Recipes_stacks]
closing [definition, in Rocoma.VCgen]
closing_box [lemma, in Rocoma.VCgen]
closing_hsubst [lemma, in Rocoma.VCgen]
Coma [library]
complete [definition, in Rocoma.Recipes_typing]
config [definition, in Rocoma.Coma]
config2expr [definition, in Rocoma.Coma]
conj_in_joker_call [lemma, in Rocoma.Recipes_joker]
conj_in_call_inst [lemma, in Rocoma.Recipes_joker]
conj_in_joker_mem [lemma, in Rocoma.Recipes_joker]
conj_in_joker_inst [lemma, in Rocoma.Recipes_joker]
conj_in_leaf [lemma, in Rocoma.Recipes_joker]
conj_in_subst_closed [lemma, in Rocoma.Recipes_joker]
conj_in_hsubst [lemma, in Rocoma.Recipes_joker]
conj_in_sind [definition, in Rocoma.Recipes_joker]
conj_in_ind [definition, in Rocoma.Recipes_joker]
conj_in_r [constructor, in Rocoma.Recipes_joker]
conj_in_l [constructor, in Rocoma.Recipes_joker]
conj_in_here [constructor, in Rocoma.Recipes_joker]
conj_in [inductive, in Rocoma.Recipes_joker]
covers [definition, in Rocoma.Recipes_joker]
covers_shift [lemma, in Rocoma.Recipes_joker]
covers_below_hsubst0 [lemma, in Rocoma.Recipes_joker]
covers_hsubst [lemma, in Rocoma.Recipes_joker]
covers_subst [lemma, in Rocoma.Recipes_joker]
covers_app_ren [lemma, in Rocoma.Recipes_joker]
covers_ren [lemma, in Rocoma.Recipes_joker]
covers_neu [lemma, in Rocoma.Recipes_joker]
covers_stack_incl [lemma, in Rocoma.Recipes_joker]
covers_appl [lemma, in Rocoma.Recipes_joker]
covers_app_appl [lemma, in Rocoma.Recipes_joker]
covers_stack [definition, in Rocoma.Recipes_joker]
covers_below_app [lemma, in Rocoma.Recipes_joker]
covers_app [definition, in Rocoma.Recipes_joker]
covers_below [definition, in Rocoma.Recipes_joker]
cross_lemma [lemma, in Rocoma.Recipes_fusion]
ctx [definition, in Rocoma.Recipes_typing]
ctx_insertion0 [lemma, in Rocoma.Recipes_typing]
ctx_insertion [definition, in Rocoma.Recipes_typing]
ctx_defs [definition, in Rocoma.Coma]
ctx_ext1 [lemma, in Rocoma.Recipes_directly_box]
ctx_ext0 [lemma, in Rocoma.Recipes_directly_box]
ctx_ext [definition, in Rocoma.Recipes_directly_box]
cty [inductive, in Rocoma.Coma]
cty_mut [definition, in Rocoma.Coma]
cty_sind [definition, in Rocoma.Coma]
cty_ind [definition, in Rocoma.Coma]
cty_defn [constructor, in Rocoma.Coma]
cty_box [constructor, in Rocoma.Coma]
cty_parc [constructor, in Rocoma.Coma]
cty_part [constructor, in Rocoma.Coma]
cty_appc [constructor, in Rocoma.Coma]
cty_appt [constructor, in Rocoma.Coma]
cty_sym [constructor, in Rocoma.Coma]
c_len [definition, in Rocoma.Recipes_joker]
c_3_10_4 [lemma, in Rocoma.Recipes_fusion]
c_3_10_3 [lemma, in Rocoma.Recipes_fusion]
c_3_10_2void [lemma, in Rocoma.Recipes_fusion]
c_3_10_2 [lemma, in Rocoma.Recipes_fusion]
c_3_10_1 [lemma, in Rocoma.Recipes_fusion]
c1 [lemma, in Rocoma.Recipes_fusion]
c1a [lemma, in Rocoma.Recipes_fusion]
D
db [inductive, in Rocoma.Recipes_directly_box]dbar [projection, in Rocoma.Coma]
dbody [projection, in Rocoma.Coma]
db_tapp3 [constructor, in Rocoma.Recipes_directly_box]
db_neu3 [constructor, in Rocoma.Recipes_directly_box]
db_imp3 [constructor, in Rocoma.Recipes_directly_box]
db_tall3 [constructor, in Rocoma.Recipes_directly_box]
db_tlam3 [constructor, in Rocoma.Recipes_directly_box]
db_appr3 [constructor, in Rocoma.Recipes_directly_box]
db_appl3 [constructor, in Rocoma.Recipes_directly_box]
db_andr3 [constructor, in Rocoma.Recipes_directly_box]
db_andl3 [constructor, in Rocoma.Recipes_directly_box]
db_lam3 [constructor, in Rocoma.Recipes_directly_box]
db_box3 [constructor, in Rocoma.Recipes_directly_box]
db_sind [definition, in Rocoma.Recipes_directly_box]
db_ind [definition, in Rocoma.Recipes_directly_box]
db_tapp [constructor, in Rocoma.Recipes_directly_box]
db_neu [constructor, in Rocoma.Recipes_directly_box]
db_imp [constructor, in Rocoma.Recipes_directly_box]
db_tall [constructor, in Rocoma.Recipes_directly_box]
db_tlam [constructor, in Rocoma.Recipes_directly_box]
db_appr [constructor, in Rocoma.Recipes_directly_box]
db_appl [constructor, in Rocoma.Recipes_directly_box]
db_andr [constructor, in Rocoma.Recipes_directly_box]
db_andl [constructor, in Rocoma.Recipes_directly_box]
db_lam [constructor, in Rocoma.Recipes_directly_box]
db_box [constructor, in Rocoma.Recipes_directly_box]
db3 [inductive, in Rocoma.Recipes_directly_box]
db3_proj3 [lemma, in Rocoma.Recipes_directly_box]
db3_proj2 [lemma, in Rocoma.Recipes_directly_box]
db3_proj1 [lemma, in Rocoma.Recipes_directly_box]
db3_sind [definition, in Rocoma.Recipes_directly_box]
db3_ind [definition, in Rocoma.Recipes_directly_box]
dec_allzbb [lemma, in Rocoma.Recipes_neuneu]
def [record, in Rocoma.Coma]
defs [definition, in Rocoma.Coma]
defs_ty_sind [definition, in Rocoma.Coma]
defs_ty_ind [definition, in Rocoma.Coma]
defs_ty_cons [constructor, in Rocoma.Coma]
defs_ty_nil [constructor, in Rocoma.Coma]
defs_ty [inductive, in Rocoma.Coma]
depth [definition, in Rocoma.Recipes]
depth_neu [lemma, in Rocoma.Recipes]
depth_hsubst [lemma, in Rocoma.Recipes]
depth_nonneg [lemma, in Rocoma.Recipes]
depth_dec [lemma, in Rocoma.Recipes]
directly_box_closed [lemma, in Rocoma.Recipes_directly_box]
directly_box_mem_box [lemma, in Rocoma.Recipes_directly_box]
directly_box_neu [lemma, in Rocoma.Recipes_directly_box]
directly_box_neu_idempotent [lemma, in Rocoma.Recipes_directly_box]
directly_box_depth [lemma, in Rocoma.Recipes_directly_box]
directly_box_ty [lemma, in Rocoma.Recipes_directly_box]
directly_box_dec [lemma, in Rocoma.Recipes_directly_box]
directly_box_ty_ext [lemma, in Rocoma.Recipes_directly_box]
directly_box_db_coincide [lemma, in Rocoma.Recipes_directly_box]
directly_box [definition, in Rocoma.Recipes_directly_box]
dty [projection, in Rocoma.Coma]
d1 [lemma, in Rocoma.Recipes_joker]
d1_1 [lemma, in Rocoma.Recipes_joker]
E
EApp [constructor, in Rocoma.Coma]eappl [definition, in Rocoma.Coma]
eappl_ty [lemma, in Rocoma.Coma]
EBar [constructor, in Rocoma.Coma]
EDef [constructor, in Rocoma.Coma]
edefs [definition, in Rocoma.Coma]
edefs_ty [lemma, in Rocoma.Coma]
ELam [constructor, in Rocoma.Coma]
empty_ctx [definition, in Rocoma.Recipes_typing]
ENT [definition, in Rocoma.Recipes_neuneu]
entails [definition, in Rocoma.Recipes_neuneu]
entails_neu [lemma, in Rocoma.Recipes_fusion]
entails_36 [lemma, in Rocoma.Recipes_neuneu]
entails_trans [lemma, in Rocoma.Recipes_neuneu]
entails_refl [lemma, in Rocoma.Recipes_neuneu]
entails_toptop [lemma, in Rocoma.Recipes_neuneu]
ent_jokerT [lemma, in Rocoma.Recipes_joker]
ENT_Neu [lemma, in Rocoma.Recipes_fusion]
ENT_and_comm [lemma, in Rocoma.Recipes_fusion]
ENT_and2 [lemma, in Rocoma.Recipes_fusion]
ENT_and1 [lemma, in Rocoma.Recipes_fusion]
ENT_and_intro [lemma, in Rocoma.Recipes_fusion]
ENT_and_neu [lemma, in Rocoma.Recipes_fusion]
ENT_tlam [lemma, in Rocoma.Recipes_fusion]
ENT_and [lemma, in Rocoma.Recipes_neuneu]
ENT_expand [lemma, in Rocoma.Recipes_neuneu]
EQU [definition, in Rocoma.Recipes_fusion]
equivalent [definition, in Rocoma.Recipes_fusion]
EQU_neu2 [lemma, in Rocoma.Recipes_fusion]
EQU_and_Neu2 [lemma, in Rocoma.Recipes_fusion]
EQU_and_Neu1 [lemma, in Rocoma.Recipes_fusion]
EQU_and_comm [lemma, in Rocoma.Recipes_fusion]
EQU_tlam [lemma, in Rocoma.Recipes_fusion]
EQU_neuneuneu [lemma, in Rocoma.Recipes_fusion]
EQU_Void_neu [lemma, in Rocoma.Recipes_fusion]
eta [definition, in Rocoma.Coma]
ETApp [constructor, in Rocoma.Coma]
ETLam [constructor, in Rocoma.Coma]
eval [inductive, in Rocoma.Recipes_eval]
Eval [section, in Rocoma.Recipes_eval]
evalf [definition, in Rocoma.Recipes_evalf]
Evalf [section, in Rocoma.Recipes_evalf]
evalf_unique [lemma, in Rocoma.Recipes_evalf]
evalf_def [lemma, in Rocoma.Recipes_evalf]
evalf_complete [lemma, in Rocoma.Recipes_evalf]
evalf_mono [lemma, in Rocoma.Recipes_evalf]
evalf_sound [lemma, in Rocoma.Recipes_evalf]
eval_conj_in [lemma, in Rocoma.Recipes_joker]
eval_joker_abs [lemma, in Rocoma.Recipes_joker]
eval_compose_and [lemma, in Rocoma.Recipes_fusion]
eval_fall_inv [lemma, in Rocoma.Recipes_eval]
eval_hsubst [lemma, in Rocoma.Recipes_eval]
eval_def [lemma, in Rocoma.Recipes_eval]
eval_Neu [lemma, in Rocoma.Recipes_eval]
eval_move_stack_left [lemma, in Rocoma.Recipes_eval]
eval_move_stack_right [lemma, in Rocoma.Recipes_eval]
eval_move_stack [lemma, in Rocoma.Recipes_eval]
eval_eval0_2 [lemma, in Rocoma.Recipes_eval]
eval_eval0_1 [lemma, in Rocoma.Recipes_eval]
eval_eval0 [lemma, in Rocoma.Recipes_eval]
eval_sind [definition, in Rocoma.Recipes_eval]
eval_ind [definition, in Rocoma.Recipes_eval]
eval_tapp [constructor, in Rocoma.Recipes_eval]
eval_app [constructor, in Rocoma.Recipes_eval]
eval_lam [constructor, in Rocoma.Recipes_eval]
eval_tall [constructor, in Rocoma.Recipes_eval]
eval_tlam [constructor, in Rocoma.Recipes_eval]
eval_neu [constructor, in Rocoma.Recipes_eval]
eval_box [constructor, in Rocoma.Recipes_eval]
eval_and [constructor, in Rocoma.Recipes_eval]
eval_imp [constructor, in Rocoma.Recipes_eval]
eval_top [constructor, in Rocoma.Recipes_eval]
eval_zero [constructor, in Rocoma.Recipes_eval]
EVar [constructor, in Rocoma.Coma]
exists_unique_eval [lemma, in Rocoma.Recipes_eval]
expr [inductive, in Rocoma.Coma]
expr_sind [definition, in Rocoma.Coma]
expr_rec [definition, in Rocoma.Coma]
expr_ind [definition, in Rocoma.Coma]
expr_rect [definition, in Rocoma.Coma]
Extraction [library]
F
fail [definition, in Rocoma.Coma]failed [definition, in Rocoma.Coma]
fall [definition, in Rocoma.Recipes]
FAll [constructor, in Rocoma.Recipes]
fallF [definition, in Rocoma.Recipes]
fallF_subst [lemma, in Rocoma.Recipes]
fall_hsubst [lemma, in Rocoma.Recipes]
fall_subst [lemma, in Rocoma.Recipes]
FAnd [constructor, in Rocoma.Recipes]
FBot [constructor, in Rocoma.Recipes]
FEqu [constructor, in Rocoma.Recipes]
FImp [constructor, in Rocoma.Recipes]
FNot [constructor, in Rocoma.Recipes]
FreeVars [section, in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.A [variable, in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.B [variable, in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.HSubstLemmas_AB [variable, in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.HSubst_AB [variable, in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.IdsLemmas_B [variable, in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.IdsLemmas_A [variable, in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.Ids_B [variable, in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.Ids_A [variable, in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.Rename_B [variable, in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.Rename_A [variable, in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.SubstHSubstComp_AB [variable, in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.SubstLemmas_B [variable, in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.SubstLemmas_A [variable, in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.Subst_B [variable, in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.Subst_A [variable, in Rocoma.Lib.Autosubst_FreeVars]
FTop [constructor, in Rocoma.Recipes]
fusion [inductive, in Rocoma.Recipes_fusion]
fusion_cross_neu [lemma, in Rocoma.Recipes_fusion]
fusion_allp_split [lemma, in Rocoma.Recipes_fusion]
fusion_meet [lemma, in Rocoma.Recipes_fusion]
fusion_has_type [lemma, in Rocoma.Recipes_fusion]
fusion_closed [lemma, in Rocoma.Recipes_fusion]
fusion_fv [lemma, in Rocoma.Recipes_fusion]
fusion_db3_fusion [lemma, in Rocoma.Recipes_fusion]
fusion_preserved_hsubst [lemma, in Rocoma.Recipes_fusion]
fusion_preserved_neu [lemma, in Rocoma.Recipes_fusion]
fusion_refl_neu [lemma, in Rocoma.Recipes_fusion]
fusion_swap [lemma, in Rocoma.Recipes_fusion]
fusion_refl [lemma, in Rocoma.Recipes_fusion]
fusion_sind [definition, in Rocoma.Recipes_fusion]
fusion_ind [definition, in Rocoma.Recipes_fusion]
fus_tapp [constructor, in Rocoma.Recipes_fusion]
fus_app [constructor, in Rocoma.Recipes_fusion]
fus_lam [constructor, in Rocoma.Recipes_fusion]
fus_tall [constructor, in Rocoma.Recipes_fusion]
fus_tlam [constructor, in Rocoma.Recipes_fusion]
fus_neu [constructor, in Rocoma.Recipes_fusion]
fus_box [constructor, in Rocoma.Recipes_fusion]
fus_and [constructor, in Rocoma.Recipes_fusion]
fus_imp [constructor, in Rocoma.Recipes_fusion]
fus_zero2 [constructor, in Rocoma.Recipes_fusion]
fus_zero1 [constructor, in Rocoma.Recipes_fusion]
fus_zero [constructor, in Rocoma.Recipes_fusion]
fus_top [constructor, in Rocoma.Recipes_fusion]
fus_var [constructor, in Rocoma.Recipes_fusion]
fv [definition, in Rocoma.Lib.Autosubst_FreeVars]
fvh [definition, in Rocoma.Lib.Autosubst_FreeVars]
fvh_joker [lemma, in Rocoma.Recipes_joker]
fvh_ids [lemma, in Rocoma.Lib.Autosubst_FreeVars]
fvh_hsubst [lemma, in Rocoma.Recipes_fv_lemmas]
fvh_sneu [lemma, in Rocoma.Recipes_fv_lemmas]
fvh_fall [lemma, in Rocoma.Recipes_fv_lemmas]
fvh_tall [lemma, in Rocoma.Recipes_fv_lemmas]
fvh_tlam [lemma, in Rocoma.Recipes_fv_lemmas]
fvh_imp [lemma, in Rocoma.Recipes_fv_lemmas]
fvh_tapp [lemma, in Rocoma.Recipes_fv_lemmas]
fvh_box [lemma, in Rocoma.Recipes_fv_lemmas]
fvh_neu [lemma, in Rocoma.Recipes_fv_lemmas]
fvh_lam [lemma, in Rocoma.Recipes_fv_lemmas]
fvh_and [lemma, in Rocoma.Recipes_fv_lemmas]
fvh_app [lemma, in Rocoma.Recipes_fv_lemmas]
fvu [definition, in Rocoma.Lib.Autosubst_FreeVars]
fvu_succ [lemma, in Rocoma.Lib.Autosubst_FreeVars]
fvu_fvu2 [lemma, in Rocoma.Lib.Autosubst_FreeVars]
fvu_equal_close2 [lemma, in Rocoma.Lib.Autosubst_FreeVars]
fvu_equal_close [lemma, in Rocoma.Lib.Autosubst_FreeVars]
fvu_subst [lemma, in Rocoma.Recipes_fv_lemmas]
fvu_tall [lemma, in Rocoma.Recipes_fv_lemmas]
fvu_tlam [lemma, in Rocoma.Recipes_fv_lemmas]
fvu0 [lemma, in Rocoma.Lib.Autosubst_FreeVars]
fvu2 [definition, in Rocoma.Lib.Autosubst_FreeVars]
fvu2_subst [lemma, in Rocoma.Recipes_fv_lemmas]
fvu2_lam [lemma, in Rocoma.Recipes_fv_lemmas]
fvu2_tall_op [lemma, in Rocoma.Recipes_fv_lemmas]
fvu2_tlam_op [lemma, in Rocoma.Recipes_fv_lemmas]
fvu2_tall [lemma, in Rocoma.Recipes_fv_lemmas]
fvu2_tlam [lemma, in Rocoma.Recipes_fv_lemmas]
fvu2_var [lemma, in Rocoma.Recipes_fv_lemmas]
fv_joker [lemma, in Rocoma.Recipes_joker]
fv_hsubst [lemma, in Rocoma.Lib.Autosubst_FreeVars]
fv_unaffected_lift [lemma, in Rocoma.Lib.Autosubst_FreeVars]
fv_ids_eq [lemma, in Rocoma.Lib.Autosubst_FreeVars]
fv_unaffectedh2 [lemma, in Rocoma.Recipes_fv_lemmas]
fv_unaffectedh [lemma, in Rocoma.Recipes_fv_lemmas]
fv_unaffected_term [lemma, in Rocoma.Recipes_fv_lemmas]
fv_unaffected [lemma, in Rocoma.Recipes_fv_lemmas]
fv_sneu [lemma, in Rocoma.Recipes_fv_lemmas]
fv_fall [lemma, in Rocoma.Recipes_fv_lemmas]
fv_tall [lemma, in Rocoma.Recipes_fv_lemmas]
fv_tlam [lemma, in Rocoma.Recipes_fv_lemmas]
fv_imp [lemma, in Rocoma.Recipes_fv_lemmas]
fv_tapp [lemma, in Rocoma.Recipes_fv_lemmas]
fv_box1 [lemma, in Rocoma.Recipes_fv_lemmas]
fv_box [lemma, in Rocoma.Recipes_fv_lemmas]
fv_neu [lemma, in Rocoma.Recipes_fv_lemmas]
fv_lam [lemma, in Rocoma.Recipes_fv_lemmas]
fv_and [lemma, in Rocoma.Recipes_fv_lemmas]
fv_app [lemma, in Rocoma.Recipes_fv_lemmas]
fv_tvar [lemma, in Rocoma.Recipes_fv_lemmas]
fv_var [lemma, in Rocoma.Recipes_fv_lemmas]
fv_has_ty [lemma, in Rocoma.Recipes_typing]
fv_plage_upn_gen [lemma, in Rocoma.Recipes_typing]
fv_plage_upn_cut_below [lemma, in Rocoma.Recipes_typing]
fv_plage_upn_cut_in [lemma, in Rocoma.Recipes_typing]
fv_plage_glue [lemma, in Rocoma.Recipes_typing]
fv_plage_shift [lemma, in Rocoma.Recipes_typing]
fv_plage_mono [lemma, in Rocoma.Recipes_typing]
fv_plage_eq [lemma, in Rocoma.Recipes_typing]
fv_plage [definition, in Rocoma.Recipes_typing]
fv1 [lemma, in Rocoma.Lib.Autosubst_FreeVars]
fv1h [lemma, in Rocoma.Lib.Autosubst_FreeVars]
fv1hh [lemma, in Rocoma.Lib.Autosubst_FreeVars]
f_ext_subst [lemma, in Rocoma.Lib.My_tactics]
G
golfouse [lemma, in Rocoma.Recipes_fv_lemmas]golfousec_le [lemma, in Rocoma.Recipes_fv_lemmas]
H
halt [definition, in Rocoma.Coma]halted [definition, in Rocoma.Coma]
has_type_jokerT [lemma, in Rocoma.Recipes_joker]
has_type_joker [lemma, in Rocoma.Recipes_joker]
has_type_joker_gen [lemma, in Rocoma.Recipes_joker]
has_type_inst_neu [lemma, in Rocoma.VCgen]
has_type_inst [lemma, in Rocoma.VCgen]
has_type_closing [lemma, in Rocoma.VCgen]
has_type_VC [lemma, in Rocoma.VCgen]
has_type_rall [lemma, in Rocoma.VCgen]
has_type_fall [lemma, in Rocoma.Recipes_typing]
has_type_beta [lemma, in Rocoma.Recipes_typing]
has_type_beta_gen [lemma, in Rocoma.Recipes_typing]
has_type_subst [lemma, in Rocoma.Recipes_typing]
has_type_ren [lemma, in Rocoma.Recipes_typing]
has_type_lower_b0 [lemma, in Rocoma.Recipes_typing]
has_type_hsubst1 [lemma, in Rocoma.Recipes_typing]
has_type_lower_1 [lemma, in Rocoma.Recipes_typing]
has_type_lower_n1 [lemma, in Rocoma.Recipes_typing]
has_type_lower_0 [lemma, in Rocoma.Recipes_typing]
has_type_lower [lemma, in Rocoma.Recipes_typing]
has_type_lower_b [lemma, in Rocoma.Recipes_typing]
has_type_hshift [lemma, in Rocoma.Recipes_typing]
has_type_hshift_cut_below [lemma, in Rocoma.Recipes_typing]
has_type_hshift_cut_in [lemma, in Rocoma.Recipes_typing]
has_type_hsubst_ext [lemma, in Rocoma.Recipes_typing]
has_type_hsubst_0 [lemma, in Rocoma.Recipes_typing]
has_type_swap_a [lemma, in Rocoma.Recipes_typing]
has_type_hsubst_upn [lemma, in Rocoma.Recipes_typing]
has_type_neu [lemma, in Rocoma.Recipes_typing]
has_type_det [lemma, in Rocoma.Recipes_typing]
has_type_sind [definition, in Rocoma.Recipes_typing]
has_type_ind [definition, in Rocoma.Recipes_typing]
has_type [inductive, in Rocoma.Recipes_typing]
has_type_appl_neu_stack [lemma, in Rocoma.Recipes_stacks]
has_type_appl_neu_head [lemma, in Rocoma.Recipes_stacks]
has_type_appl2_hole [lemma, in Rocoma.Recipes_stacks]
has_type_appl_hole [lemma, in Rocoma.Recipes_stacks]
has_type_appl2_neu [lemma, in Rocoma.Recipes_stacks]
has_type_appl_neu_head_ex [lemma, in Rocoma.Recipes_stacks]
has_type_appl2 [lemma, in Rocoma.Recipes_stacks]
has_type_appl [lemma, in Rocoma.Recipes_stacks]
has_type_appl_void [lemma, in Rocoma.Recipes_stacks]
Hide [constructor, in Rocoma.Coma]
HSubstLemmas_term_expr [instance, in Rocoma.Coma]
HSubstLemmas_term_recipe [instance, in Rocoma.Recipes]
hsubst_T_is_ren [lemma, in Rocoma.Recipes_typing]
HSubst_term_expr [instance, in Rocoma.Coma]
HSubst_term_recipe [instance, in Rocoma.Recipes]
I
IdsLemmas [record, in Rocoma.Lib.Autosubst_FreeVars]IdsLemmas_T [instance, in Rocoma.Recipes]
IdsLemmas_R [instance, in Rocoma.Recipes]
ids_inj_False [lemma, in Rocoma.Lib.Autosubst_FreeVars]
ids_inj [projection, in Rocoma.Lib.Autosubst_FreeVars]
Ids_expr [instance, in Rocoma.Coma]
Ids_recipe [instance, in Rocoma.Recipes]
Ids_term [instance, in Rocoma.Recipes]
if_ [definition, in Rocoma.Coma]
Imp [constructor, in Rocoma.Recipes]
inner1 [lemma, in Rocoma.Recipes_eval]
inner2g [lemma, in Rocoma.Recipes_eval]
inst [definition, in Rocoma.Recipes_fv_lemmas]
inst_nth [lemma, in Rocoma.Recipes_fv_lemmas]
inst_high [lemma, in Rocoma.Recipes_fv_lemmas]
inversion_neu_box [lemma, in Rocoma.Recipes]
inversion_neu_neu [lemma, in Rocoma.Recipes]
inversion_neu_tall [lemma, in Rocoma.Recipes]
inversion_neu_tlam [lemma, in Rocoma.Recipes]
inversion_neu_imp [lemma, in Rocoma.Recipes]
inversion_neu_lam [lemma, in Rocoma.Recipes]
inversion_neu_tapp [lemma, in Rocoma.Recipes]
inversion_neu_app [lemma, in Rocoma.Recipes]
inversion_neu_and [lemma, in Rocoma.Recipes]
inversion_neu_top [lemma, in Rocoma.Recipes]
inversion_neu_var [lemma, in Rocoma.Recipes]
in_aligned_arg [lemma, in Rocoma.Recipes_logrel]
in_stack_hsubst [lemma, in Rocoma.Recipes_stacks]
J
joker [definition, in Rocoma.Recipes_joker]jokerT [definition, in Rocoma.Recipes_joker]
joker_entails [lemma, in Rocoma.Recipes_joker]
joker_call_inst [lemma, in Rocoma.Recipes_joker]
joker_bot [lemma, in Rocoma.Recipes_joker]
joker_entails_mem [lemma, in Rocoma.Recipes_joker]
joker_inst [definition, in Rocoma.Recipes_joker]
joker_hsubst [lemma, in Rocoma.Recipes_joker]
joker_subst [lemma, in Rocoma.Recipes_joker]
joker_all [definition, in Rocoma.Recipes_joker]
joker_abs [definition, in Rocoma.Recipes_joker]
jstack [definition, in Rocoma.Recipes_joker]
L
Lam [constructor, in Rocoma.Recipes]lam_params [definition, in Rocoma.VCgen]
lift_inj_ids [lemma, in Rocoma.Lib.Autosubst_FreeVars]
logical_relation_lemma3_proj2 [lemma, in Rocoma.Recipes_fusion]
logical_relation_lemma3_proj1 [lemma, in Rocoma.Recipes_fusion]
logical_relation_lemma3 [lemma, in Rocoma.Recipes_fusion]
logical_relation_lemma2_proj2 [lemma, in Rocoma.Recipes_logrel]
logical_relation_lemma2_proj1 [lemma, in Rocoma.Recipes_logrel]
logical_relation_lemma2 [lemma, in Rocoma.Recipes_logrel]
logical_relation_lemma_proj2 [lemma, in Rocoma.Recipes_logrel]
logical_relation_lemma_proj1 [lemma, in Rocoma.Recipes_logrel]
logical_relation_lemma [lemma, in Rocoma.Recipes_logrel]
logrel [definition, in Rocoma.Recipes_logrel]
logrel2 [definition, in Rocoma.Recipes_logrel]
logrel3 [definition, in Rocoma.Recipes_fusion]
logrel3_andl_ren [lemma, in Rocoma.Recipes_fusion]
logrel3_andl [lemma, in Rocoma.Recipes_fusion]
ltac_Mark_sind [definition, in Rocoma.Lib.My_tactics]
ltac_Mark_rec [definition, in Rocoma.Lib.My_tactics]
ltac_Mark_ind [definition, in Rocoma.Lib.My_tactics]
ltac_Mark_rect [definition, in Rocoma.Lib.My_tactics]
ltac_mark [constructor, in Rocoma.Lib.My_tactics]
ltac_Mark [inductive, in Rocoma.Lib.My_tactics]
l_3_10 [lemma, in Rocoma.Recipes_fusion]
M
Main [library]MEET [definition, in Rocoma.Recipes_fusion]
meet [definition, in Rocoma.Recipes_fusion]
meet_refl [lemma, in Rocoma.Recipes_fusion]
mem_ren_shift [lemma, in Rocoma.Recipes_joker]
mem_ren_hsubst [lemma, in Rocoma.Recipes_joker]
mem_ren_ren [lemma, in Rocoma.Recipes_joker]
mem_ren_closed [lemma, in Rocoma.Recipes_joker]
mem_ren_0 [lemma, in Rocoma.Recipes_joker]
mem_ren [definition, in Rocoma.Recipes_joker]
mem_box_depth [lemma, in Rocoma.Recipes_directly_box]
mem_box [definition, in Rocoma.Recipes_directly_box]
MMapExt_fun [instance, in Rocoma.Autosubst.AutosubstSsr]
mmapExt_seq [instance, in Rocoma.Autosubst.AutosubstSsr]
MMapExt_pair [instance, in Rocoma.Autosubst.AutosubstSsr]
MMapExt_option [instance, in Rocoma.Autosubst.AutosubstSsr]
MMapInstances [section, in Rocoma.Autosubst.AutosubstSsr]
MMapInstances.A [variable, in Rocoma.Autosubst.AutosubstSsr]
MMapInstances.B [variable, in Rocoma.Autosubst.AutosubstSsr]
MMapInstances.C [variable, in Rocoma.Autosubst.AutosubstSsr]
MMapInstances.MMapExt_A_C [variable, in Rocoma.Autosubst.AutosubstSsr]
MMapInstances.MMapExt_A_B [variable, in Rocoma.Autosubst.AutosubstSsr]
MMapInstances.MMapLemmas_A_C [variable, in Rocoma.Autosubst.AutosubstSsr]
MMapInstances.MMapLemmas_A_B [variable, in Rocoma.Autosubst.AutosubstSsr]
MMapInstances.MMap_A_C [variable, in Rocoma.Autosubst.AutosubstSsr]
MMapInstances.MMap_A_B [variable, in Rocoma.Autosubst.AutosubstSsr]
MMapLemmas_fun [instance, in Rocoma.Autosubst.AutosubstSsr]
mmapLemmas_seq [instance, in Rocoma.Autosubst.AutosubstSsr]
MMapLemmas_pair [instance, in Rocoma.Autosubst.AutosubstSsr]
MMapLemmas_option [instance, in Rocoma.Autosubst.AutosubstSsr]
MMap_fun [instance, in Rocoma.Autosubst.AutosubstSsr]
mmap_seq [instance, in Rocoma.Autosubst.AutosubstSsr]
MMap_pair [instance, in Rocoma.Autosubst.AutosubstSsr]
MMap_option [instance, in Rocoma.Autosubst.AutosubstSsr]
Model [module, in Rocoma.Recipes_valid_model]
model [definition, in Rocoma.Main]
Model.valid [definition, in Rocoma.Recipes_valid_model]
Model.valid_all_elim [lemma, in Rocoma.Recipes_valid_model]
Model.valid_all_de_bruijn [lemma, in Rocoma.Recipes_valid_model]
Model.valid_all_and [lemma, in Rocoma.Recipes_valid_model]
Model.valid_all_mono [lemma, in Rocoma.Recipes_valid_model]
Model.valid_cut [lemma, in Rocoma.Recipes_valid_model]
Model.valid_contr [lemma, in Rocoma.Recipes_valid_model]
Model.valid_weak [lemma, in Rocoma.Recipes_valid_model]
Model.valid_imp_elim [lemma, in Rocoma.Recipes_valid_model]
Model.valid_imp_intro [lemma, in Rocoma.Recipes_valid_model]
Model.valid_and_l_cycle [lemma, in Rocoma.Recipes_valid_model]
Model.valid_and_intro_l [lemma, in Rocoma.Recipes_valid_model]
Model.valid_and_elim [lemma, in Rocoma.Recipes_valid_model]
Model.valid_and_intro [lemma, in Rocoma.Recipes_valid_model]
Model.valid_consistent [lemma, in Rocoma.Recipes_valid_model]
Model.valid_contradiction [lemma, in Rocoma.Recipes_valid_model]
Model.valid_top_l2 [lemma, in Rocoma.Recipes_valid_model]
Model.valid_top_l1 [lemma, in Rocoma.Recipes_valid_model]
Model.valid_top [lemma, in Rocoma.Recipes_valid_model]
Model.valid_assumption [lemma, in Rocoma.Recipes_valid_model]
_ ⟛ _ (model_scope) [notation, in Rocoma.Recipes_valid_model]
||- _ (model_scope) [notation, in Rocoma.Recipes_valid_model]
_ ||- _ (model_scope) [notation, in Rocoma.Recipes_valid_model]
My_tactics [library]
N
neu [definition, in Rocoma.Recipes]Neu [constructor, in Rocoma.Recipes]
NEU [definition, in Rocoma.Recipes_neuneu]
neuneu [lemma, in Rocoma.Recipes_neuneu]
neuneug [lemma, in Rocoma.Recipes_neuneu]
neuneu2 [lemma, in Rocoma.Recipes_neuneu]
neutral [definition, in Rocoma.Recipes_neuneu]
neu_joker_top [lemma, in Rocoma.Recipes_joker]
neu_joker [lemma, in Rocoma.Recipes_joker]
neu_eq_closedh [lemma, in Rocoma.Recipes_fv_lemmas]
neu_eq_fvh [lemma, in Rocoma.Recipes_fv_lemmas]
neu_eq_closed [lemma, in Rocoma.Recipes_fv_lemmas]
neu_eq_fv [lemma, in Rocoma.Recipes_fv_lemmas]
neu_eq_same_type [lemma, in Rocoma.Recipes_typing]
neu_stack_idempotent [lemma, in Rocoma.Recipes_stacks]
neu_stack_lemma [lemma, in Rocoma.Recipes_stacks]
neu_stack [definition, in Rocoma.Recipes_stacks]
neu_fall [lemma, in Rocoma.Recipes]
neu_subst_neu [lemma, in Rocoma.Recipes]
neu_idempotent [lemma, in Rocoma.Recipes]
neu_ren_comm [lemma, in Rocoma.Recipes]
neu_upren_comm [lemma, in Rocoma.Recipes]
neu_hsubst_comm [lemma, in Rocoma.Recipes]
NEU_Neu [lemma, in Rocoma.Recipes_neuneu]
NEU_tall [lemma, in Rocoma.Recipes_neuneu]
NEU_tlam [lemma, in Rocoma.Recipes_neuneu]
NEU_lam [lemma, in Rocoma.Recipes_neuneu]
NEU_beta [lemma, in Rocoma.Recipes_neuneu]
NEU_and [lemma, in Rocoma.Recipes_neuneu]
NEU_expand [lemma, in Rocoma.Recipes_neuneu]
O
olookup [definition, in Rocoma.Coma]OpSem [section, in Rocoma.Coma]
OpSem.valid [variable, in Rocoma.Coma]
order [definition, in Rocoma.Recipes]
order_nonneg [lemma, in Rocoma.Recipes]
order_arg [lemma, in Rocoma.Recipes]
P
piΓ [definition, in Rocoma.Recipes_joker]piΓ_shift [lemma, in Rocoma.Recipes_joker]
pushup [lemma, in Rocoma.Lib.Autosubst_FreeVars]
R
R [constructor, in Rocoma.Recipes_stacks]rall [definition, in Rocoma.VCgen]
recipe [inductive, in Rocoma.Recipes]
Recipes [library]
Recipes_joker [library]
Recipes_directly_box [library]
Recipes_fv_lemmas [library]
Recipes_logrel [library]
Recipes_stacks [library]
Recipes_evalf [library]
Recipes_box_rel [library]
Recipes_valid_model [library]
Recipes_fusion [library]
Recipes_eval [library]
Recipes_neuneu [library]
Recipes_valid_sig [library]
Recipes_typing [library]
recipe_eq_dec [lemma, in Rocoma.Recipes]
recipe_sind [definition, in Rocoma.Recipes]
recipe_rec [definition, in Rocoma.Recipes]
recipe_ind [definition, in Rocoma.Recipes]
recipe_rect [definition, in Rocoma.Recipes]
Rename_expr [instance, in Rocoma.Coma]
Rename_recipe [instance, in Rocoma.Recipes]
Rename_term [instance, in Rocoma.Recipes]
ren_hsubst [lemma, in Rocoma.Lib.Autosubst_FreeVars]
ren_inst [lemma, in Rocoma.Recipes_fv_lemmas]
ren_upn_subst [lemma, in Rocoma.Recipes_fv_lemmas]
ren_add [lemma, in Rocoma.Recipes_fv_lemmas]
ren_upn_ren [lemma, in Rocoma.Recipes_fv_lemmas]
ren_dec [definition, in Rocoma.Recipes_typing]
results [definition, in Rocoma.Main]
rlet [definition, in Rocoma.VCgen]
S
scompA [lemma, in Rocoma.Lib.Autosubst_FreeVars]scons_hcomp [lemma, in Rocoma.Recipes_fv_lemmas]
sel [definition, in Rocoma.Coma]
sel_eq [lemma, in Rocoma.Coma]
sem [definition, in Rocoma.Recipes_valid_model]
Sem [section, in Rocoma.Recipes_fusion]
Sem [section, in Rocoma.Recipes_neuneu]
sem_subst [lemma, in Rocoma.Recipes_valid_model]
sem_ren [lemma, in Rocoma.Recipes_valid_model]
sem_ext [lemma, in Rocoma.Recipes_valid_model]
Show [constructor, in Rocoma.Coma]
size_terms [lemma, in Rocoma.Recipes_joker]
stack [definition, in Rocoma.Recipes_stacks]
stack_rel_submits [lemma, in Rocoma.Recipes_joker]
stack_rel2_jstack [lemma, in Rocoma.Recipes_joker]
stack_rel3_meet_stack_rel2_entails [lemma, in Rocoma.Recipes_fusion]
stack_rel3_meet_refl [lemma, in Rocoma.Recipes_fusion]
stack_rel3_sind [definition, in Rocoma.Recipes_fusion]
stack_rel3_ind [definition, in Rocoma.Recipes_fusion]
stack_rel3_recipe [constructor, in Rocoma.Recipes_fusion]
stack_rel3_term [constructor, in Rocoma.Recipes_fusion]
stack_rel3_nil [constructor, in Rocoma.Recipes_fusion]
stack_rel3 [inductive, in Rocoma.Recipes_fusion]
stack_rel2_sind [definition, in Rocoma.Recipes_logrel]
stack_rel2_ind [definition, in Rocoma.Recipes_logrel]
stack_rel2_recipe [constructor, in Rocoma.Recipes_logrel]
stack_rel2_term [constructor, in Rocoma.Recipes_logrel]
stack_rel2_nil [constructor, in Rocoma.Recipes_logrel]
stack_rel2 [inductive, in Rocoma.Recipes_logrel]
stack_rel_sind [definition, in Rocoma.Recipes_logrel]
stack_rel_ind [definition, in Rocoma.Recipes_logrel]
stack_rel_recipe [constructor, in Rocoma.Recipes_logrel]
stack_rel_term [constructor, in Rocoma.Recipes_logrel]
stack_rel_nil [constructor, in Rocoma.Recipes_logrel]
stack_rel [inductive, in Rocoma.Recipes_logrel]
stack_has_type_hsubst [lemma, in Rocoma.Recipes_stacks]
stack_hsubst [definition, in Rocoma.Recipes_stacks]
stack_form [lemma, in Rocoma.Recipes_stacks]
stack_has_type_sind [definition, in Rocoma.Recipes_stacks]
stack_has_type_ind [definition, in Rocoma.Recipes_stacks]
stack_has_type_recipe [constructor, in Rocoma.Recipes_stacks]
stack_has_type_term [constructor, in Rocoma.Recipes_stacks]
stack_has_type_void [constructor, in Rocoma.Recipes_stacks]
stack_has_type [inductive, in Rocoma.Recipes_stacks]
stack_item_sind [definition, in Rocoma.Recipes_stacks]
stack_item_rec [definition, in Rocoma.Recipes_stacks]
stack_item_ind [definition, in Rocoma.Recipes_stacks]
stack_item_rect [definition, in Rocoma.Recipes_stacks]
stack_item [inductive, in Rocoma.Recipes_stacks]
stack_rel_entails_refl2 [lemma, in Rocoma.Recipes_neuneu]
step [inductive, in Rocoma.Coma]
steps [inductive, in Rocoma.Coma]
steps_sind [definition, in Rocoma.Coma]
steps_ind [definition, in Rocoma.Coma]
steps_step [constructor, in Rocoma.Coma]
steps_refl [constructor, in Rocoma.Coma]
step_sind [definition, in Rocoma.Coma]
step_ind [definition, in Rocoma.Coma]
step_if_false [constructor, in Rocoma.Coma]
step_if_true [constructor, in Rocoma.Coma]
step_box [constructor, in Rocoma.Coma]
step_appc [constructor, in Rocoma.Coma]
step_appt [constructor, in Rocoma.Coma]
step_sym [constructor, in Rocoma.Coma]
step_defn [constructor, in Rocoma.Coma]
step_app [constructor, in Rocoma.Coma]
step_tapp [constructor, in Rocoma.Coma]
strongly [definition, in Rocoma.Recipes]
strongly2 [definition, in Rocoma.Recipes]
strongly3 [definition, in Rocoma.Recipes_fusion]
SUB [definition, in Rocoma.Recipes_joker]
submits [definition, in Rocoma.Recipes_joker]
submits_app [lemma, in Rocoma.Recipes_joker]
subSn1 [lemma, in Rocoma.Recipes_fv_lemmas]
SubstHSubstComp_term_expr [instance, in Rocoma.Coma]
SubstHSubstComp_term_recipe [instance, in Rocoma.Recipes]
SubstLemmas_expr [instance, in Rocoma.Coma]
SubstLemmas_recipe [instance, in Rocoma.Recipes]
SubstLemmas_term [instance, in Rocoma.Recipes]
subst_depth_hit [lemma, in Rocoma.Recipes_joker]
subst_depth_var [lemma, in Rocoma.Recipes_joker]
subst_depth [definition, in Rocoma.Recipes_joker]
subst_var2_miss [lemma, in Rocoma.Lib.Autosubst_FreeVars]
subst_var_tsubst_recipe_alt_3 [lemma, in Rocoma.Lib.Autosubst_FreeVars]
subst_var_tsubst_recipe_alt_2 [lemma, in Rocoma.Lib.Autosubst_FreeVars]
subst_var_tsubst_recipe_alt [lemma, in Rocoma.Lib.Autosubst_FreeVars]
subst_var_tsubst_alt [lemma, in Rocoma.Lib.Autosubst_FreeVars]
subst_var_tsubst_upn_alt [lemma, in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.SubstHSubstComp_AB [variable, in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.HSubstLemmas_AB [variable, in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.HSubst_AB [variable, in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.SubstLemmas_B [variable, in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.IdsLemmas_B [variable, in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.Subst_B [variable, in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.Rename_B [variable, in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.Ids_B [variable, in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.B [variable, in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.SubstLemmas_A [variable, in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.IdsLemmas_A [variable, in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.Subst_A [variable, in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.Rename_A [variable, in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.Ids_A [variable, in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.A [variable, in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p [section, in Rocoma.Lib.Autosubst_FreeVars]
subst_var_lemma_up1_alt_2 [lemma, in Rocoma.Lib.Autosubst_FreeVars]
subst_var_lemma_up1_alt [lemma, in Rocoma.Lib.Autosubst_FreeVars]
subst_var_lemma_upn_alt2 [lemma, in Rocoma.Lib.Autosubst_FreeVars]
subst_var_lemma_upn_alt [lemma, in Rocoma.Lib.Autosubst_FreeVars]
subst_var2 [definition, in Rocoma.Lib.Autosubst_FreeVars]
subst_var2.SubstLemmas_A [variable, in Rocoma.Lib.Autosubst_FreeVars]
subst_var2.IdsLemmas_A [variable, in Rocoma.Lib.Autosubst_FreeVars]
subst_var2.Subst_A [variable, in Rocoma.Lib.Autosubst_FreeVars]
subst_var2.Rename_A [variable, in Rocoma.Lib.Autosubst_FreeVars]
subst_var2.Ids_A [variable, in Rocoma.Lib.Autosubst_FreeVars]
subst_var2.A [variable, in Rocoma.Lib.Autosubst_FreeVars]
subst_var2 [section, in Rocoma.Lib.Autosubst_FreeVars]
subst_var_hsubst [lemma, in Rocoma.Lib.Autosubst_FreeVars]
subst_var_lemma [lemma, in Rocoma.Lib.Autosubst_FreeVars]
subst_var_tsubst2 [lemma, in Rocoma.Lib.Autosubst_FreeVars]
subst_var_tsubst [lemma, in Rocoma.Lib.Autosubst_FreeVars]
subst_var_tsubst_upn [lemma, in Rocoma.Lib.Autosubst_FreeVars]
subst_var_id [lemma, in Rocoma.Lib.Autosubst_FreeVars]
subst_var_0 [lemma, in Rocoma.Lib.Autosubst_FreeVars]
subst_var_miss_2 [lemma, in Rocoma.Lib.Autosubst_FreeVars]
subst_var_match [lemma, in Rocoma.Lib.Autosubst_FreeVars]
subst_var_miss_1 [lemma, in Rocoma.Lib.Autosubst_FreeVars]
_ .[ _ // _ ] (subst_scope) [notation, in Rocoma.Lib.Autosubst_FreeVars]
subst_var [definition, in Rocoma.Lib.Autosubst_FreeVars]
Subst_var.SubstLemmas_A [variable, in Rocoma.Lib.Autosubst_FreeVars]
Subst_var.IdsLemmas_A [variable, in Rocoma.Lib.Autosubst_FreeVars]
Subst_var.Subst_A [variable, in Rocoma.Lib.Autosubst_FreeVars]
Subst_var.Rename_A [variable, in Rocoma.Lib.Autosubst_FreeVars]
Subst_var.Ids_A [variable, in Rocoma.Lib.Autosubst_FreeVars]
Subst_var.A [variable, in Rocoma.Lib.Autosubst_FreeVars]
Subst_var [section, in Rocoma.Lib.Autosubst_FreeVars]
subst_var2_up [lemma, in Rocoma.Recipes_fv_lemmas]
Subst_expr [instance, in Rocoma.Coma]
subst_neu0 [lemma, in Rocoma.Recipes]
subst_neu [lemma, in Rocoma.Recipes]
Subst_recipe [instance, in Rocoma.Recipes]
Subst_term [instance, in Rocoma.Recipes]
subterm [definition, in Rocoma.Recipes_directly_box]
subterm_neu_idempotent [lemma, in Rocoma.Recipes_directly_box]
subterm_directly_box [lemma, in Rocoma.Recipes_directly_box]
subterm_refl [lemma, in Rocoma.Recipes_directly_box]
SUB_expand [lemma, in Rocoma.Recipes_joker]
sub_cov_hcomp [lemma, in Rocoma.Recipes_joker]
sub_cov_up [lemma, in Rocoma.Recipes_joker]
sub_cov_box [lemma, in Rocoma.Recipes_joker]
sub_cov [definition, in Rocoma.Recipes_joker]
surjective_to_stack2 [lemma, in Rocoma.Recipes_stacks]
surjective_to_stack [lemma, in Rocoma.Recipes_stacks]
T
T [constructor, in Rocoma.Recipes_stacks]TAll [constructor, in Rocoma.Recipes]
TApp [constructor, in Rocoma.Recipes]
TArr [constructor, in Rocoma.Recipes]
TCons [constructor, in Rocoma.Recipes]
term [inductive, in Rocoma.Recipes]
terms [definition, in Rocoma.Recipes_joker]
term_eq_dec [lemma, in Rocoma.Recipes]
term_sind [definition, in Rocoma.Recipes]
term_rec [definition, in Rocoma.Recipes]
term_ind [definition, in Rocoma.Recipes]
term_rect [definition, in Rocoma.Recipes]
Test [section, in Rocoma.Recipes_joker]
TLam [constructor, in Rocoma.Recipes]
TNat [constructor, in Rocoma.Recipes]
Top [constructor, in Rocoma.Recipes]
to_stack_appl_cat [lemma, in Rocoma.Recipes_stacks]
to_stack_appl [lemma, in Rocoma.Recipes_stacks]
to_stack_r [lemma, in Rocoma.Recipes_stacks]
to_stack_idempotent2 [lemma, in Rocoma.Recipes_stacks]
to_stack_idempotent [lemma, in Rocoma.Recipes_stacks]
to_stack_l [lemma, in Rocoma.Recipes_stacks]
to_stack [definition, in Rocoma.Recipes_stacks]
to_stack_rec [definition, in Rocoma.Recipes_stacks]
TRAC [definition, in Rocoma.Recipes_eval]
tractable [definition, in Rocoma.Recipes_eval]
truth [definition, in Rocoma.Recipes_valid_model]
tsubst_ext_one [lemma, in Rocoma.Recipes_typing]
TVar [constructor, in Rocoma.Recipes]
type [inductive, in Rocoma.Recipes]
type_eq_dec [lemma, in Rocoma.Recipes]
type_sind [definition, in Rocoma.Recipes]
type_rec [definition, in Rocoma.Recipes]
type_ind [definition, in Rocoma.Recipes]
type_rect [definition, in Rocoma.Recipes]
ty_params [lemma, in Rocoma.VCgen]
ty_VC [lemma, in Rocoma.VCgen]
ty_neu [constructor, in Rocoma.Recipes_typing]
ty_box [constructor, in Rocoma.Recipes_typing]
ty_tall [constructor, in Rocoma.Recipes_typing]
ty_tlam [constructor, in Rocoma.Recipes_typing]
ty_lam [constructor, in Rocoma.Recipes_typing]
ty_tapp [constructor, in Rocoma.Recipes_typing]
ty_app [constructor, in Rocoma.Recipes_typing]
ty_and [constructor, in Rocoma.Recipes_typing]
ty_imp [constructor, in Rocoma.Recipes_typing]
ty_top [constructor, in Rocoma.Recipes_typing]
ty_zero [constructor, in Rocoma.Recipes_typing]
ty_var [constructor, in Rocoma.Recipes_typing]
t_len [definition, in Rocoma.Recipes_joker]
U
Udiv [definition, in Rocoma.Recipes_joker]UEQU [definition, in Rocoma.VCgen]
UMEET [definition, in Rocoma.VCgen]
UNEU [definition, in Rocoma.VCgen]
UNEU_beta [lemma, in Rocoma.VCgen]
UNEU_lam [lemma, in Rocoma.VCgen]
UNEU_tlam [lemma, in Rocoma.VCgen]
UNEU_app [lemma, in Rocoma.VCgen]
UNEU_and [lemma, in Rocoma.VCgen]
UNEU_neu [lemma, in Rocoma.VCgen]
unfold_box_rel3 [lemma, in Rocoma.Recipes_fusion]
unfold_box_rel [lemma, in Rocoma.Recipes_box_rel]
unfold_to_stack_2_corr [lemma, in Rocoma.Recipes_stacks]
unfold_to_stack_2 [lemma, in Rocoma.Recipes_stacks]
uniformly [definition, in Rocoma.VCgen]
uniformly2 [definition, in Rocoma.VCgen]
uniformly3 [definition, in Rocoma.VCgen]
uniqueness_eval [lemma, in Rocoma.Recipes_eval]
uniqueness_eval_u [lemma, in Rocoma.Recipes_eval]
unnaffectedh_jokerT [lemma, in Rocoma.Recipes_joker]
unnaffected_jokerT [lemma, in Rocoma.Recipes_joker]
upnP [lemma, in Rocoma.Lib.Autosubst_FreeVars]
upnP_cond [lemma, in Rocoma.Lib.Autosubst_FreeVars]
upn_ren_hsubst [lemma, in Rocoma.Lib.Autosubst_FreeVars]
upn_ren_miss [lemma, in Rocoma.Lib.Autosubst_FreeVars]
upn_ren_app [lemma, in Rocoma.Lib.Autosubst_FreeVars]
upn_k_sigma_x [lemma, in Rocoma.Lib.Autosubst_FreeVars]
upn_add [lemma, in Rocoma.Recipes_fv_lemmas]
upn_hcomp [lemma, in Rocoma.Recipes_fv_lemmas]
upn_T_vs_dec [lemma, in Rocoma.Recipes_typing]
upn_miss_var [lemma, in Rocoma.Recipes_typing]
upn1 [lemma, in Rocoma.Lib.Autosubst_FreeVars]
upn2P [lemma, in Rocoma.Lib.Autosubst_FreeVars]
up_compt [lemma, in Rocoma.Lib.Autosubst_FreeVars]
up_comp [lemma, in Rocoma.Lib.Autosubst_FreeVars]
up_ren [lemma, in Rocoma.Lib.Autosubst_FreeVars]
up_ext_one [lemma, in Rocoma.Recipes_typing]
V
V [module, in Rocoma.Recipes_neuneu]val [inductive, in Rocoma.Recipes_valid_model]
VALID [module, in Rocoma.Recipes_valid_sig]
valid_and_imp3_r [lemma, in Rocoma.Recipes_neuneu]
valid_and_imp3_l [lemma, in Rocoma.Recipes_neuneu]
valid_and_mix_l [lemma, in Rocoma.Recipes_neuneu]
valid_and_mix_r [lemma, in Rocoma.Recipes_neuneu]
valid_equiv_cut [lemma, in Rocoma.Recipes_neuneu]
valid_equiv_sym [lemma, in Rocoma.Recipes_neuneu]
valid_imp_imp_split [lemma, in Rocoma.Recipes_neuneu]
valid_weak0 [lemma, in Rocoma.Recipes_neuneu]
valid_fallF_elim [lemma, in Rocoma.Recipes_neuneu]
valid_all_intro [lemma, in Rocoma.Recipes_neuneu]
valid_top0 [lemma, in Rocoma.Recipes_neuneu]
valid_and_and_intro [lemma, in Rocoma.Recipes_neuneu]
valid_assumption_and [lemma, in Rocoma.Recipes_neuneu]
valid_and_l_weak2 [lemma, in Rocoma.Recipes_neuneu]
valid_and_l_sym [lemma, in Rocoma.Recipes_neuneu]
valid_and [lemma, in Rocoma.Recipes_neuneu]
valid_dup [lemma, in Rocoma.Recipes_neuneu]
valid_exfalso [lemma, in Rocoma.Recipes_neuneu]
VALID.valid [axiom, in Rocoma.Recipes_valid_sig]
VALID.valid_all_elim [axiom, in Rocoma.Recipes_valid_sig]
VALID.valid_all_de_bruijn [axiom, in Rocoma.Recipes_valid_sig]
VALID.valid_all_and [axiom, in Rocoma.Recipes_valid_sig]
VALID.valid_all_mono [axiom, in Rocoma.Recipes_valid_sig]
VALID.valid_cut [axiom, in Rocoma.Recipes_valid_sig]
VALID.valid_contr [axiom, in Rocoma.Recipes_valid_sig]
VALID.valid_weak [axiom, in Rocoma.Recipes_valid_sig]
VALID.valid_imp_elim [axiom, in Rocoma.Recipes_valid_sig]
VALID.valid_imp_intro [axiom, in Rocoma.Recipes_valid_sig]
VALID.valid_and_l_cycle [axiom, in Rocoma.Recipes_valid_sig]
VALID.valid_and_intro_l [axiom, in Rocoma.Recipes_valid_sig]
VALID.valid_and_elim [axiom, in Rocoma.Recipes_valid_sig]
VALID.valid_and_intro [axiom, in Rocoma.Recipes_valid_sig]
VALID.valid_consistent [axiom, in Rocoma.Recipes_valid_sig]
VALID.valid_contradiction [axiom, in Rocoma.Recipes_valid_sig]
VALID.valid_top_l2 [axiom, in Rocoma.Recipes_valid_sig]
VALID.valid_top_l1 [axiom, in Rocoma.Recipes_valid_sig]
VALID.valid_top [axiom, in Rocoma.Recipes_valid_sig]
VALID.valid_assumption [axiom, in Rocoma.Recipes_valid_sig]
_ ⟛ _ (valid_scope) [notation, in Rocoma.Recipes_valid_sig]
||- _ (valid_scope) [notation, in Rocoma.Recipes_valid_sig]
_ ||- _ (valid_scope) [notation, in Rocoma.Recipes_valid_sig]
val_sind [definition, in Rocoma.Recipes_valid_model]
val_rec [definition, in Rocoma.Recipes_valid_model]
val_ind [definition, in Rocoma.Recipes_valid_model]
val_rect [definition, in Rocoma.Recipes_valid_model]
Var [constructor, in Rocoma.Recipes]
var_not_free_upn_ge [lemma, in Rocoma.Lib.Autosubst_FreeVars]
var_not_free_upn_mid [lemma, in Rocoma.Lib.Autosubst_FreeVars]
var_not_free_add [lemma, in Rocoma.Lib.Autosubst_FreeVars]
var_not_free_upn_lt [lemma, in Rocoma.Lib.Autosubst_FreeVars]
var_not_free [definition, in Rocoma.Lib.Autosubst_FreeVars]
var_not_free_upn_lt_gen [lemma, in Rocoma.Recipes_fv_lemmas]
var_not_free_neu [lemma, in Rocoma.Recipes_fv_lemmas]
var_not_free_hsubst [lemma, in Rocoma.Recipes_fv_lemmas]
var_eq_dec [lemma, in Rocoma.Recipes]
VC [definition, in Rocoma.VCgen]
vcall [definition, in Rocoma.Recipes_joker]
vcall_hsubst [lemma, in Rocoma.Recipes_joker]
VCgen [library]
VCons [constructor, in Rocoma.Recipes_valid_model]
VC_meet [lemma, in Rocoma.VCgen]
VC_split [lemma, in Rocoma.VCgen]
VC_notnot [lemma, in Rocoma.VCgen]
VC_neutral [lemma, in Rocoma.VCgen]
VC_ren [lemma, in Rocoma.VCgen]
VC_hsubst [lemma, in Rocoma.VCgen]
VNat [constructor, in Rocoma.Recipes_valid_model]
Void [constructor, in Rocoma.Recipes]
void_stack [lemma, in Rocoma.Recipes_stacks]
VProp [constructor, in Rocoma.Recipes_valid_model]
W
weakly [definition, in Rocoma.Recipes]weakly_uniform2 [definition, in Rocoma.VCgen]
weakly2 [definition, in Rocoma.Recipes]
weight [definition, in Rocoma.Recipes]
weight_neu [lemma, in Rocoma.Recipes]
weight_subst_box [lemma, in Rocoma.Recipes]
weight_subst_hsubst [lemma, in Rocoma.Recipes]
weight_hsubst_subst [lemma, in Rocoma.Recipes]
weight_hsubst [lemma, in Rocoma.Recipes]
weight_pos [lemma, in Rocoma.Recipes]
wf_config [definition, in Rocoma.Coma]
wt_config2expr [lemma, in Rocoma.Coma]
WUEQU [definition, in Rocoma.VCgen]
WUEQU_tlam [lemma, in Rocoma.VCgen]
WUEQU_and_comm [lemma, in Rocoma.VCgen]
WUEQU_app [lemma, in Rocoma.VCgen]
Z
Zero [constructor, in Rocoma.Recipes]_
__has_type_eq_ab_refuted [lemma, in Rocoma.Recipes_typing]other
[ _ ⊩ _ ↦ _ ] (coma_scope) [notation, in Rocoma.Coma][ _ ⊩ _ :- _ ] (coma_scope) [notation, in Rocoma.Coma]
_ .[ _ // _ ] (subst_scope) [notation, in Rocoma.Lib.Autosubst_FreeVars]
\[ _ ] _ (ty_scope) [notation, in Rocoma.Recipes_joker]
_ --> _ (ty_scope) [notation, in Rocoma.Recipes_joker]
◻ (ty_scope) [notation, in Rocoma.Recipes_joker]
[ ⊢ _ :- _ ] (ty_scope) [notation, in Rocoma.Recipes_typing]
[ _ , _ , _ ⊢ _ :- _ ] (ty_scope) [notation, in Rocoma.Recipes_typing]
[ ⊨ _ :- _ ] (ty_scope) [notation, in Rocoma.Recipes_stacks]
[ _ , _ , _ ⊨ _ :- _ ] (ty_scope) [notation, in Rocoma.Recipes_stacks]
_ ++ _ (valid_scope) [notation, in Rocoma.Recipes_valid_sig]
_ ⟛ _ (valid_scope) [notation, in Rocoma.Recipes_neuneu]
||- _ (valid_scope) [notation, in Rocoma.Recipes_neuneu]
_ ||- _ (valid_scope) [notation, in Rocoma.Recipes_neuneu]
_ ∘ _ [notation, in Rocoma.Recipes_stacks]
Notation Index
M
_ ⟛ _ (model_scope) [in Rocoma.Recipes_valid_model]||- _ (model_scope) [in Rocoma.Recipes_valid_model]
_ ||- _ (model_scope) [in Rocoma.Recipes_valid_model]
S
_ .[ _ // _ ] (subst_scope) [in Rocoma.Lib.Autosubst_FreeVars]V
_ ⟛ _ (valid_scope) [in Rocoma.Recipes_valid_sig]||- _ (valid_scope) [in Rocoma.Recipes_valid_sig]
_ ||- _ (valid_scope) [in Rocoma.Recipes_valid_sig]
other
[ _ ⊩ _ ↦ _ ] (coma_scope) [in Rocoma.Coma][ _ ⊩ _ :- _ ] (coma_scope) [in Rocoma.Coma]
_ .[ _ // _ ] (subst_scope) [in Rocoma.Lib.Autosubst_FreeVars]
\[ _ ] _ (ty_scope) [in Rocoma.Recipes_joker]
_ --> _ (ty_scope) [in Rocoma.Recipes_joker]
◻ (ty_scope) [in Rocoma.Recipes_joker]
[ ⊢ _ :- _ ] (ty_scope) [in Rocoma.Recipes_typing]
[ _ , _ , _ ⊢ _ :- _ ] (ty_scope) [in Rocoma.Recipes_typing]
[ ⊨ _ :- _ ] (ty_scope) [in Rocoma.Recipes_stacks]
[ _ , _ , _ ⊨ _ :- _ ] (ty_scope) [in Rocoma.Recipes_stacks]
_ ++ _ (valid_scope) [in Rocoma.Recipes_valid_sig]
_ ⟛ _ (valid_scope) [in Rocoma.Recipes_neuneu]
||- _ (valid_scope) [in Rocoma.Recipes_neuneu]
_ ||- _ (valid_scope) [in Rocoma.Recipes_neuneu]
_ ∘ _ [in Rocoma.Recipes_stacks]
Module Index
M
Model [in Rocoma.Recipes_valid_model]V
V [in Rocoma.Recipes_neuneu]VALID [in Rocoma.Recipes_valid_sig]
Variable Index
B
Both.A [in Rocoma.Lib.Autosubst_FreeVars]Both.B [in Rocoma.Lib.Autosubst_FreeVars]
Both.HSubstLemmas_AB [in Rocoma.Lib.Autosubst_FreeVars]
Both.HSubst_AB [in Rocoma.Lib.Autosubst_FreeVars]
Both.IdsLemmas_B [in Rocoma.Lib.Autosubst_FreeVars]
Both.IdsLemmas_A [in Rocoma.Lib.Autosubst_FreeVars]
Both.Ids_B [in Rocoma.Lib.Autosubst_FreeVars]
Both.Ids_A [in Rocoma.Lib.Autosubst_FreeVars]
Both.Rename_B [in Rocoma.Lib.Autosubst_FreeVars]
Both.Rename_A [in Rocoma.Lib.Autosubst_FreeVars]
Both.SubstHSubstComp_AB [in Rocoma.Lib.Autosubst_FreeVars]
Both.SubstLemmas_B [in Rocoma.Lib.Autosubst_FreeVars]
Both.SubstLemmas_A [in Rocoma.Lib.Autosubst_FreeVars]
Both.Subst_B [in Rocoma.Lib.Autosubst_FreeVars]
Both.Subst_A [in Rocoma.Lib.Autosubst_FreeVars]
F
FreeVars.A [in Rocoma.Lib.Autosubst_FreeVars]FreeVars.B [in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.HSubstLemmas_AB [in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.HSubst_AB [in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.IdsLemmas_B [in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.IdsLemmas_A [in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.Ids_B [in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.Ids_A [in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.Rename_B [in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.Rename_A [in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.SubstHSubstComp_AB [in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.SubstLemmas_B [in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.SubstLemmas_A [in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.Subst_B [in Rocoma.Lib.Autosubst_FreeVars]
FreeVars.Subst_A [in Rocoma.Lib.Autosubst_FreeVars]
M
MMapInstances.A [in Rocoma.Autosubst.AutosubstSsr]MMapInstances.B [in Rocoma.Autosubst.AutosubstSsr]
MMapInstances.C [in Rocoma.Autosubst.AutosubstSsr]
MMapInstances.MMapExt_A_C [in Rocoma.Autosubst.AutosubstSsr]
MMapInstances.MMapExt_A_B [in Rocoma.Autosubst.AutosubstSsr]
MMapInstances.MMapLemmas_A_C [in Rocoma.Autosubst.AutosubstSsr]
MMapInstances.MMapLemmas_A_B [in Rocoma.Autosubst.AutosubstSsr]
MMapInstances.MMap_A_C [in Rocoma.Autosubst.AutosubstSsr]
MMapInstances.MMap_A_B [in Rocoma.Autosubst.AutosubstSsr]
O
OpSem.valid [in Rocoma.Coma]S
subst_var2p.SubstHSubstComp_AB [in Rocoma.Lib.Autosubst_FreeVars]subst_var2p.HSubstLemmas_AB [in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.HSubst_AB [in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.SubstLemmas_B [in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.IdsLemmas_B [in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.Subst_B [in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.Rename_B [in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.Ids_B [in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.B [in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.SubstLemmas_A [in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.IdsLemmas_A [in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.Subst_A [in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.Rename_A [in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.Ids_A [in Rocoma.Lib.Autosubst_FreeVars]
subst_var2p.A [in Rocoma.Lib.Autosubst_FreeVars]
subst_var2.SubstLemmas_A [in Rocoma.Lib.Autosubst_FreeVars]
subst_var2.IdsLemmas_A [in Rocoma.Lib.Autosubst_FreeVars]
subst_var2.Subst_A [in Rocoma.Lib.Autosubst_FreeVars]
subst_var2.Rename_A [in Rocoma.Lib.Autosubst_FreeVars]
subst_var2.Ids_A [in Rocoma.Lib.Autosubst_FreeVars]
subst_var2.A [in Rocoma.Lib.Autosubst_FreeVars]
Subst_var.SubstLemmas_A [in Rocoma.Lib.Autosubst_FreeVars]
Subst_var.IdsLemmas_A [in Rocoma.Lib.Autosubst_FreeVars]
Subst_var.Subst_A [in Rocoma.Lib.Autosubst_FreeVars]
Subst_var.Rename_A [in Rocoma.Lib.Autosubst_FreeVars]
Subst_var.Ids_A [in Rocoma.Lib.Autosubst_FreeVars]
Subst_var.A [in Rocoma.Lib.Autosubst_FreeVars]
Library Index
A
AutosubstSsrAutosubst_FreeVars
C
ComaE
ExtractionM
MainMy_tactics
R
RecipesRecipes_joker
Recipes_directly_box
Recipes_fv_lemmas
Recipes_logrel
Recipes_stacks
Recipes_evalf
Recipes_box_rel
Recipes_valid_model
Recipes_fusion
Recipes_eval
Recipes_neuneu
Recipes_valid_sig
Recipes_typing
V
VCgenLemma Index
A
aligned_jstack [in Rocoma.Recipes_joker]aligned_type_void2 [in Rocoma.Recipes_logrel]
aligned_closed_appl2 [in Rocoma.Recipes_logrel]
aligned_hsubst [in Rocoma.Recipes_logrel]
aligned_neu [in Rocoma.Recipes_logrel]
aligned_cons_t [in Rocoma.Recipes_logrel]
aligned_cons_r [in Rocoma.Recipes_logrel]
aligned_complete [in Rocoma.Recipes_logrel]
aligned_type_void [in Rocoma.Recipes_logrel]
allzbb_hsubst [in Rocoma.Recipes_neuneu]
allzbb_subst_var [in Rocoma.Recipes_neuneu]
allzbb_subst_var_n [in Rocoma.Recipes_neuneu]
allzbb_neu [in Rocoma.Recipes_neuneu]
all3_fusion_refl_neu [in Rocoma.Recipes_fusion]
appl_hsubst [in Rocoma.Recipes_stacks]
appl_one_stept [in Rocoma.Recipes_stacks]
appl_one_step [in Rocoma.Recipes_stacks]
appl_not_tlam [in Rocoma.Recipes_stacks]
appl_not_neu [in Rocoma.Recipes_stacks]
appl_not_box [in Rocoma.Recipes_stacks]
appl_not_and [in Rocoma.Recipes_stacks]
appl_not_imp [in Rocoma.Recipes_stacks]
appl_not_lam [in Rocoma.Recipes_stacks]
appl_not_top [in Rocoma.Recipes_stacks]
appl_not_zero [in Rocoma.Recipes_stacks]
appl_not_var [in Rocoma.Recipes_stacks]
B
box_rel3_box_ids [in Rocoma.Recipes_fusion]box_rel3_type_det13 [in Rocoma.Recipes_fusion]
box_rel3_type_det12 [in Rocoma.Recipes_fusion]
box_rel3_preserved_hsubst0 [in Rocoma.Recipes_fusion]
box_rel3_preserved_hsubst [in Rocoma.Recipes_fusion]
box_rel3_preserved_ren [in Rocoma.Recipes_fusion]
box_rel3_preserved_subst0 [in Rocoma.Recipes_fusion]
box_rel3_preserved_subst [in Rocoma.Recipes_fusion]
box_rel3_preserved_neu [in Rocoma.Recipes_fusion]
box_rel3_nobox [in Rocoma.Recipes_fusion]
box_rel2_nobox [in Rocoma.Recipes_box_rel]
box_rel2_box_ids [in Rocoma.Recipes_box_rel]
box_rel2_type_det [in Rocoma.Recipes_box_rel]
box_rel2_preserved_hsubst0 [in Rocoma.Recipes_box_rel]
box_rel2_preserved_hsubst [in Rocoma.Recipes_box_rel]
box_rel2_preserved_ren [in Rocoma.Recipes_box_rel]
box_rel2_preserved_subst0 [in Rocoma.Recipes_box_rel]
box_rel2_preserved_subst [in Rocoma.Recipes_box_rel]
box_rel2_preserved_neu [in Rocoma.Recipes_box_rel]
box_rel2_weight_eq [in Rocoma.Recipes_box_rel]
box_rel_nobox [in Rocoma.Recipes_box_rel]
box_rel_box_ids [in Rocoma.Recipes_box_rel]
box_rel_preserved_neu [in Rocoma.Recipes_box_rel]
box_rel_preserved_hsubst0 [in Rocoma.Recipes_box_rel]
box_rel_preserved_hsubst [in Rocoma.Recipes_box_rel]
box_rel_preserved_ren [in Rocoma.Recipes_box_rel]
box_rel_preserved_subst0 [in Rocoma.Recipes_box_rel]
box_rel_preserved_subst [in Rocoma.Recipes_box_rel]
b1 [in Rocoma.Recipes_neuneu]
C
cabs_cty [in Rocoma.Coma]closedh_jokerT [in Rocoma.Recipes_joker]
closedh_joker [in Rocoma.Recipes_joker]
closedh_ids [in Rocoma.Lib.Autosubst_FreeVars]
closedh_eq [in Rocoma.Lib.Autosubst_FreeVars]
closedh_fvh [in Rocoma.Recipes_fv_lemmas]
closedh_hsubst [in Rocoma.Recipes_fv_lemmas]
closedh_sneu2 [in Rocoma.Recipes_fv_lemmas]
closedh_sneu [in Rocoma.Recipes_fv_lemmas]
closedh_tall1 [in Rocoma.Recipes_fv_lemmas]
closedh_tlam1 [in Rocoma.Recipes_fv_lemmas]
closedh_imp [in Rocoma.Recipes_fv_lemmas]
closedh_tapp [in Rocoma.Recipes_fv_lemmas]
closedh_box1 [in Rocoma.Recipes_fv_lemmas]
closedh_box [in Rocoma.Recipes_fv_lemmas]
closedh_neu1 [in Rocoma.Recipes_fv_lemmas]
closedh_neu [in Rocoma.Recipes_fv_lemmas]
closedh_lam [in Rocoma.Recipes_fv_lemmas]
closedh_and [in Rocoma.Recipes_fv_lemmas]
closedh_app [in Rocoma.Recipes_fv_lemmas]
closedh_top [in Rocoma.Recipes_fv_lemmas]
closed_jokerT [in Rocoma.Recipes_joker]
closed_call [in Rocoma.Recipes_joker]
closed_joker [in Rocoma.Recipes_joker]
closed_subst_closed [in Rocoma.VCgen]
closed_ids [in Rocoma.Lib.Autosubst_FreeVars]
closed_eq [in Rocoma.Lib.Autosubst_FreeVars]
closed_fv [in Rocoma.Recipes_fv_lemmas]
closed_unaffectedh [in Rocoma.Recipes_fv_lemmas]
closed_unaffected_term [in Rocoma.Recipes_fv_lemmas]
closed_subst [in Rocoma.Recipes_fv_lemmas]
closed_unaffected [in Rocoma.Recipes_fv_lemmas]
closed_sneu2 [in Rocoma.Recipes_fv_lemmas]
closed_sneu [in Rocoma.Recipes_fv_lemmas]
closed_tall1 [in Rocoma.Recipes_fv_lemmas]
closed_tall [in Rocoma.Recipes_fv_lemmas]
closed_tlam1 [in Rocoma.Recipes_fv_lemmas]
closed_tlam [in Rocoma.Recipes_fv_lemmas]
closed_imp1 [in Rocoma.Recipes_fv_lemmas]
closed_imp [in Rocoma.Recipes_fv_lemmas]
closed_tapp1 [in Rocoma.Recipes_fv_lemmas]
closed_tapp [in Rocoma.Recipes_fv_lemmas]
closed_box1 [in Rocoma.Recipes_fv_lemmas]
closed_box [in Rocoma.Recipes_fv_lemmas]
closed_neu1 [in Rocoma.Recipes_fv_lemmas]
closed_neu [in Rocoma.Recipes_fv_lemmas]
closed_lam1 [in Rocoma.Recipes_fv_lemmas]
closed_lam [in Rocoma.Recipes_fv_lemmas]
closed_and1 [in Rocoma.Recipes_fv_lemmas]
closed_and [in Rocoma.Recipes_fv_lemmas]
closed_app1 [in Rocoma.Recipes_fv_lemmas]
closed_app [in Rocoma.Recipes_fv_lemmas]
closed_top [in Rocoma.Recipes_fv_lemmas]
closed_has_ty_weak [in Rocoma.Recipes_typing]
closed_has_ty_contr [in Rocoma.Recipes_typing]
closed_stack_hsubst [in Rocoma.Recipes_stacks]
closed_stack_in [in Rocoma.Recipes_stacks]
closed_appl_neu_stack [in Rocoma.Recipes_stacks]
closed_appl_neu_head [in Rocoma.Recipes_stacks]
closed_appl_inv_strong [in Rocoma.Recipes_stacks]
closed_appl [in Rocoma.Recipes_stacks]
closing_box [in Rocoma.VCgen]
closing_hsubst [in Rocoma.VCgen]
conj_in_joker_call [in Rocoma.Recipes_joker]
conj_in_call_inst [in Rocoma.Recipes_joker]
conj_in_joker_mem [in Rocoma.Recipes_joker]
conj_in_joker_inst [in Rocoma.Recipes_joker]
conj_in_leaf [in Rocoma.Recipes_joker]
conj_in_subst_closed [in Rocoma.Recipes_joker]
conj_in_hsubst [in Rocoma.Recipes_joker]
covers_shift [in Rocoma.Recipes_joker]
covers_below_hsubst0 [in Rocoma.Recipes_joker]
covers_hsubst [in Rocoma.Recipes_joker]
covers_subst [in Rocoma.Recipes_joker]
covers_app_ren [in Rocoma.Recipes_joker]
covers_ren [in Rocoma.Recipes_joker]
covers_neu [in Rocoma.Recipes_joker]
covers_stack_incl [in Rocoma.Recipes_joker]
covers_appl [in Rocoma.Recipes_joker]
covers_app_appl [in Rocoma.Recipes_joker]
covers_below_app [in Rocoma.Recipes_joker]
cross_lemma [in Rocoma.Recipes_fusion]
ctx_insertion0 [in Rocoma.Recipes_typing]
ctx_ext1 [in Rocoma.Recipes_directly_box]
ctx_ext0 [in Rocoma.Recipes_directly_box]
c_3_10_4 [in Rocoma.Recipes_fusion]
c_3_10_3 [in Rocoma.Recipes_fusion]
c_3_10_2void [in Rocoma.Recipes_fusion]
c_3_10_2 [in Rocoma.Recipes_fusion]
c_3_10_1 [in Rocoma.Recipes_fusion]
c1 [in Rocoma.Recipes_fusion]
c1a [in Rocoma.Recipes_fusion]
D
db3_proj3 [in Rocoma.Recipes_directly_box]db3_proj2 [in Rocoma.Recipes_directly_box]
db3_proj1 [in Rocoma.Recipes_directly_box]
dec_allzbb [in Rocoma.Recipes_neuneu]
depth_neu [in Rocoma.Recipes]
depth_hsubst [in Rocoma.Recipes]
depth_nonneg [in Rocoma.Recipes]
depth_dec [in Rocoma.Recipes]
directly_box_closed [in Rocoma.Recipes_directly_box]
directly_box_mem_box [in Rocoma.Recipes_directly_box]
directly_box_neu [in Rocoma.Recipes_directly_box]
directly_box_neu_idempotent [in Rocoma.Recipes_directly_box]
directly_box_depth [in Rocoma.Recipes_directly_box]
directly_box_ty [in Rocoma.Recipes_directly_box]
directly_box_dec [in Rocoma.Recipes_directly_box]
directly_box_ty_ext [in Rocoma.Recipes_directly_box]
directly_box_db_coincide [in Rocoma.Recipes_directly_box]
d1 [in Rocoma.Recipes_joker]
d1_1 [in Rocoma.Recipes_joker]
E
eappl_ty [in Rocoma.Coma]edefs_ty [in Rocoma.Coma]
entails_neu [in Rocoma.Recipes_fusion]
entails_36 [in Rocoma.Recipes_neuneu]
entails_trans [in Rocoma.Recipes_neuneu]
entails_refl [in Rocoma.Recipes_neuneu]
entails_toptop [in Rocoma.Recipes_neuneu]
ent_jokerT [in Rocoma.Recipes_joker]
ENT_Neu [in Rocoma.Recipes_fusion]
ENT_and_comm [in Rocoma.Recipes_fusion]
ENT_and2 [in Rocoma.Recipes_fusion]
ENT_and1 [in Rocoma.Recipes_fusion]
ENT_and_intro [in Rocoma.Recipes_fusion]
ENT_and_neu [in Rocoma.Recipes_fusion]
ENT_tlam [in Rocoma.Recipes_fusion]
ENT_and [in Rocoma.Recipes_neuneu]
ENT_expand [in Rocoma.Recipes_neuneu]
EQU_neu2 [in Rocoma.Recipes_fusion]
EQU_and_Neu2 [in Rocoma.Recipes_fusion]
EQU_and_Neu1 [in Rocoma.Recipes_fusion]
EQU_and_comm [in Rocoma.Recipes_fusion]
EQU_tlam [in Rocoma.Recipes_fusion]
EQU_neuneuneu [in Rocoma.Recipes_fusion]
EQU_Void_neu [in Rocoma.Recipes_fusion]
evalf_unique [in Rocoma.Recipes_evalf]
evalf_def [in Rocoma.Recipes_evalf]
evalf_complete [in Rocoma.Recipes_evalf]
evalf_mono [in Rocoma.Recipes_evalf]
evalf_sound [in Rocoma.Recipes_evalf]
eval_conj_in [in Rocoma.Recipes_joker]
eval_joker_abs [in Rocoma.Recipes_joker]
eval_compose_and [in Rocoma.Recipes_fusion]
eval_fall_inv [in Rocoma.Recipes_eval]
eval_hsubst [in Rocoma.Recipes_eval]
eval_def [in Rocoma.Recipes_eval]
eval_Neu [in Rocoma.Recipes_eval]
eval_move_stack_left [in Rocoma.Recipes_eval]
eval_move_stack_right [in Rocoma.Recipes_eval]
eval_move_stack [in Rocoma.Recipes_eval]
eval_eval0_2 [in Rocoma.Recipes_eval]
eval_eval0_1 [in Rocoma.Recipes_eval]
eval_eval0 [in Rocoma.Recipes_eval]
exists_unique_eval [in Rocoma.Recipes_eval]
F
fallF_subst [in Rocoma.Recipes]fall_hsubst [in Rocoma.Recipes]
fall_subst [in Rocoma.Recipes]
fusion_cross_neu [in Rocoma.Recipes_fusion]
fusion_allp_split [in Rocoma.Recipes_fusion]
fusion_meet [in Rocoma.Recipes_fusion]
fusion_has_type [in Rocoma.Recipes_fusion]
fusion_closed [in Rocoma.Recipes_fusion]
fusion_fv [in Rocoma.Recipes_fusion]
fusion_db3_fusion [in Rocoma.Recipes_fusion]
fusion_preserved_hsubst [in Rocoma.Recipes_fusion]
fusion_preserved_neu [in Rocoma.Recipes_fusion]
fusion_refl_neu [in Rocoma.Recipes_fusion]
fusion_swap [in Rocoma.Recipes_fusion]
fusion_refl [in Rocoma.Recipes_fusion]
fvh_joker [in Rocoma.Recipes_joker]
fvh_ids [in Rocoma.Lib.Autosubst_FreeVars]
fvh_hsubst [in Rocoma.Recipes_fv_lemmas]
fvh_sneu [in Rocoma.Recipes_fv_lemmas]
fvh_fall [in Rocoma.Recipes_fv_lemmas]
fvh_tall [in Rocoma.Recipes_fv_lemmas]
fvh_tlam [in Rocoma.Recipes_fv_lemmas]
fvh_imp [in Rocoma.Recipes_fv_lemmas]
fvh_tapp [in Rocoma.Recipes_fv_lemmas]
fvh_box [in Rocoma.Recipes_fv_lemmas]
fvh_neu [in Rocoma.Recipes_fv_lemmas]
fvh_lam [in Rocoma.Recipes_fv_lemmas]
fvh_and [in Rocoma.Recipes_fv_lemmas]
fvh_app [in Rocoma.Recipes_fv_lemmas]
fvu_succ [in Rocoma.Lib.Autosubst_FreeVars]
fvu_fvu2 [in Rocoma.Lib.Autosubst_FreeVars]
fvu_equal_close2 [in Rocoma.Lib.Autosubst_FreeVars]
fvu_equal_close [in Rocoma.Lib.Autosubst_FreeVars]
fvu_subst [in Rocoma.Recipes_fv_lemmas]
fvu_tall [in Rocoma.Recipes_fv_lemmas]
fvu_tlam [in Rocoma.Recipes_fv_lemmas]
fvu0 [in Rocoma.Lib.Autosubst_FreeVars]
fvu2_subst [in Rocoma.Recipes_fv_lemmas]
fvu2_lam [in Rocoma.Recipes_fv_lemmas]
fvu2_tall_op [in Rocoma.Recipes_fv_lemmas]
fvu2_tlam_op [in Rocoma.Recipes_fv_lemmas]
fvu2_tall [in Rocoma.Recipes_fv_lemmas]
fvu2_tlam [in Rocoma.Recipes_fv_lemmas]
fvu2_var [in Rocoma.Recipes_fv_lemmas]
fv_joker [in Rocoma.Recipes_joker]
fv_hsubst [in Rocoma.Lib.Autosubst_FreeVars]
fv_unaffected_lift [in Rocoma.Lib.Autosubst_FreeVars]
fv_ids_eq [in Rocoma.Lib.Autosubst_FreeVars]
fv_unaffectedh2 [in Rocoma.Recipes_fv_lemmas]
fv_unaffectedh [in Rocoma.Recipes_fv_lemmas]
fv_unaffected_term [in Rocoma.Recipes_fv_lemmas]
fv_unaffected [in Rocoma.Recipes_fv_lemmas]
fv_sneu [in Rocoma.Recipes_fv_lemmas]
fv_fall [in Rocoma.Recipes_fv_lemmas]
fv_tall [in Rocoma.Recipes_fv_lemmas]
fv_tlam [in Rocoma.Recipes_fv_lemmas]
fv_imp [in Rocoma.Recipes_fv_lemmas]
fv_tapp [in Rocoma.Recipes_fv_lemmas]
fv_box1 [in Rocoma.Recipes_fv_lemmas]
fv_box [in Rocoma.Recipes_fv_lemmas]
fv_neu [in Rocoma.Recipes_fv_lemmas]
fv_lam [in Rocoma.Recipes_fv_lemmas]
fv_and [in Rocoma.Recipes_fv_lemmas]
fv_app [in Rocoma.Recipes_fv_lemmas]
fv_tvar [in Rocoma.Recipes_fv_lemmas]
fv_var [in Rocoma.Recipes_fv_lemmas]
fv_has_ty [in Rocoma.Recipes_typing]
fv_plage_upn_gen [in Rocoma.Recipes_typing]
fv_plage_upn_cut_below [in Rocoma.Recipes_typing]
fv_plage_upn_cut_in [in Rocoma.Recipes_typing]
fv_plage_glue [in Rocoma.Recipes_typing]
fv_plage_shift [in Rocoma.Recipes_typing]
fv_plage_mono [in Rocoma.Recipes_typing]
fv_plage_eq [in Rocoma.Recipes_typing]
fv1 [in Rocoma.Lib.Autosubst_FreeVars]
fv1h [in Rocoma.Lib.Autosubst_FreeVars]
fv1hh [in Rocoma.Lib.Autosubst_FreeVars]
f_ext_subst [in Rocoma.Lib.My_tactics]
G
golfouse [in Rocoma.Recipes_fv_lemmas]golfousec_le [in Rocoma.Recipes_fv_lemmas]
H
has_type_jokerT [in Rocoma.Recipes_joker]has_type_joker [in Rocoma.Recipes_joker]
has_type_joker_gen [in Rocoma.Recipes_joker]
has_type_inst_neu [in Rocoma.VCgen]
has_type_inst [in Rocoma.VCgen]
has_type_closing [in Rocoma.VCgen]
has_type_VC [in Rocoma.VCgen]
has_type_rall [in Rocoma.VCgen]
has_type_fall [in Rocoma.Recipes_typing]
has_type_beta [in Rocoma.Recipes_typing]
has_type_beta_gen [in Rocoma.Recipes_typing]
has_type_subst [in Rocoma.Recipes_typing]
has_type_ren [in Rocoma.Recipes_typing]
has_type_lower_b0 [in Rocoma.Recipes_typing]
has_type_hsubst1 [in Rocoma.Recipes_typing]
has_type_lower_1 [in Rocoma.Recipes_typing]
has_type_lower_n1 [in Rocoma.Recipes_typing]
has_type_lower_0 [in Rocoma.Recipes_typing]
has_type_lower [in Rocoma.Recipes_typing]
has_type_lower_b [in Rocoma.Recipes_typing]
has_type_hshift [in Rocoma.Recipes_typing]
has_type_hshift_cut_below [in Rocoma.Recipes_typing]
has_type_hshift_cut_in [in Rocoma.Recipes_typing]
has_type_hsubst_ext [in Rocoma.Recipes_typing]
has_type_hsubst_0 [in Rocoma.Recipes_typing]
has_type_swap_a [in Rocoma.Recipes_typing]
has_type_hsubst_upn [in Rocoma.Recipes_typing]
has_type_neu [in Rocoma.Recipes_typing]
has_type_det [in Rocoma.Recipes_typing]
has_type_appl_neu_stack [in Rocoma.Recipes_stacks]
has_type_appl_neu_head [in Rocoma.Recipes_stacks]
has_type_appl2_hole [in Rocoma.Recipes_stacks]
has_type_appl_hole [in Rocoma.Recipes_stacks]
has_type_appl2_neu [in Rocoma.Recipes_stacks]
has_type_appl_neu_head_ex [in Rocoma.Recipes_stacks]
has_type_appl2 [in Rocoma.Recipes_stacks]
has_type_appl [in Rocoma.Recipes_stacks]
has_type_appl_void [in Rocoma.Recipes_stacks]
hsubst_T_is_ren [in Rocoma.Recipes_typing]
I
ids_inj_False [in Rocoma.Lib.Autosubst_FreeVars]inner1 [in Rocoma.Recipes_eval]
inner2g [in Rocoma.Recipes_eval]
inst_nth [in Rocoma.Recipes_fv_lemmas]
inst_high [in Rocoma.Recipes_fv_lemmas]
inversion_neu_box [in Rocoma.Recipes]
inversion_neu_neu [in Rocoma.Recipes]
inversion_neu_tall [in Rocoma.Recipes]
inversion_neu_tlam [in Rocoma.Recipes]
inversion_neu_imp [in Rocoma.Recipes]
inversion_neu_lam [in Rocoma.Recipes]
inversion_neu_tapp [in Rocoma.Recipes]
inversion_neu_app [in Rocoma.Recipes]
inversion_neu_and [in Rocoma.Recipes]
inversion_neu_top [in Rocoma.Recipes]
inversion_neu_var [in Rocoma.Recipes]
in_aligned_arg [in Rocoma.Recipes_logrel]
in_stack_hsubst [in Rocoma.Recipes_stacks]
J
joker_entails [in Rocoma.Recipes_joker]joker_call_inst [in Rocoma.Recipes_joker]
joker_bot [in Rocoma.Recipes_joker]
joker_entails_mem [in Rocoma.Recipes_joker]
joker_hsubst [in Rocoma.Recipes_joker]
joker_subst [in Rocoma.Recipes_joker]
L
lift_inj_ids [in Rocoma.Lib.Autosubst_FreeVars]logical_relation_lemma3_proj2 [in Rocoma.Recipes_fusion]
logical_relation_lemma3_proj1 [in Rocoma.Recipes_fusion]
logical_relation_lemma3 [in Rocoma.Recipes_fusion]
logical_relation_lemma2_proj2 [in Rocoma.Recipes_logrel]
logical_relation_lemma2_proj1 [in Rocoma.Recipes_logrel]
logical_relation_lemma2 [in Rocoma.Recipes_logrel]
logical_relation_lemma_proj2 [in Rocoma.Recipes_logrel]
logical_relation_lemma_proj1 [in Rocoma.Recipes_logrel]
logical_relation_lemma [in Rocoma.Recipes_logrel]
logrel3_andl_ren [in Rocoma.Recipes_fusion]
logrel3_andl [in Rocoma.Recipes_fusion]
l_3_10 [in Rocoma.Recipes_fusion]
M
meet_refl [in Rocoma.Recipes_fusion]mem_ren_shift [in Rocoma.Recipes_joker]
mem_ren_hsubst [in Rocoma.Recipes_joker]
mem_ren_ren [in Rocoma.Recipes_joker]
mem_ren_closed [in Rocoma.Recipes_joker]
mem_ren_0 [in Rocoma.Recipes_joker]
mem_box_depth [in Rocoma.Recipes_directly_box]
Model.valid_all_elim [in Rocoma.Recipes_valid_model]
Model.valid_all_de_bruijn [in Rocoma.Recipes_valid_model]
Model.valid_all_and [in Rocoma.Recipes_valid_model]
Model.valid_all_mono [in Rocoma.Recipes_valid_model]
Model.valid_cut [in Rocoma.Recipes_valid_model]
Model.valid_contr [in Rocoma.Recipes_valid_model]
Model.valid_weak [in Rocoma.Recipes_valid_model]
Model.valid_imp_elim [in Rocoma.Recipes_valid_model]
Model.valid_imp_intro [in Rocoma.Recipes_valid_model]
Model.valid_and_l_cycle [in Rocoma.Recipes_valid_model]
Model.valid_and_intro_l [in Rocoma.Recipes_valid_model]
Model.valid_and_elim [in Rocoma.Recipes_valid_model]
Model.valid_and_intro [in Rocoma.Recipes_valid_model]
Model.valid_consistent [in Rocoma.Recipes_valid_model]
Model.valid_contradiction [in Rocoma.Recipes_valid_model]
Model.valid_top_l2 [in Rocoma.Recipes_valid_model]
Model.valid_top_l1 [in Rocoma.Recipes_valid_model]
Model.valid_top [in Rocoma.Recipes_valid_model]
Model.valid_assumption [in Rocoma.Recipes_valid_model]
N
neuneu [in Rocoma.Recipes_neuneu]neuneug [in Rocoma.Recipes_neuneu]
neuneu2 [in Rocoma.Recipes_neuneu]
neu_joker_top [in Rocoma.Recipes_joker]
neu_joker [in Rocoma.Recipes_joker]
neu_eq_closedh [in Rocoma.Recipes_fv_lemmas]
neu_eq_fvh [in Rocoma.Recipes_fv_lemmas]
neu_eq_closed [in Rocoma.Recipes_fv_lemmas]
neu_eq_fv [in Rocoma.Recipes_fv_lemmas]
neu_eq_same_type [in Rocoma.Recipes_typing]
neu_stack_idempotent [in Rocoma.Recipes_stacks]
neu_stack_lemma [in Rocoma.Recipes_stacks]
neu_fall [in Rocoma.Recipes]
neu_subst_neu [in Rocoma.Recipes]
neu_idempotent [in Rocoma.Recipes]
neu_ren_comm [in Rocoma.Recipes]
neu_upren_comm [in Rocoma.Recipes]
neu_hsubst_comm [in Rocoma.Recipes]
NEU_Neu [in Rocoma.Recipes_neuneu]
NEU_tall [in Rocoma.Recipes_neuneu]
NEU_tlam [in Rocoma.Recipes_neuneu]
NEU_lam [in Rocoma.Recipes_neuneu]
NEU_beta [in Rocoma.Recipes_neuneu]
NEU_and [in Rocoma.Recipes_neuneu]
NEU_expand [in Rocoma.Recipes_neuneu]
O
order_nonneg [in Rocoma.Recipes]order_arg [in Rocoma.Recipes]
P
piΓ_shift [in Rocoma.Recipes_joker]pushup [in Rocoma.Lib.Autosubst_FreeVars]
R
recipe_eq_dec [in Rocoma.Recipes]ren_hsubst [in Rocoma.Lib.Autosubst_FreeVars]
ren_inst [in Rocoma.Recipes_fv_lemmas]
ren_upn_subst [in Rocoma.Recipes_fv_lemmas]
ren_add [in Rocoma.Recipes_fv_lemmas]
ren_upn_ren [in Rocoma.Recipes_fv_lemmas]
S
scompA [in Rocoma.Lib.Autosubst_FreeVars]scons_hcomp [in Rocoma.Recipes_fv_lemmas]
sel_eq [in Rocoma.Coma]
sem_subst [in Rocoma.Recipes_valid_model]
sem_ren [in Rocoma.Recipes_valid_model]
sem_ext [in Rocoma.Recipes_valid_model]
size_terms [in Rocoma.Recipes_joker]
stack_rel_submits [in Rocoma.Recipes_joker]
stack_rel2_jstack [in Rocoma.Recipes_joker]
stack_rel3_meet_stack_rel2_entails [in Rocoma.Recipes_fusion]
stack_rel3_meet_refl [in Rocoma.Recipes_fusion]
stack_has_type_hsubst [in Rocoma.Recipes_stacks]
stack_form [in Rocoma.Recipes_stacks]
stack_rel_entails_refl2 [in Rocoma.Recipes_neuneu]
submits_app [in Rocoma.Recipes_joker]
subSn1 [in Rocoma.Recipes_fv_lemmas]
subst_depth_hit [in Rocoma.Recipes_joker]
subst_depth_var [in Rocoma.Recipes_joker]
subst_var2_miss [in Rocoma.Lib.Autosubst_FreeVars]
subst_var_tsubst_recipe_alt_3 [in Rocoma.Lib.Autosubst_FreeVars]
subst_var_tsubst_recipe_alt_2 [in Rocoma.Lib.Autosubst_FreeVars]
subst_var_tsubst_recipe_alt [in Rocoma.Lib.Autosubst_FreeVars]
subst_var_tsubst_alt [in Rocoma.Lib.Autosubst_FreeVars]
subst_var_tsubst_upn_alt [in Rocoma.Lib.Autosubst_FreeVars]
subst_var_lemma_up1_alt_2 [in Rocoma.Lib.Autosubst_FreeVars]
subst_var_lemma_up1_alt [in Rocoma.Lib.Autosubst_FreeVars]
subst_var_lemma_upn_alt2 [in Rocoma.Lib.Autosubst_FreeVars]
subst_var_lemma_upn_alt [in Rocoma.Lib.Autosubst_FreeVars]
subst_var_hsubst [in Rocoma.Lib.Autosubst_FreeVars]
subst_var_lemma [in Rocoma.Lib.Autosubst_FreeVars]
subst_var_tsubst2 [in Rocoma.Lib.Autosubst_FreeVars]
subst_var_tsubst [in Rocoma.Lib.Autosubst_FreeVars]
subst_var_tsubst_upn [in Rocoma.Lib.Autosubst_FreeVars]
subst_var_id [in Rocoma.Lib.Autosubst_FreeVars]
subst_var_0 [in Rocoma.Lib.Autosubst_FreeVars]
subst_var_miss_2 [in Rocoma.Lib.Autosubst_FreeVars]
subst_var_match [in Rocoma.Lib.Autosubst_FreeVars]
subst_var_miss_1 [in Rocoma.Lib.Autosubst_FreeVars]
subst_var2_up [in Rocoma.Recipes_fv_lemmas]
subst_neu0 [in Rocoma.Recipes]
subst_neu [in Rocoma.Recipes]
subterm_neu_idempotent [in Rocoma.Recipes_directly_box]
subterm_directly_box [in Rocoma.Recipes_directly_box]
subterm_refl [in Rocoma.Recipes_directly_box]
SUB_expand [in Rocoma.Recipes_joker]
sub_cov_hcomp [in Rocoma.Recipes_joker]
sub_cov_up [in Rocoma.Recipes_joker]
sub_cov_box [in Rocoma.Recipes_joker]
surjective_to_stack2 [in Rocoma.Recipes_stacks]
surjective_to_stack [in Rocoma.Recipes_stacks]
T
term_eq_dec [in Rocoma.Recipes]to_stack_appl_cat [in Rocoma.Recipes_stacks]
to_stack_appl [in Rocoma.Recipes_stacks]
to_stack_r [in Rocoma.Recipes_stacks]
to_stack_idempotent2 [in Rocoma.Recipes_stacks]
to_stack_idempotent [in Rocoma.Recipes_stacks]
to_stack_l [in Rocoma.Recipes_stacks]
tsubst_ext_one [in Rocoma.Recipes_typing]
type_eq_dec [in Rocoma.Recipes]
ty_params [in Rocoma.VCgen]
ty_VC [in Rocoma.VCgen]
U
UNEU_beta [in Rocoma.VCgen]UNEU_lam [in Rocoma.VCgen]
UNEU_tlam [in Rocoma.VCgen]
UNEU_app [in Rocoma.VCgen]
UNEU_and [in Rocoma.VCgen]
UNEU_neu [in Rocoma.VCgen]
unfold_box_rel3 [in Rocoma.Recipes_fusion]
unfold_box_rel [in Rocoma.Recipes_box_rel]
unfold_to_stack_2_corr [in Rocoma.Recipes_stacks]
unfold_to_stack_2 [in Rocoma.Recipes_stacks]
uniqueness_eval [in Rocoma.Recipes_eval]
uniqueness_eval_u [in Rocoma.Recipes_eval]
unnaffectedh_jokerT [in Rocoma.Recipes_joker]
unnaffected_jokerT [in Rocoma.Recipes_joker]
upnP [in Rocoma.Lib.Autosubst_FreeVars]
upnP_cond [in Rocoma.Lib.Autosubst_FreeVars]
upn_ren_hsubst [in Rocoma.Lib.Autosubst_FreeVars]
upn_ren_miss [in Rocoma.Lib.Autosubst_FreeVars]
upn_ren_app [in Rocoma.Lib.Autosubst_FreeVars]
upn_k_sigma_x [in Rocoma.Lib.Autosubst_FreeVars]
upn_add [in Rocoma.Recipes_fv_lemmas]
upn_hcomp [in Rocoma.Recipes_fv_lemmas]
upn_T_vs_dec [in Rocoma.Recipes_typing]
upn_miss_var [in Rocoma.Recipes_typing]
upn1 [in Rocoma.Lib.Autosubst_FreeVars]
upn2P [in Rocoma.Lib.Autosubst_FreeVars]
up_compt [in Rocoma.Lib.Autosubst_FreeVars]
up_comp [in Rocoma.Lib.Autosubst_FreeVars]
up_ren [in Rocoma.Lib.Autosubst_FreeVars]
up_ext_one [in Rocoma.Recipes_typing]
V
valid_and_imp3_r [in Rocoma.Recipes_neuneu]valid_and_imp3_l [in Rocoma.Recipes_neuneu]
valid_and_mix_l [in Rocoma.Recipes_neuneu]
valid_and_mix_r [in Rocoma.Recipes_neuneu]
valid_equiv_cut [in Rocoma.Recipes_neuneu]
valid_equiv_sym [in Rocoma.Recipes_neuneu]
valid_imp_imp_split [in Rocoma.Recipes_neuneu]
valid_weak0 [in Rocoma.Recipes_neuneu]
valid_fallF_elim [in Rocoma.Recipes_neuneu]
valid_all_intro [in Rocoma.Recipes_neuneu]
valid_top0 [in Rocoma.Recipes_neuneu]
valid_and_and_intro [in Rocoma.Recipes_neuneu]
valid_assumption_and [in Rocoma.Recipes_neuneu]
valid_and_l_weak2 [in Rocoma.Recipes_neuneu]
valid_and_l_sym [in Rocoma.Recipes_neuneu]
valid_and [in Rocoma.Recipes_neuneu]
valid_dup [in Rocoma.Recipes_neuneu]
valid_exfalso [in Rocoma.Recipes_neuneu]
var_not_free_upn_ge [in Rocoma.Lib.Autosubst_FreeVars]
var_not_free_upn_mid [in Rocoma.Lib.Autosubst_FreeVars]
var_not_free_add [in Rocoma.Lib.Autosubst_FreeVars]
var_not_free_upn_lt [in Rocoma.Lib.Autosubst_FreeVars]
var_not_free_upn_lt_gen [in Rocoma.Recipes_fv_lemmas]
var_not_free_neu [in Rocoma.Recipes_fv_lemmas]
var_not_free_hsubst [in Rocoma.Recipes_fv_lemmas]
var_eq_dec [in Rocoma.Recipes]
vcall_hsubst [in Rocoma.Recipes_joker]
VC_meet [in Rocoma.VCgen]
VC_split [in Rocoma.VCgen]
VC_notnot [in Rocoma.VCgen]
VC_neutral [in Rocoma.VCgen]
VC_ren [in Rocoma.VCgen]
VC_hsubst [in Rocoma.VCgen]
void_stack [in Rocoma.Recipes_stacks]
W
weight_neu [in Rocoma.Recipes]weight_subst_box [in Rocoma.Recipes]
weight_subst_hsubst [in Rocoma.Recipes]
weight_hsubst_subst [in Rocoma.Recipes]
weight_hsubst [in Rocoma.Recipes]
weight_pos [in Rocoma.Recipes]
wt_config2expr [in Rocoma.Coma]
WUEQU_tlam [in Rocoma.VCgen]
WUEQU_and_comm [in Rocoma.VCgen]
WUEQU_app [in Rocoma.VCgen]
_
__has_type_eq_ab_refuted [in Rocoma.Recipes_typing]Constructor Index
A
AC [in Rocoma.Coma]all3_cons_t [in Rocoma.Recipes_fusion]
all3_cons_r [in Rocoma.Recipes_fusion]
all3_nil [in Rocoma.Recipes_fusion]
And [in Rocoma.Recipes]
App [in Rocoma.Recipes]
args_ty_c [in Rocoma.Coma]
args_ty_t [in Rocoma.Coma]
args_ty_nil [in Rocoma.Coma]
arg_tarr [in Rocoma.Recipes]
arg_arr [in Rocoma.Recipes]
arg_here [in Rocoma.Recipes]
Arr [in Rocoma.Recipes]
AT [in Rocoma.Coma]
B
Box [in Rocoma.Recipes]box_rel3_and [in Rocoma.Recipes_fusion]
box_rel3_app [in Rocoma.Recipes_fusion]
box_rel3_zeror [in Rocoma.Recipes_fusion]
box_rel3_zerol [in Rocoma.Recipes_fusion]
box_rel3_zeroz [in Rocoma.Recipes_fusion]
box_rel3_top [in Rocoma.Recipes_fusion]
box_rel3_var [in Rocoma.Recipes_fusion]
box_rel3_tapp [in Rocoma.Recipes_fusion]
box_rel3_lam [in Rocoma.Recipes_fusion]
box_rel3_imp [in Rocoma.Recipes_fusion]
box_rel3_neu [in Rocoma.Recipes_fusion]
box_rel3_tall [in Rocoma.Recipes_fusion]
box_rel3_tlam [in Rocoma.Recipes_fusion]
box_rel3_box [in Rocoma.Recipes_fusion]
box_rel2_and [in Rocoma.Recipes_box_rel]
box_rel2_app [in Rocoma.Recipes_box_rel]
box_rel2_zero [in Rocoma.Recipes_box_rel]
box_rel2_top [in Rocoma.Recipes_box_rel]
box_rel2_var [in Rocoma.Recipes_box_rel]
box_rel2_tapp [in Rocoma.Recipes_box_rel]
box_rel2_lam [in Rocoma.Recipes_box_rel]
box_rel2_imp [in Rocoma.Recipes_box_rel]
box_rel2_neu [in Rocoma.Recipes_box_rel]
box_rel2_tall [in Rocoma.Recipes_box_rel]
box_rel2_tlam [in Rocoma.Recipes_box_rel]
box_rel2_box [in Rocoma.Recipes_box_rel]
box_rel_and [in Rocoma.Recipes_box_rel]
box_rel_app [in Rocoma.Recipes_box_rel]
box_rel_zero [in Rocoma.Recipes_box_rel]
box_rel_top [in Rocoma.Recipes_box_rel]
box_rel_var [in Rocoma.Recipes_box_rel]
box_rel_tapp [in Rocoma.Recipes_box_rel]
box_rel_lam [in Rocoma.Recipes_box_rel]
box_rel_imp [in Rocoma.Recipes_box_rel]
box_rel_neu [in Rocoma.Recipes_box_rel]
box_rel_tall [in Rocoma.Recipes_box_rel]
box_rel_tlam [in Rocoma.Recipes_box_rel]
box_rel_box [in Rocoma.Recipes_box_rel]
C
cabs_c [in Rocoma.Coma]cabs_t [in Rocoma.Coma]
cabs_void [in Rocoma.Coma]
closed_stack_term [in Rocoma.Recipes_stacks]
closed_stack_recipe [in Rocoma.Recipes_stacks]
closed_stack_empty [in Rocoma.Recipes_stacks]
conj_in_r [in Rocoma.Recipes_joker]
conj_in_l [in Rocoma.Recipes_joker]
conj_in_here [in Rocoma.Recipes_joker]
cty_defn [in Rocoma.Coma]
cty_box [in Rocoma.Coma]
cty_parc [in Rocoma.Coma]
cty_part [in Rocoma.Coma]
cty_appc [in Rocoma.Coma]
cty_appt [in Rocoma.Coma]
cty_sym [in Rocoma.Coma]
D
db_tapp3 [in Rocoma.Recipes_directly_box]db_neu3 [in Rocoma.Recipes_directly_box]
db_imp3 [in Rocoma.Recipes_directly_box]
db_tall3 [in Rocoma.Recipes_directly_box]
db_tlam3 [in Rocoma.Recipes_directly_box]
db_appr3 [in Rocoma.Recipes_directly_box]
db_appl3 [in Rocoma.Recipes_directly_box]
db_andr3 [in Rocoma.Recipes_directly_box]
db_andl3 [in Rocoma.Recipes_directly_box]
db_lam3 [in Rocoma.Recipes_directly_box]
db_box3 [in Rocoma.Recipes_directly_box]
db_tapp [in Rocoma.Recipes_directly_box]
db_neu [in Rocoma.Recipes_directly_box]
db_imp [in Rocoma.Recipes_directly_box]
db_tall [in Rocoma.Recipes_directly_box]
db_tlam [in Rocoma.Recipes_directly_box]
db_appr [in Rocoma.Recipes_directly_box]
db_appl [in Rocoma.Recipes_directly_box]
db_andr [in Rocoma.Recipes_directly_box]
db_andl [in Rocoma.Recipes_directly_box]
db_lam [in Rocoma.Recipes_directly_box]
db_box [in Rocoma.Recipes_directly_box]
defs_ty_cons [in Rocoma.Coma]
defs_ty_nil [in Rocoma.Coma]
E
EApp [in Rocoma.Coma]EBar [in Rocoma.Coma]
EDef [in Rocoma.Coma]
ELam [in Rocoma.Coma]
ETApp [in Rocoma.Coma]
ETLam [in Rocoma.Coma]
eval_tapp [in Rocoma.Recipes_eval]
eval_app [in Rocoma.Recipes_eval]
eval_lam [in Rocoma.Recipes_eval]
eval_tall [in Rocoma.Recipes_eval]
eval_tlam [in Rocoma.Recipes_eval]
eval_neu [in Rocoma.Recipes_eval]
eval_box [in Rocoma.Recipes_eval]
eval_and [in Rocoma.Recipes_eval]
eval_imp [in Rocoma.Recipes_eval]
eval_top [in Rocoma.Recipes_eval]
eval_zero [in Rocoma.Recipes_eval]
EVar [in Rocoma.Coma]
F
FAll [in Rocoma.Recipes]FAnd [in Rocoma.Recipes]
FBot [in Rocoma.Recipes]
FEqu [in Rocoma.Recipes]
FImp [in Rocoma.Recipes]
FNot [in Rocoma.Recipes]
FTop [in Rocoma.Recipes]
fus_tapp [in Rocoma.Recipes_fusion]
fus_app [in Rocoma.Recipes_fusion]
fus_lam [in Rocoma.Recipes_fusion]
fus_tall [in Rocoma.Recipes_fusion]
fus_tlam [in Rocoma.Recipes_fusion]
fus_neu [in Rocoma.Recipes_fusion]
fus_box [in Rocoma.Recipes_fusion]
fus_and [in Rocoma.Recipes_fusion]
fus_imp [in Rocoma.Recipes_fusion]
fus_zero2 [in Rocoma.Recipes_fusion]
fus_zero1 [in Rocoma.Recipes_fusion]
fus_zero [in Rocoma.Recipes_fusion]
fus_top [in Rocoma.Recipes_fusion]
fus_var [in Rocoma.Recipes_fusion]
H
Hide [in Rocoma.Coma]I
Imp [in Rocoma.Recipes]L
Lam [in Rocoma.Recipes]ltac_mark [in Rocoma.Lib.My_tactics]
N
Neu [in Rocoma.Recipes]R
R [in Rocoma.Recipes_stacks]S
Show [in Rocoma.Coma]stack_rel3_recipe [in Rocoma.Recipes_fusion]
stack_rel3_term [in Rocoma.Recipes_fusion]
stack_rel3_nil [in Rocoma.Recipes_fusion]
stack_rel2_recipe [in Rocoma.Recipes_logrel]
stack_rel2_term [in Rocoma.Recipes_logrel]
stack_rel2_nil [in Rocoma.Recipes_logrel]
stack_rel_recipe [in Rocoma.Recipes_logrel]
stack_rel_term [in Rocoma.Recipes_logrel]
stack_rel_nil [in Rocoma.Recipes_logrel]
stack_has_type_recipe [in Rocoma.Recipes_stacks]
stack_has_type_term [in Rocoma.Recipes_stacks]
stack_has_type_void [in Rocoma.Recipes_stacks]
steps_step [in Rocoma.Coma]
steps_refl [in Rocoma.Coma]
step_if_false [in Rocoma.Coma]
step_if_true [in Rocoma.Coma]
step_box [in Rocoma.Coma]
step_appc [in Rocoma.Coma]
step_appt [in Rocoma.Coma]
step_sym [in Rocoma.Coma]
step_defn [in Rocoma.Coma]
step_app [in Rocoma.Coma]
step_tapp [in Rocoma.Coma]
T
T [in Rocoma.Recipes_stacks]TAll [in Rocoma.Recipes]
TApp [in Rocoma.Recipes]
TArr [in Rocoma.Recipes]
TCons [in Rocoma.Recipes]
TLam [in Rocoma.Recipes]
TNat [in Rocoma.Recipes]
Top [in Rocoma.Recipes]
TVar [in Rocoma.Recipes]
ty_neu [in Rocoma.Recipes_typing]
ty_box [in Rocoma.Recipes_typing]
ty_tall [in Rocoma.Recipes_typing]
ty_tlam [in Rocoma.Recipes_typing]
ty_lam [in Rocoma.Recipes_typing]
ty_tapp [in Rocoma.Recipes_typing]
ty_app [in Rocoma.Recipes_typing]
ty_and [in Rocoma.Recipes_typing]
ty_imp [in Rocoma.Recipes_typing]
ty_top [in Rocoma.Recipes_typing]
ty_zero [in Rocoma.Recipes_typing]
ty_var [in Rocoma.Recipes_typing]
V
Var [in Rocoma.Recipes]VCons [in Rocoma.Recipes_valid_model]
VNat [in Rocoma.Recipes_valid_model]
Void [in Rocoma.Recipes]
VProp [in Rocoma.Recipes_valid_model]
Z
Zero [in Rocoma.Recipes]Axiom Index
V
VALID.valid [in Rocoma.Recipes_valid_sig]VALID.valid_all_elim [in Rocoma.Recipes_valid_sig]
VALID.valid_all_de_bruijn [in Rocoma.Recipes_valid_sig]
VALID.valid_all_and [in Rocoma.Recipes_valid_sig]
VALID.valid_all_mono [in Rocoma.Recipes_valid_sig]
VALID.valid_cut [in Rocoma.Recipes_valid_sig]
VALID.valid_contr [in Rocoma.Recipes_valid_sig]
VALID.valid_weak [in Rocoma.Recipes_valid_sig]
VALID.valid_imp_elim [in Rocoma.Recipes_valid_sig]
VALID.valid_imp_intro [in Rocoma.Recipes_valid_sig]
VALID.valid_and_l_cycle [in Rocoma.Recipes_valid_sig]
VALID.valid_and_intro_l [in Rocoma.Recipes_valid_sig]
VALID.valid_and_elim [in Rocoma.Recipes_valid_sig]
VALID.valid_and_intro [in Rocoma.Recipes_valid_sig]
VALID.valid_consistent [in Rocoma.Recipes_valid_sig]
VALID.valid_contradiction [in Rocoma.Recipes_valid_sig]
VALID.valid_top_l2 [in Rocoma.Recipes_valid_sig]
VALID.valid_top_l1 [in Rocoma.Recipes_valid_sig]
VALID.valid_top [in Rocoma.Recipes_valid_sig]
VALID.valid_assumption [in Rocoma.Recipes_valid_sig]
Inductive Index
A
all3 [in Rocoma.Recipes_fusion]arg [in Rocoma.Coma]
args_ty [in Rocoma.Coma]
arg_of [in Rocoma.Recipes]
B
barrier [in Rocoma.Coma]box_rel3 [in Rocoma.Recipes_fusion]
box_rel2 [in Rocoma.Recipes_box_rel]
box_rel [in Rocoma.Recipes_box_rel]
C
cabs [in Rocoma.Coma]closed_stack [in Rocoma.Recipes_stacks]
conj_in [in Rocoma.Recipes_joker]
cty [in Rocoma.Coma]
D
db [in Rocoma.Recipes_directly_box]db3 [in Rocoma.Recipes_directly_box]
defs_ty [in Rocoma.Coma]
E
eval [in Rocoma.Recipes_eval]expr [in Rocoma.Coma]
F
fusion [in Rocoma.Recipes_fusion]H
has_type [in Rocoma.Recipes_typing]L
ltac_Mark [in Rocoma.Lib.My_tactics]R
recipe [in Rocoma.Recipes]S
stack_rel3 [in Rocoma.Recipes_fusion]stack_rel2 [in Rocoma.Recipes_logrel]
stack_rel [in Rocoma.Recipes_logrel]
stack_has_type [in Rocoma.Recipes_stacks]
stack_item [in Rocoma.Recipes_stacks]
step [in Rocoma.Coma]
steps [in Rocoma.Coma]
T
term [in Rocoma.Recipes]type [in Rocoma.Recipes]
V
val [in Rocoma.Recipes_valid_model]Projection Index
D
dbar [in Rocoma.Coma]dbody [in Rocoma.Coma]
dty [in Rocoma.Coma]
I
ids_inj [in Rocoma.Lib.Autosubst_FreeVars]Section Index
B
Both [in Rocoma.Lib.Autosubst_FreeVars]E
Eval [in Rocoma.Recipes_eval]Evalf [in Rocoma.Recipes_evalf]
F
FreeVars [in Rocoma.Lib.Autosubst_FreeVars]M
MMapInstances [in Rocoma.Autosubst.AutosubstSsr]O
OpSem [in Rocoma.Coma]S
Sem [in Rocoma.Recipes_fusion]Sem [in Rocoma.Recipes_neuneu]
subst_var2p [in Rocoma.Lib.Autosubst_FreeVars]
subst_var2 [in Rocoma.Lib.Autosubst_FreeVars]
Subst_var [in Rocoma.Lib.Autosubst_FreeVars]
T
Test [in Rocoma.Recipes_joker]Instance Index
H
HSubstLemmas_term_expr [in Rocoma.Coma]HSubstLemmas_term_recipe [in Rocoma.Recipes]
HSubst_term_expr [in Rocoma.Coma]
HSubst_term_recipe [in Rocoma.Recipes]
I
IdsLemmas_T [in Rocoma.Recipes]IdsLemmas_R [in Rocoma.Recipes]
Ids_expr [in Rocoma.Coma]
Ids_recipe [in Rocoma.Recipes]
Ids_term [in Rocoma.Recipes]
M
MMapExt_fun [in Rocoma.Autosubst.AutosubstSsr]mmapExt_seq [in Rocoma.Autosubst.AutosubstSsr]
MMapExt_pair [in Rocoma.Autosubst.AutosubstSsr]
MMapExt_option [in Rocoma.Autosubst.AutosubstSsr]
MMapLemmas_fun [in Rocoma.Autosubst.AutosubstSsr]
mmapLemmas_seq [in Rocoma.Autosubst.AutosubstSsr]
MMapLemmas_pair [in Rocoma.Autosubst.AutosubstSsr]
MMapLemmas_option [in Rocoma.Autosubst.AutosubstSsr]
MMap_fun [in Rocoma.Autosubst.AutosubstSsr]
mmap_seq [in Rocoma.Autosubst.AutosubstSsr]
MMap_pair [in Rocoma.Autosubst.AutosubstSsr]
MMap_option [in Rocoma.Autosubst.AutosubstSsr]
R
Rename_expr [in Rocoma.Coma]Rename_recipe [in Rocoma.Recipes]
Rename_term [in Rocoma.Recipes]
S
SubstHSubstComp_term_expr [in Rocoma.Coma]SubstHSubstComp_term_recipe [in Rocoma.Recipes]
SubstLemmas_expr [in Rocoma.Coma]
SubstLemmas_recipe [in Rocoma.Recipes]
SubstLemmas_term [in Rocoma.Recipes]
Subst_expr [in Rocoma.Coma]
Subst_recipe [in Rocoma.Recipes]
Subst_term [in Rocoma.Recipes]
Definition Index
A
aligned [in Rocoma.Recipes_logrel]allzbb [in Rocoma.Recipes_neuneu]
all_params [in Rocoma.VCgen]
all3_sind [in Rocoma.Recipes_fusion]
all3_ind [in Rocoma.Recipes_fusion]
appl [in Rocoma.Recipes_stacks]
args [in Rocoma.Coma]
args_ty_sind [in Rocoma.Coma]
args_ty_ind [in Rocoma.Coma]
arg_ren [in Rocoma.Coma]
arg_sind [in Rocoma.Coma]
arg_rec [in Rocoma.Coma]
arg_ind [in Rocoma.Coma]
arg_rect [in Rocoma.Coma]
arg_of_sind [in Rocoma.Recipes]
arg_of_ind [in Rocoma.Recipes]
B
barrier_sind [in Rocoma.Coma]barrier_rec [in Rocoma.Coma]
barrier_ind [in Rocoma.Coma]
barrier_rect [in Rocoma.Coma]
box_rel3_sind [in Rocoma.Recipes_fusion]
box_rel3_ind [in Rocoma.Recipes_fusion]
box_rel2_sind [in Rocoma.Recipes_box_rel]
box_rel2_ind [in Rocoma.Recipes_box_rel]
box_rel_sind [in Rocoma.Recipes_box_rel]
box_rel_ind [in Rocoma.Recipes_box_rel]
C
cabs_mut [in Rocoma.Coma]cabs_sind [in Rocoma.Coma]
cabs_ind [in Rocoma.Coma]
closed [in Rocoma.Lib.Autosubst_FreeVars]
closedh [in Rocoma.Lib.Autosubst_FreeVars]
closed_stack_sind [in Rocoma.Recipes_stacks]
closed_stack_ind [in Rocoma.Recipes_stacks]
closing [in Rocoma.VCgen]
complete [in Rocoma.Recipes_typing]
config [in Rocoma.Coma]
config2expr [in Rocoma.Coma]
conj_in_sind [in Rocoma.Recipes_joker]
conj_in_ind [in Rocoma.Recipes_joker]
covers [in Rocoma.Recipes_joker]
covers_stack [in Rocoma.Recipes_joker]
covers_app [in Rocoma.Recipes_joker]
covers_below [in Rocoma.Recipes_joker]
ctx [in Rocoma.Recipes_typing]
ctx_insertion [in Rocoma.Recipes_typing]
ctx_defs [in Rocoma.Coma]
ctx_ext [in Rocoma.Recipes_directly_box]
cty_mut [in Rocoma.Coma]
cty_sind [in Rocoma.Coma]
cty_ind [in Rocoma.Coma]
c_len [in Rocoma.Recipes_joker]
D
db_sind [in Rocoma.Recipes_directly_box]db_ind [in Rocoma.Recipes_directly_box]
db3_sind [in Rocoma.Recipes_directly_box]
db3_ind [in Rocoma.Recipes_directly_box]
defs [in Rocoma.Coma]
defs_ty_sind [in Rocoma.Coma]
defs_ty_ind [in Rocoma.Coma]
depth [in Rocoma.Recipes]
directly_box [in Rocoma.Recipes_directly_box]
E
eappl [in Rocoma.Coma]edefs [in Rocoma.Coma]
empty_ctx [in Rocoma.Recipes_typing]
ENT [in Rocoma.Recipes_neuneu]
entails [in Rocoma.Recipes_neuneu]
EQU [in Rocoma.Recipes_fusion]
equivalent [in Rocoma.Recipes_fusion]
eta [in Rocoma.Coma]
evalf [in Rocoma.Recipes_evalf]
eval_sind [in Rocoma.Recipes_eval]
eval_ind [in Rocoma.Recipes_eval]
expr_sind [in Rocoma.Coma]
expr_rec [in Rocoma.Coma]
expr_ind [in Rocoma.Coma]
expr_rect [in Rocoma.Coma]
F
fail [in Rocoma.Coma]failed [in Rocoma.Coma]
fall [in Rocoma.Recipes]
fallF [in Rocoma.Recipes]
fusion_sind [in Rocoma.Recipes_fusion]
fusion_ind [in Rocoma.Recipes_fusion]
fv [in Rocoma.Lib.Autosubst_FreeVars]
fvh [in Rocoma.Lib.Autosubst_FreeVars]
fvu [in Rocoma.Lib.Autosubst_FreeVars]
fvu2 [in Rocoma.Lib.Autosubst_FreeVars]
fv_plage [in Rocoma.Recipes_typing]
H
halt [in Rocoma.Coma]halted [in Rocoma.Coma]
has_type_sind [in Rocoma.Recipes_typing]
has_type_ind [in Rocoma.Recipes_typing]
I
if_ [in Rocoma.Coma]inst [in Rocoma.Recipes_fv_lemmas]
J
joker [in Rocoma.Recipes_joker]jokerT [in Rocoma.Recipes_joker]
joker_inst [in Rocoma.Recipes_joker]
joker_all [in Rocoma.Recipes_joker]
joker_abs [in Rocoma.Recipes_joker]
jstack [in Rocoma.Recipes_joker]
L
lam_params [in Rocoma.VCgen]logrel [in Rocoma.Recipes_logrel]
logrel2 [in Rocoma.Recipes_logrel]
logrel3 [in Rocoma.Recipes_fusion]
ltac_Mark_sind [in Rocoma.Lib.My_tactics]
ltac_Mark_rec [in Rocoma.Lib.My_tactics]
ltac_Mark_ind [in Rocoma.Lib.My_tactics]
ltac_Mark_rect [in Rocoma.Lib.My_tactics]
M
MEET [in Rocoma.Recipes_fusion]meet [in Rocoma.Recipes_fusion]
mem_ren [in Rocoma.Recipes_joker]
mem_box [in Rocoma.Recipes_directly_box]
model [in Rocoma.Main]
Model.valid [in Rocoma.Recipes_valid_model]
N
neu [in Rocoma.Recipes]NEU [in Rocoma.Recipes_neuneu]
neutral [in Rocoma.Recipes_neuneu]
neu_stack [in Rocoma.Recipes_stacks]
O
olookup [in Rocoma.Coma]order [in Rocoma.Recipes]
P
piΓ [in Rocoma.Recipes_joker]R
rall [in Rocoma.VCgen]recipe_sind [in Rocoma.Recipes]
recipe_rec [in Rocoma.Recipes]
recipe_ind [in Rocoma.Recipes]
recipe_rect [in Rocoma.Recipes]
ren_dec [in Rocoma.Recipes_typing]
results [in Rocoma.Main]
rlet [in Rocoma.VCgen]
S
sel [in Rocoma.Coma]sem [in Rocoma.Recipes_valid_model]
stack [in Rocoma.Recipes_stacks]
stack_rel3_sind [in Rocoma.Recipes_fusion]
stack_rel3_ind [in Rocoma.Recipes_fusion]
stack_rel2_sind [in Rocoma.Recipes_logrel]
stack_rel2_ind [in Rocoma.Recipes_logrel]
stack_rel_sind [in Rocoma.Recipes_logrel]
stack_rel_ind [in Rocoma.Recipes_logrel]
stack_hsubst [in Rocoma.Recipes_stacks]
stack_has_type_sind [in Rocoma.Recipes_stacks]
stack_has_type_ind [in Rocoma.Recipes_stacks]
stack_item_sind [in Rocoma.Recipes_stacks]
stack_item_rec [in Rocoma.Recipes_stacks]
stack_item_ind [in Rocoma.Recipes_stacks]
stack_item_rect [in Rocoma.Recipes_stacks]
steps_sind [in Rocoma.Coma]
steps_ind [in Rocoma.Coma]
step_sind [in Rocoma.Coma]
step_ind [in Rocoma.Coma]
strongly [in Rocoma.Recipes]
strongly2 [in Rocoma.Recipes]
strongly3 [in Rocoma.Recipes_fusion]
SUB [in Rocoma.Recipes_joker]
submits [in Rocoma.Recipes_joker]
subst_depth [in Rocoma.Recipes_joker]
subst_var2 [in Rocoma.Lib.Autosubst_FreeVars]
subst_var [in Rocoma.Lib.Autosubst_FreeVars]
subterm [in Rocoma.Recipes_directly_box]
sub_cov [in Rocoma.Recipes_joker]
T
terms [in Rocoma.Recipes_joker]term_sind [in Rocoma.Recipes]
term_rec [in Rocoma.Recipes]
term_ind [in Rocoma.Recipes]
term_rect [in Rocoma.Recipes]
to_stack [in Rocoma.Recipes_stacks]
to_stack_rec [in Rocoma.Recipes_stacks]
TRAC [in Rocoma.Recipes_eval]
tractable [in Rocoma.Recipes_eval]
truth [in Rocoma.Recipes_valid_model]
type_sind [in Rocoma.Recipes]
type_rec [in Rocoma.Recipes]
type_ind [in Rocoma.Recipes]
type_rect [in Rocoma.Recipes]
t_len [in Rocoma.Recipes_joker]
U
Udiv [in Rocoma.Recipes_joker]UEQU [in Rocoma.VCgen]
UMEET [in Rocoma.VCgen]
UNEU [in Rocoma.VCgen]
uniformly [in Rocoma.VCgen]
uniformly2 [in Rocoma.VCgen]
uniformly3 [in Rocoma.VCgen]
V
val_sind [in Rocoma.Recipes_valid_model]val_rec [in Rocoma.Recipes_valid_model]
val_ind [in Rocoma.Recipes_valid_model]
val_rect [in Rocoma.Recipes_valid_model]
var_not_free [in Rocoma.Lib.Autosubst_FreeVars]
VC [in Rocoma.VCgen]
vcall [in Rocoma.Recipes_joker]
W
weakly [in Rocoma.Recipes]weakly_uniform2 [in Rocoma.VCgen]
weakly2 [in Rocoma.Recipes]
weight [in Rocoma.Recipes]
wf_config [in Rocoma.Coma]
WUEQU [in Rocoma.VCgen]
Record Index
D
def [in Rocoma.Coma]I
IdsLemmas [in Rocoma.Lib.Autosubst_FreeVars]| 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 | (1157 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 | (22 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 | (3 entries) |
| Variable 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 | (67 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 | (21 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 | (562 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 | (189 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 | (20 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 | (31 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (32 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 | (192 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |