| 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 | (1255 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 | (51 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| 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 | (13 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 | (24 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 | (736 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 | (52 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 | (28 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 | (27 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) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (18 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 | (290 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
Abcase [definition, in AlphaEqProps]abindersDeep [definition, in SubstAuxAlphaEq]
Abstraction [inductive, in AlphaEquality]
aCons [constructor, in LetrecEx]
addl [definition, in list]
alAbP [constructor, in AlphaEquality]
alAbT [constructor, in AlphaEquality]
albindersDeep [definition, in SubstAuxAlphaEq]
albndDeepMakeAbPSubset [lemma, in SubstAuxAlphaEq]
albndDeepMakeAbTSubset [lemma, in SubstAuxAlphaEq]
ALDom [definition, in AssociationList]
ALDomCombine [lemma, in AssociationList]
ALDomFilterCommute [lemma, in AssociationList]
alembed [constructor, in AlphaEquality]
ALEndoMapFilterCommute [lemma, in AssociationList]
ALFilter [definition, in AssociationList]
ALFilterAppAsDiff [lemma, in AssociationList]
ALFilterAppR [lemma, in AssociationList]
ALFilterAppSub [lemma, in AssociationList]
ALFilterDom [lemma, in AssociationList]
ALFilterLIn [lemma, in AssociationList]
ALFilterSubset [lemma, in AssociationList]
ALFilterSwap [lemma, in AssociationList]
ALFilter_nil_r [lemma, in AssociationList]
ALFind [definition, in AssociationList]
ALFindApp [lemma, in AssociationList]
ALFindDef [definition, in AssociationList]
ALFindDef2 [definition, in AssociationList]
ALFindDef2Same [lemma, in AssociationList]
ALFindEndoMapSome [lemma, in AssociationList]
ALFindFilterNone [lemma, in AssociationList]
ALFindFilterSome [lemma, in AssociationList]
ALFindMapNone [lemma, in AssociationList]
ALFindMapSome [lemma, in AssociationList]
ALFindNone [lemma, in AssociationList]
ALFindNoneKeepFirstSingleton [lemma, in AssociationList]
ALFindRangeMapNone [lemma, in AssociationList]
ALFindRangeMapSome [lemma, in AssociationList]
ALFindSome [lemma, in AssociationList]
ALFindSomeKeepFirstSingleton [lemma, in AssociationList]
ALFind2 [lemma, in AssociationList]
ALInEta [lemma, in AssociationList]
ALKeepFirst [definition, in AssociationList]
ALKeepFirstAppLin [lemma, in AssociationList]
ALKeepFirstFilterDiff [lemma, in AssociationList]
ALKeepFirstLin [lemma, in AssociationList]
ALKeepFirstLinApp [lemma, in AssociationList]
ALKeepFirstNil [lemma, in AssociationList]
ALKeepFirstSubst [lemma, in AssociationList]
allBndngVars [definition, in Term]
AllButBindersSubset [lemma, in Term]
AllVarsEquivariant [lemma, in SwapProps]
allVarsSub [definition, in SubstAuxAlphaEq]
ALMap [definition, in AssociationList]
ALMapFilterCommute [lemma, in AssociationList]
ALMapRange [definition, in AssociationList]
ALMapRangeFilterCommute [lemma, in AssociationList]
ALMapRangeFindCommute [lemma, in AssociationList]
alnode [constructor, in AlphaEquality]
ALpcase [definition, in AlphaEqProps]
AlphaDecider [library]
AlphaEqAbs [inductive, in AlphaEquality]
alphaEqAbsMut [definition, in AlphaEquality]
AlphaEqAbsPSameParam [lemma, in AlphaEqProps]
AlphaEqAbsTSameParam [lemma, in AlphaEqProps]
alphaEqAlphaSubst [lemma, in SubstAuxAlphaEq]
alphaEqDecidable [lemma, in AlphaDecider]
AlphaEqNilAbsP [lemma, in AlphaEqProps]
AlphaEqNilAbsT [lemma, in AlphaEqProps]
AlphaEqProps [library]
alphaEqRefl [lemma, in AlphaEqProps]
AlphaEqSubst [definition, in SubstAuxAlphaEq]
AlphaEqSubstApp [lemma, in SubstAuxAlphaEq]
AlphaEqSubstRefl [lemma, in SubstAuxAlphaEq]
alphaEqSwapNonFree [lemma, in AlphaEqProps]
alphaEqSym [lemma, in AlphaEqProps]
alphaEqTransitive [lemma, in AlphaEqProps]
AlphaEquality [library]
alphaEquiVariant [lemma, in AlphaEqProps]
AlphaProps [section, in AlphaEqProps]
AlphaRen [library]
alpha_preserves_free_vars [lemma, in AlphaEqProps]
alpnode [constructor, in AlphaEquality]
alpt [constructor, in AlphaEquality]
alpvar [constructor, in AlphaEquality]
ALRange [definition, in AssociationList]
ALRangeCombine [lemma, in AssociationList]
ALRangeRel [definition, in AssociationList]
ALRangeRelApp [lemma, in AssociationList]
ALRangeRelFilter [lemma, in AssociationList]
ALRangeRelFind [lemma, in AssociationList]
ALRangeRelRefl [lemma, in AssociationList]
ALRangeRelSameDom [lemma, in AssociationList]
alSSubstAux [definition, in SubstAuxAlphaEq]
alSSubstAux_MakeAbstractionsPNode [lemma, in SubstAuxAlphaEq]
alSSubstAux_MakeAbstractionsTNode [lemma, in SubstAuxAlphaEq]
ALSwitch [definition, in AssociationList]
ALSwitchCombine [lemma, in AssociationList]
alt [constructor, in AlphaEquality]
ALtcase [definition, in AlphaEqProps]
alv [constructor, in AlphaEquality]
andb_eq_true [lemma, in UsefulTypes]
andb_true [lemma, in UsefulTypes]
and_true_r [lemma, in UsefulTypes]
and_true_l [lemma, in UsefulTypes]
and_tiff_compat_l [lemma, in UsefulTypes]
aNil [constructor, in LetrecEx]
app [constructor, in LetrecEx]
appl [definition, in list]
apply_eq [lemma, in UsefulTypes]
app_if [lemma, in list]
app_eq_nil_iff [lemma, in list]
app_split [lemma, in list]
app_subset [lemma, in list]
asgn [constructor, in LetrecEx]
asgnP [constructor, in LetrecEx]
asgnRhs [constructor, in LetrecEx]
asgnRhsE [constructor, in LetrecEx]
assert [definition, in UsefulTypes]
assert_memvar_false [lemma, in variables]
assert_sub_vars [lemma, in variables]
assert_eq_vars [lemma, in variables]
assert_memvar [lemma, in variables]
assert_of_andb [lemma, in UsefulTypes]
assert_andb [lemma, in UsefulTypes]
assert_orb [lemma, in UsefulTypes]
assert_memberb [lemma, in list]
assert_beq_list [lemma, in list]
assert_eqsetb [lemma, in list]
assert_subsetb [lemma, in list]
assert_nullb [lemma, in list]
AssociationList [section, in AssociationList]
AssociationList [library]
AssociationList.DeqKey [variable, in AssociationList]
AssociationList.Key [variable, in AssociationList]
AssociationList.Value [variable, in AssociationList]
AssocList [definition, in AssociationList]
aSSubstAux [definition, in SubstAuxAlphaEq]
AvRenaming [definition, in AlphaRen]
AvRenamingSubset [lemma, in AlphaRen]
B
ball [definition, in list]ball_map_true [lemma, in list]
ball_true [lemma, in list]
beq_var_sym [lemma, in variables]
beq_var_false [lemma, in variables]
beq_var_false_not_eq [lemma, in variables]
beq_var_true [lemma, in variables]
beq_var_eq [lemma, in variables]
beq_var_refl [lemma, in variables]
beq_var [definition, in variables]
beq_nat_sym [lemma, in UsefulTypes]
beq_list_refl [lemma, in list]
beq_list [definition, in list]
betterAbsPElim [lemma, in AlphaEqProps]
betterAbsTElim [lemma, in AlphaEqProps]
bijection [definition, in UsefulTypes]
bindCount [definition, in CFGV]
bindersAllvarsSubset [lemma, in Term]
bindersDeep_in_allvars [lemma, in Term]
bindersSSubstAuxNoCnange [lemma, in SubstAux]
bindersSubsetDeep [lemma, in Term]
bindingInfo [definition, in LetrecEx]
bindingInfo [projection, in CFGV]
bindingInfoCorrect [projection, in CFGV]
bindingSourcesNth [definition, in CFGV]
binrel_list_cons [lemma, in list]
binrel_list_nil [lemma, in list]
binrel_list [definition, in list]
bin_rel_and [definition, in bin_rels]
bin_rel [definition, in bin_rels]
bin_rel_list_refl [lemma, in list]
bin_rels [library]
bndngPatIndices [definition, in CFGV]
bndngPatIndicesValid [lemma, in CFGV]
bndngPatIndicesValid2 [lemma, in CFGV]
bndngVarsDeepEquivariant [lemma, in SwapProps]
bool2_Equi [lemma, in UsefulTypes]
boxer [constructor, in LibTactics]
Boxer [inductive, in LibTactics]
bsNthValid [lemma, in CFGV]
C
cast [constructor, in eq_rel]Cast [inductive, in eq_rel]
cast2 [constructor, in eq_rel]
Cast2 [inductive, in eq_rel]
CFGV [record, in CFGV]
CFGV [library]
change_bvars_rangewspec [lemma, in SSubst]
change_bvars_range_spec [lemma, in SSubst]
change_bvars_range [definition, in SSubst]
combine_t_iff_proofs_not [lemma, in eq_rel]
combine_t_iff_proofs_sum [lemma, in eq_rel]
combine_t_iff_proofs_prod [lemma, in eq_rel]
combine_t_iff_proofs_t_iff [lemma, in eq_rel]
combine_t_iff_proofs_imp [lemma, in eq_rel]
combine_cons [lemma, in list]
combine_eq [lemma, in list]
combine_in_right [lemma, in list]
combine_app_app [lemma, in list]
combine_nil [lemma, in list]
combine_app_eq [lemma, in list]
combine_in_left2 [lemma, in list]
combine_in_left [lemma, in list]
comp_ind_type [lemma, in UsefulTypes]
comp_ind [lemma, in UsefulTypes]
constantFn [definition, in UsefulTypes]
constantMapEq [lemma, in UsefulTypes]
cons_inj [lemma, in list]
cons_snoc [lemma, in list]
cons_app [lemma, in list]
cons_eq [lemma, in list]
cons_as_app [lemma, in list]
cons_subset [lemma, in list]
Csurjection [definition, in UsefulTypes]
CType_S [lemma, in eq_rel]
c_t_iff [definition, in eq_rel]
D
decDisjointV [definition, in CFGV]decidable [definition, in UsefulTypes]
decidable_prod [lemma, in UsefulTypes]
decideAbsP [lemma, in AlphaDecider]
decideAbsT [lemma, in AlphaDecider]
dec_disjointv [definition, in variables]
dec_disjoint [lemma, in list]
dep_pair_eq [lemma, in UsefulTypes]
Deq [definition, in UsefulTypes]
DeqBool [definition, in UsefulTypes]
DeqDeqp [lemma, in UsefulTypes]
deqEm [projection, in CFGV]
deqGSym [lemma, in CFGV]
deqMixP [lemma, in CFGV]
deqNT [projection, in CFGV]
DeqP [definition, in UsefulTypes]
deqPPr [projection, in CFGV]
deqPr [projection, in CFGV]
deqPT [projection, in CFGV]
deqSigTSemType [lemma, in CFGV]
deqSigVType [lemma, in CFGV]
DeqSym [lemma, in UsefulTypes]
deqT [projection, in CFGV]
DeqTrue [lemma, in UsefulTypes]
deqTSem [projection, in CFGV]
DeqVarSym [projection, in CFGV]
DeqVtype [lemma, in CFGV]
deq_nvar [lemma, in variables]
deq_nat [abbreviation, in UsefulTypes]
deq_prod [lemma, in UsefulTypes]
deq_list [lemma, in list]
Deq2Bool [definition, in UsefulTypes]
diff [definition, in list]
diffEmbedNode [definition, in AlphaDecider]
diffPProdsNode [definition, in AlphaDecider]
diffPVarClasses [definition, in AlphaDecider]
diffSameNil [lemma, in list]
diffTProdsNode [definition, in AlphaDecider]
diffVarClasses [definition, in AlphaDecider]
diff_cons_r_ni [lemma, in list]
diff_cons_r [lemma, in list]
diff_dup2 [lemma, in list]
diff_dup [lemma, in list]
diff_move [lemma, in list]
diff_repeat [lemma, in list]
diff_app_l [lemma, in list]
diff_app_r [lemma, in list]
diff_comm [lemma, in list]
diff_remove [lemma, in list]
diff_nil [lemma, in list]
disjoint [definition, in list]
disjointDeepShallowPlusAlready [lemma, in Term]
DisjointEquivariant [lemma, in SwapProps]
DisjointEquivariantRev [lemma, in SwapProps]
disjointSwapLVar [lemma, in SwapProps]
disjoint_remove_nvars2 [lemma, in variables]
disjoint_remove_nvars [lemma, in variables]
disjoint_remove_nvars_l [lemma, in variables]
disjoint_flatten_tl [lemma, in SubstAux]
disjoint_app_lr [lemma, in list]
disjoint_diff_l [lemma, in list]
disjoint_remove_l [lemma, in list]
disjoint_flat_map_r [lemma, in list]
disjoint_flat_map_l [lemma, in list]
disjoint_app_r [lemma, in list]
disjoint_app_l [lemma, in list]
disjoint_singleton_r [lemma, in list]
disjoint_singleton_l [lemma, in list]
disjoint_snoc_l [lemma, in list]
disjoint_snoc_r [lemma, in list]
disjoint_iff_diff [lemma, in list]
disjoint_cons_l [lemma, in list]
disjoint_cons_r [lemma, in list]
disjoint_sym [lemma, in list]
disjoint_sym_impl [lemma, in list]
disjoint_nil_l_iff [lemma, in list]
disjoint_nil_l [lemma, in list]
disjoint_nil_r_iff [lemma, in list]
disjoint_nil_r [lemma, in list]
dmemvar [lemma, in variables]
Dom [abbreviation, in SSubst]
dont_touch_forall3 [lemma, in eq_rel]
dont_touch_forall2 [lemma, in eq_rel]
dont_touch_forall [lemma, in eq_rel]
dup_lemma [lemma, in LibTactics]
E
embed [constructor, in Term]EmbedProd [inductive, in LetrecEx]
EmbedProd [projection, in CFGV]
epLhs [definition, in CFGV]
epLhsRhs [definition, in LetrecEx]
epLhsRhs [projection, in CFGV]
epRhs [definition, in CFGV]
eqdec [projection, in GVariables]
eqset [definition, in list]
eqsetb [definition, in list]
eqsetCommute [lemma, in list]
eqsetCommute3 [lemma, in list]
eqSetDeepShallowPlusAlready [lemma, in Term]
eqsetSubset [lemma, in list]
eqset_subtractv_if_right [lemma, in AlphaEqProps]
eqset_subtractv_if_left [lemma, in AlphaEqProps]
eqset_sym [lemma, in list]
eqset_trans [lemma, in list]
eqset_diff_if_right [lemma, in list]
eqset_diff_if_left [lemma, in list]
eqset_app_if [lemma, in list]
eqset_same [lemma, in list]
eqset2 [definition, in list]
equipollent [definition, in UsefulTypes]
equipollent_Deq [lemma, in UsefulTypes]
EquiVariantFn [definition, in Swap]
EquiVariantFn2 [definition, in Swap]
EquiVariantFn3 [definition, in Swap]
EquiVariantRel [definition, in Swap]
EquiVariantRelSame [definition, in Swap]
EquiVariantRelUn [definition, in Swap]
EquivariantSSubstAux [lemma, in SubstAuxAlphaEq]
eqvars [definition, in variables]
eqvars_remove_nvars_implies [lemma, in variables]
eqvars_cons_lr [lemma, in variables]
eqvars_disjoint_r [lemma, in variables]
eqvars_app [lemma, in variables]
eqvars_remove_nvars [lemma, in variables]
eqvars_trans [lemma, in variables]
eqvars_nil [lemma, in variables]
eqvars_refl [lemma, in variables]
eqvars_remove_nvar [lemma, in variables]
eqvars_cons_l_iff [lemma, in variables]
eqvars_disjoint [lemma, in variables]
eqvars_sym [lemma, in variables]
eqvars_prop [lemma, in variables]
eq_var_iff [lemma, in variables]
eq_vars_sym [lemma, in variables]
eq_vars_nil [lemma, in variables]
eq_vars [definition, in variables]
eq_var_dec [lemma, in variables]
eq_existsT [definition, in UsefulTypes]
eq_bin_rel [definition, in bin_rels]
eq_subtractv [lemma, in AlphaEqProps]
eq_subtractv_if_right [lemma, in AlphaEqProps]
eq_subtractv_if_left [lemma, in AlphaEqProps]
eq_snoc [lemma, in list]
eq_cons [lemma, in list]
eq_gmapds [lemma, in list]
eq_gmaps [lemma, in list]
eq_maps2 [lemma, in list]
eq_set_empty [lemma, in list]
eq_set_refl2 [lemma, in list]
eq_set_refl [lemma, in list]
eq_set_iff_eq_set2 [lemma, in list]
eq_set2 [definition, in list]
eq_set [definition, in list]
eq_list2 [lemma, in list]
eq_list [lemma, in list]
eq_maps [lemma, in list]
eq_flat_maps [lemma, in list]
eq_lists [lemma, in list]
eq_rel [library]
eq' [definition, in LibTactics]
everything [library]
ex_fresh_var [lemma, in variables]
F
false_in_combine_repeat [lemma, in list]filter [abbreviation, in SSubst]
FilterLIn [lemma, in list]
filter_app [lemma, in list]
filter_snoc [lemma, in list]
Fin [definition, in UsefulTypes]
Finite [definition, in UsefulTypes]
finite [definition, in list]
Finite_Deq [lemma, in UsefulTypes]
Fin_decidable [lemma, in UsefulTypes]
Fin_eq [lemma, in UsefulTypes]
firstn_nil [lemma, in list]
first_index [lemma, in list]
flatten [definition, in CFGV]
flatten [definition, in list]
flat_map_snoc [lemma, in list]
flat_map_app [lemma, in list]
flat_map_as_appl_map [lemma, in list]
flat_map_map [lemma, in list]
flat_map_empty [lemma, in list]
fold_assert [lemma, in UsefulTypes]
fold_subset [lemma, in list]
forall_num_lt_d [lemma, in UsefulTypes]
freevarsEquivariant [lemma, in SwapProps]
freeVarsSupp [lemma, in AlphaEqProps]
freeVarsSuppAux [lemma, in AlphaEqProps]
freeVarsSuppAux2 [lemma, in AlphaEqProps]
freevars_in_allvars [lemma, in AlphaEqProps]
freevars_swap_eq [lemma, in AlphaEqProps]
freevars_labs [definition, in AlphaEqProps]
freevars_abs [definition, in AlphaEqProps]
free_vars_SSubstAux [lemma, in SubstAux]
fresh [projection, in GVariables]
freshCorrect [projection, in GVariables]
FreshDistinctRenamings [definition, in GVariables]
FreshDistinctVars [definition, in GVariables]
FreshDistRenSpec [lemma, in GVariables]
FreshDistRenWSpec [lemma, in GVariables]
FreshDistVarsSpec [lemma, in CFGV]
FreshDistVarsSpec [lemma, in GVariables]
freshString [definition, in GVariables]
freshStringAux [definition, in GVariables]
freshStringAuxSpec [lemma, in GVariables]
freshStringSpec [lemma, in GVariables]
fresh_vars [lemma, in variables]
fresh_distinct_vars_spec1 [lemma, in variables]
fresh_distinct_vars_spec [lemma, in variables]
fresh_distinct_vars [definition, in variables]
fresh_var_nil [lemma, in variables]
fresh_var_nvarx [lemma, in variables]
fresh_var_aux_0 [lemma, in variables]
fresh_var_not_in [lemma, in variables]
fresh_var [definition, in variables]
fresh_var_aux_sorted_not_in [lemma, in variables]
fresh_var_aux_le [lemma, in variables]
fresh_var_aux [definition, in variables]
fst_split_as_map [lemma, in list]
fv [abbreviation, in SSubst]
fvr [abbreviation, in SSubst]
FVSSubst [lemma, in SSubst]
G
GAlphaInd [lemma, in AlphaEquality]getBVarsNth [definition, in Term]
getBVarsNthRange [lemma, in Term]
getBVarsNthRangeContra [lemma, in Term]
getBVarsNth_swap [lemma, in SwapProps]
GFreshDistRenWSpec [lemma, in CFGV]
GFreshVars [definition, in CFGV]
GInduction [definition, in Term]
GInductionS [lemma, in Term]
gmap [lemma, in list]
gmapd [definition, in list]
gmap_eq_d [lemma, in list]
gmap_length [lemma, in list]
Gram [section, in Term]
GramVC [section, in SSubst]
GramVC [section, in SubstAuxAlphaEq]
GramVC [section, in AlphaEquality]
GramVC [section, in SubstAux]
GramVC.G [variable, in SSubst]
GramVC.G [variable, in SubstAuxAlphaEq]
GramVC.G [variable, in AlphaEquality]
GramVC.G [variable, in SubstAux]
GramVC.SSubstRespectsAlpha [section, in SSubst]
GramVC.S1Term1Sub [section, in SSubst]
GramVC.S1Term1Sub1Lv [section, in SSubst]
GramVC.S1Term2Sub [section, in SSubst]
GramVC.vc [variable, in SSubst]
GramVC.vc [variable, in SubstAuxAlphaEq]
GramVC.vc [variable, in AlphaEquality]
GramVC.vc [variable, in SubstAux]
_ === _ [notation, in SSubst]
_ == _ [notation, in SSubst]
GSym [inductive, in CFGV]
gsymNotNT [definition, in CFGV]
gsymNotP [definition, in CFGV]
gsymPN [constructor, in CFGV]
gsymT [constructor, in CFGV]
gsymTN [constructor, in CFGV]
gsymV [constructor, in CFGV]
GVariables [library]
H
hide_hyp [lemma, in tactics]I
iff_push_down_impliesT [lemma, in UsefulTypes]iff_push_down_forallT [lemma, in UsefulTypes]
iff_push_down_forall [lemma, in UsefulTypes]
iff_intro_swap [lemma, in LibTactics]
iff_symm [lemma, in tactics]
implies_lforall [lemma, in list]
implies_in_combine [lemma, in list]
In [definition, in list]
indep_bin_rel [definition, in bin_rels]
injection [definition, in UsefulTypes]
injection_surjection_equipollent [lemma, in UsefulTypes]
injective_fun [definition, in UsefulTypes]
injective_fun_swapVar [lemma, in SwapProps]
injRightsigT [lemma, in UsefulTypes]
inll [abbreviation, in LetrecEx]
inlr [abbreviation, in LetrecEx]
inrr [abbreviation, in LetrecEx]
insert [definition, in variables]
insert_in [lemma, in variables]
intersect [definition, in list]
intersect_vars [lemma, in variables]
intersect_single_l [lemma, in list]
intersect_nil_l [lemma, in list]
intersect_cons_l [lemma, in list]
in_insert [lemma, in variables]
in_remove_nvar [lemma, in variables]
in_remove_nvars [lemma, in variables]
in_nvar_list_dec [lemma, in variables]
in_ALRange_ALFilter_implies [lemma, in SubstAux]
in_cons_iff [lemma, in list]
in_cons_if [lemma, in list]
in_cons_left [lemma, in list]
in_combine_right_eauto [lemma, in list]
in_combine_left_eauto [lemma, in list]
in_nth3 [lemma, in list]
in_single_iff [lemma, in list]
in_combine_repeat [lemma, in list]
in_firstn [lemma, in list]
in_repeat [lemma, in list]
in_combine [lemma, in list]
in_list1_elim [lemma, in list]
in_list1 [lemma, in list]
in_list2_elim [lemma, in list]
in_list2 [lemma, in list]
in_single [lemma, in list]
in_deq_t [lemma, in list]
in_deq [lemma, in list]
in_subset [lemma, in list]
in_snoc [lemma, in list]
in_nth [lemma, in list]
in_app_deq [lemma, in list]
in_map_iff [lemma, in list]
in_app_iff [lemma, in list]
in_diff [lemma, in list]
in_remove [lemma, in list]
isEmbed [definition, in AlphaDecider]
isInl [definition, in UsefulTypes]
isInlInl [definition, in UsefulTypes]
isInr [definition, in UsefulTypes]
isPNode [definition, in AlphaDecider]
isReflSwapping [definition, in SwapProps]
isReflSwapping_cons [lemma, in SwapProps]
issorted [inductive, in variables]
issorted_cons [constructor, in variables]
issorted_nil [constructor, in variables]
isVLeaf [definition, in AlphaDecider]
is_greatest_rel_sat [definition, in bin_rels]
is_ge_any_rel_sat [definition, in bin_rels]
is_first_index_unique [lemma, in list]
is_first_index [definition, in list]
K
keepFirst [abbreviation, in SSubst]L
LAbcase [definition, in AlphaEqProps]lAlAbsCons [constructor, in AlphaEquality]
lAlAbsNil [constructor, in AlphaEquality]
lAlphaEqAbs [inductive, in AlphaEquality]
lAlphaEqAbsMut [definition, in AlphaEquality]
lam [constructor, in LetrecEx]
lasgn [constructor, in LetrecEx]
last_snoc [lemma, in list]
lBoundVars [definition, in Term]
lBoundVarsLength [lemma, in Term]
lBoundVarsLenSameifNth [lemma, in Term]
lBoundVarsmBndngVars [lemma, in Term]
lBoundVarsOld [definition, in Term]
lBoundVarsSameifNth [lemma, in Term]
lBoundVarsSameSSubstAux [lemma, in SubstAux]
lBoundVars_equivariant [lemma, in SwapProps]
lBoundVars_swap [lemma, in SwapProps]
lbShallowNoChange [lemma, in AlphaRen]
leavesLVarUnchanged [definition, in SwapProps]
leavesLVarUnchanged1 [lemma, in SwapProps]
leavesVarUnchanged [definition, in SwapProps]
left_id_injection [lemma, in UsefulTypes]
left_identity [definition, in UsefulTypes]
lengthAppendStr [lemma, in GVariables]
length_pRhsAugIsPat [lemma, in CFGV]
length_combine_eq [lemma, in list]
length_filter [lemma, in list]
length_app [lemma, in list]
length_snoc [lemma, in list]
length0 [lemma, in list]
length1 [lemma, in list]
length2 [lemma, in list]
length3 [lemma, in list]
length4 [lemma, in list]
len_flat_map [lemma, in list]
letr [constructor, in LetrecEx]
letrecCFGV [definition, in LetrecEx]
LetrecEx [library]
LetrecFEx [library]
letr_xyz [definition, in LetrecEx]
le_var [definition, in variables]
le_bin_rel [definition, in bin_rels]
le_binrel_list_un [lemma, in list]
lForall [definition, in list]
lforall [definition, in list]
lforallApp [lemma, in list]
lForallSame [lemma, in list]
lhead [definition, in list]
lheadEquivariant [lemma, in SwapProps]
LibTactics [library]
LibTacticsCompatibility [module, in LibTactics]
liftInl [definition, in UsefulTypes]
liftNth [definition, in UsefulTypes]
liftPointwise [definition, in list]
liftRelPtwise [definition, in Term]
lift_bin_rel_ifdp [lemma, in bin_rels]
lift_bin_rel_if [lemma, in bin_rels]
LIn [definition, in list]
LInEquivariant [lemma, in SwapProps]
LInSeqIff [lemma, in list]
Lin_eauto2 [lemma, in list]
Lin_eauto1 [lemma, in list]
lin_lift [lemma, in list]
lin_flat_map [lemma, in list]
list [library]
lKeep [definition, in list]
lKeepDisjoint [lemma, in list]
lKeepSubset [lemma, in list]
lmax [definition, in GVariables]
lmaxSpec [lemma, in GVariables]
lmaxSpecLen [lemma, in GVariables]
ltac_to_generalize [definition, in LibTactics]
ltac_tag_subst [definition, in LibTactics]
ltac_nat_from_int [definition, in LibTactics]
ltac_database_provide [lemma, in LibTactics]
ltac_database [definition, in LibTactics]
ltac_mark [constructor, in LibTactics]
ltac_Mark [inductive, in LibTactics]
ltac_wilds [constructor, in LibTactics]
ltac_Wilds [inductive, in LibTactics]
ltac_wild [constructor, in LibTactics]
ltac_Wild [inductive, in LibTactics]
ltac_no_arg [constructor, in LibTactics]
ltac_No_arg [inductive, in LibTactics]
ltac_something_show [lemma, in tactics]
ltac_something_hide [lemma, in tactics]
ltac_something_eq [lemma, in tactics]
ltac_something [definition, in tactics]
lt_var [definition, in variables]
lVars [definition, in AlphaRen]
lvKeep [definition, in Term]
M
MakeAbsPNodeCommute [lemma, in AlphaEquality]MakeAbsPnodeSame [lemma, in AlphaEqProps]
MakeAbsTNodeCommute [lemma, in AlphaEquality]
MakeAbstractions [definition, in AlphaEquality]
MakeAbstractionsPNode [definition, in AlphaEquality]
MakeAbstractionsTNode [definition, in AlphaEquality]
MakeAbstractionsTNodeAux [definition, in AlphaEquality]
MakeLAbsSwapCommute [lemma, in AlphaEquality]
MakeLAbsSwapCommute [lemma, in AlphaRen]
mAllButBinders [definition, in Term]
mAllVars [definition, in Term]
mAlphaEq [definition, in AlphaEquality]
mAlreadyBndBinders [definition, in Term]
map_length [lemma, in GVariables]
map_firstn [lemma, in list]
map_cons [lemma, in list]
map_diff_commute [lemma, in list]
map_remove_commute [lemma, in list]
map_eq_injective [lemma, in list]
map_gmap_eq [lemma, in list]
map_eq_length_eq [lemma, in list]
map_combine [lemma, in list]
map_snoc [lemma, in list]
map_map [lemma, in list]
map_flat_map [lemma, in list]
maxl [definition, in list]
maxl_prop [lemma, in list]
max_or [lemma, in UsefulTypes]
max_prop2 [lemma, in UsefulTypes]
max_prop1 [lemma, in UsefulTypes]
mBndngVars [definition, in Term]
mBndngVarsAsNth [lemma, in Term]
mBndngVarsDeep [definition, in Term]
mBndngVarsSameIfNth [lemma, in Term]
mBndngVarsShallowSame [lemma, in AlphaRen]
mcase [definition, in Term]
memberb [definition, in list]
memberb_din [lemma, in list]
memberb_app [lemma, in list]
memvar [definition, in variables]
memvar_dmemvar [lemma, in variables]
memvar_singleton_diff_r [lemma, in variables]
memvar_singleton [lemma, in variables]
memvar_app [lemma, in variables]
mfreevars [definition, in Term]
mFresh [definition, in Swap]
minus0 [lemma, in UsefulTypes]
min_eq [lemma, in UsefulTypes]
MixInd [definition, in Term]
MixMap [definition, in Term]
MixMapLength [lemma, in Term]
Mixture [inductive, in Term]
MixtureParam [definition, in CFGV]
mix_mut [definition, in Term]
mkAsgn [definition, in LetrecEx]
mkLAsgn [definition, in LetrecEx]
mkLetr [definition, in LetrecEx]
mkVTerm [definition, in LetrecEx]
mLSwapTermEmbed [definition, in AlphaRen]
mLSwapTermEmbedSameBinders [lemma, in AlphaRen]
mLSwapTermEmbedSameLBV [lemma, in AlphaRen]
mLSwapTermEmbedSameNthBinder [lemma, in AlphaRen]
mnil [constructor, in Term]
monotoneFilter [lemma, in list]
monotoneSetFn [definition, in list]
monotoneSetFnFlatMap [lemma, in list]
monotoneSetFnMap [lemma, in list]
monotone_eauto [lemma, in list]
MParamCorrectb [definition, in CFGV]
mpcons [constructor, in Term]
mRenAlpha [definition, in AlphaRen]
mRenBinders [definition, in AlphaRen]
mRenBindersSpec3 [lemma, in AlphaRen]
mRenlBinderShallowSame [lemma, in AlphaRen]
mSize [definition, in Term]
mSSubstAux [definition, in SubstAux]
mSwap [definition, in Swap]
mSwapEmbed [definition, in Swap]
mtcons [constructor, in Term]
N
nat_compare_dec [lemma, in list]nat2string [lemma, in GVariables]
ndRenAlAxAlpha [lemma, in AlphaRen]
ndRenAlAxSpecDisj [lemma, in AlphaRen]
ndRenAlAxSpecDisjAux [lemma, in AlphaRen]
negb_eq_true [lemma, in UsefulTypes]
NegLInEquivariant [lemma, in SwapProps]
nil_subset_iff [lemma, in list]
nil_subset [lemma, in list]
nil_snoc_false [lemma, in list]
nodeRenAlphaAux [definition, in AlphaRen]
NoRepeatsEquivariant [lemma, in SwapProps]
not_over_not_lin_nvar [lemma, in variables]
not_eq_beq_var_false [lemma, in variables]
not_false_is_true [lemma, in UsefulTypes]
not_over_or [lemma, in UsefulTypes]
not_or [lemma, in UsefulTypes]
not_of_assert [lemma, in UsefulTypes]
not_assert [lemma, in UsefulTypes]
not_in_prefix [definition, in list]
not_in_subset [lemma, in list]
no_repeats_singleton [lemma, in list]
no_repeat_dec [lemma, in list]
no_rep_flat_map_seq2 [lemma, in list]
no_rep_flat_map_seq1 [lemma, in list]
no_repeats_app [lemma, in list]
no_repeats_cons [lemma, in list]
no_repeats_index_unique2 [lemma, in list]
no_repeats_index_unique [lemma, in list]
no_rep_cons [constructor, in list]
no_rep_nil [constructor, in list]
no_repeats [inductive, in list]
nth_in2 [lemma, in list]
nth_select3 [lemma, in list]
nth_select2 [lemma, in list]
nth_select1 [lemma, in list]
nth_in [lemma, in list]
nth2 [lemma, in list]
nth2_equiv [lemma, in list]
nth3 [lemma, in list]
null [definition, in list]
nullb [definition, in list]
null_remove_nvars_subvars [lemma, in variables]
null_remove_nvars [lemma, in variables]
null_subset [lemma, in list]
null_diff_subset [lemma, in list]
null_map [lemma, in list]
null_app [lemma, in list]
null_cons [lemma, in list]
null_iff_nil [lemma, in list]
null_diff [lemma, in list]
null_nil_iff [lemma, in list]
null_nil [lemma, in list]
nvar [constructor, in variables]
NVar [inductive, in variables]
nvara [definition, in variables]
nvarb [definition, in variables]
nvarc [definition, in variables]
nvard [definition, in variables]
nvarf [definition, in variables]
nvarg [definition, in variables]
nvarh [definition, in variables]
nvari [definition, in variables]
nvarj [definition, in variables]
nvark [definition, in variables]
nvarl [definition, in variables]
nvarVarType [definition, in GVariables]
nvarx [definition, in variables]
nvary [definition, in variables]
nvarz [definition, in variables]
O
oneSwapVar [definition, in Swap]oneSwapVar_prop_s1 [lemma, in SwapProps]
or_false_l [lemma, in UsefulTypes]
or_false_r [lemma, in UsefulTypes]
or_true_r [lemma, in UsefulTypes]
or_true_l [lemma, in UsefulTypes]
P
pairInProofs [lemma, in list]pairInProofsCons [lemma, in list]
pair_inj [lemma, in UsefulTypes]
pAllButBinders [definition, in Term]
pAllVars [definition, in Term]
pAlphaEq [inductive, in AlphaEquality]
pAlphaEqEquivariantRev [lemma, in AlphaEqProps]
pAlphaEqG [definition, in AlphaDecider]
pAlphaEqMut [definition, in AlphaEquality]
pAlphaEqTransEauto [lemma, in AlphaEqProps]
pAlphaSwapEmSwap [lemma, in AlphaEqProps]
pAlreadyBndBinders [definition, in Term]
PAT [definition, in LetrecEx]
patAbs [constructor, in AlphaEquality]
PatInd [definition, in Term]
PatIndNoEmbed [lemma, in Term]
PatInMix [definition, in Term]
PatProd [inductive, in LetrecEx]
PatProd [projection, in CFGV]
Pattern [inductive, in Term]
pat_mut [definition, in Term]
pBndngVars [definition, in Term]
pBndngVarsDeep [definition, in Term]
pBndngVars_swap [lemma, in SwapProps]
pcase [definition, in Term]
pfreevars [definition, in Term]
pFresh [definition, in Swap]
pFreshSubset [lemma, in Swap]
pFresh_app [lemma, in AlphaEqProps]
pnode [constructor, in Term]
PNonTerminal [inductive, in LetrecEx]
PNonTerminal [projection, in CFGV]
ppLhs [definition, in CFGV]
ppLhsRhs [definition, in LetrecEx]
ppLhsRhs [projection, in CFGV]
ppRhsSym [definition, in CFGV]
pRenAlpha [definition, in AlphaRen]
pRenBinders [definition, in AlphaRen]
pRenBindersAlpha [lemma, in AlphaRen]
prhsIsBound [definition, in CFGV]
prhs_aux [definition, in CFGV]
prod_comm [lemma, in UsefulTypes]
prod_assoc [lemma, in UsefulTypes]
prod_sym [lemma, in tactics]
projT [variable, in UsefulTypes]
pSize [definition, in Term]
pSSubstAux [definition, in SubstAux]
pSwap [definition, in Swap]
pSwapEmbed [definition, in Swap]
ptleaf [constructor, in Term]
ptrhs_aux_nonNT [lemma, in CFGV]
ptrhs_aux [definition, in CFGV]
pvleaf [constructor, in Term]
R
rangeFreeVars [definition, in SubstAux]rangeFreeVarsApp [lemma, in SubstAux]
rangeFreeVarsEquivariant [lemma, in SubstAuxAlphaEq]
rangeFreeVarsKeepFirstAppImplies [lemma, in SubstAux]
rangeFreeVarsKeepFirstAppL [lemma, in SubstAux]
rangeFreeVarsKeepFirstAppR [lemma, in SubstAux]
rangeFreeVars_ALFilter_subset [lemma, in SubstAux]
rangeFreeVars_cons [lemma, in SubstAux]
refl_rel [definition, in bin_rels]
removev [definition, in Term]
remove_nvar_comm [lemma, in variables]
remove_nvar_insert [lemma, in variables]
remove_nvars_eq [lemma, in variables]
remove_nvar_cons [lemma, in variables]
remove_nvars_cons_r [lemma, in variables]
remove_nvars_cons_l_weak [lemma, in variables]
remove_nvars_cons [lemma, in variables]
remove_nvars_move [lemma, in variables]
remove_nvars_dup [lemma, in variables]
remove_nvars_comm [lemma, in variables]
remove_nvars_flat_map [lemma, in variables]
remove_nvars_app_l [lemma, in variables]
remove_nvars_app_r [lemma, in variables]
remove_nvars_nil_r [lemma, in variables]
remove_var_nil [lemma, in variables]
remove_nvars_nil_l [lemma, in variables]
remove_nvars_unchanged [lemma, in variables]
remove_nvar_nil [lemma, in variables]
remove_nvar [definition, in variables]
remove_nvars [definition, in variables]
remove_dup [lemma, in list]
remove_repeat [lemma, in list]
remove_comm [lemma, in list]
remove_app [lemma, in list]
remove_trivial [lemma, in list]
RenAlphaAlpha [lemma, in AlphaRen]
RenAlphaAvoid [lemma, in AlphaRen]
RenAlphaNoChange [lemma, in AlphaRen]
renBindersLBVLenSame [lemma, in AlphaRen]
renBindersSameLength [lemma, in AlphaRen]
RenBindersSpec [lemma, in AlphaRen]
RenBindersSpec2 [lemma, in AlphaRen]
RenBindersSpec3 [lemma, in AlphaRen]
repeat [definition, in list]
repeat_length [lemma, in list]
revSubest1 [lemma, in list]
revSubest2 [lemma, in list]
rev_list_ind [lemma, in list]
rev_list_dest2 [lemma, in list]
rev_list_dest [lemma, in list]
rev_list_indT [lemma, in list]
rm [definition, in LibTactics]
S
sdkfd [lemma, in Term]select [definition, in list]
select_in [lemma, in list]
select_lt [lemma, in list]
seq_length [lemma, in GVariables]
shead [definition, in GVariables]
sigTDeq [definition, in UsefulTypes]
simple_combine_app_app [lemma, in AlphaEqProps]
SimplifyForPaper [module, in Term]
SimplifyForPaper.allBndngVars [definition, in Term]
simpl_fst [lemma, in list]
singleton_as_snoc [lemma, in list]
singleton_subset [lemma, in list]
SizePositive [lemma, in Term]
skip_axiom [variable, in LibTactics]
snoc [definition, in list]
snoc_inj [lemma, in list]
snoc_cases [lemma, in list]
snoc_append_l [lemma, in list]
snoc_append_r [lemma, in list]
snoc_as_append [lemma, in list]
snoc1 [lemma, in list]
some_inj [lemma, in list]
sort [definition, in variables]
sort_issorted [lemma, in variables]
sort_eqvars [lemma, in variables]
split_cons [lemma, in list]
split_eta [lemma, in list]
split_length_eq [lemma, in list]
SSubst [library]
SSubstAuxAppAwap [lemma, in SubstAux]
SSubstAuxBVarsDisjoint [lemma, in SubstAux]
SSubstAuxNestAsApp [lemma, in SubstAux]
SSubstAuxNestSwap [lemma, in SubstAux]
SSubstAuxNilNoChange [lemma, in SubstAux]
SSubstAuxSubFilter [lemma, in SubstAux]
SSubstAuxTrivial [lemma, in SubstAux]
SSubstFilter [lemma, in SSubst]
SSubstFVarsDisjoint [lemma, in SSubst]
SSubstitution [definition, in SubstAux]
SSubstNestAsApp [lemma, in SSubst]
SSubstNestSwap [lemma, in SSubst]
SSubstRespectsAlpha [lemma, in SSubst]
SSubstRespectsAlpha1 [lemma, in SSubst]
SSubstRespectsAlpha2 [lemma, in SSubst]
SSubstSubRespectsAlpha [lemma, in SSubst]
StringVar [lemma, in GVariables]
subAlphaSameFV [lemma, in SubstAuxAlphaEq]
SubFilter [definition, in SubstAux]
SubKeepFirst [definition, in SubstAux]
subset [definition, in list]
subsetAlbindersDeep [lemma, in SubstAuxAlphaEq]
subsetAppEauto [lemma, in list]
subsetAppEauto2 [lemma, in list]
subsetAppEauto3 [lemma, in list]
subsetb [definition, in list]
subsetb_subset [lemma, in list]
subsetConsEauto [lemma, in list]
subsetFlatMap2Eauto [lemma, in list]
subsetSingleFlatMap [lemma, in list]
subset_disjoint_r [lemma, in list]
subset_app_lr [lemma, in list]
subset_eq [lemma, in list]
subset_eauto [lemma, in list]
subset_singleton_r [lemma, in list]
subset_disjointLR [lemma, in list]
subset_disjoint [lemma, in list]
subset_diff [lemma, in list]
subset_flat_map [lemma, in list]
subset_cons_l [lemma, in list]
subset_snoc_l [lemma, in list]
subset_snoc_r [lemma, in list]
subset_app [lemma, in list]
subset_app_l [lemma, in list]
subset_app_r [lemma, in list]
subset_cons2 [lemma, in list]
subset_cons1 [lemma, in list]
subset_cons_nil [lemma, in list]
subset_trans [lemma, in list]
subset_nil_l_iff [lemma, in list]
subset_nil_l [lemma, in list]
subset_refl_iff [lemma, in list]
subset_refl [lemma, in list]
SubstAux [library]
SubstAuxAlphaEq [library]
SubstAuxRespectsAlpha [lemma, in SubstAuxAlphaEq]
SubstAuxRespectsAlpha2 [lemma, in SubstAuxAlphaEq]
SubstFilterDisjAux [lemma, in SubstAuxAlphaEq]
SubstSub [definition, in SSubst]
SubstSubAsSubstAux [lemma, in SSubst]
SubstSubFVarsDisjoint [lemma, in SSubst]
subSwapAlpha [lemma, in SubstAuxAlphaEq]
subtractv [definition, in Term]
subtractv_cons [lemma, in Term]
subtractv_disjoint [lemma, in Term]
subtractv_disjoint_subset [lemma, in Term]
subtractv_app_r [lemma, in Term]
subtractv_app_l [lemma, in AlphaEqProps]
subtractv_nil_l [lemma, in AlphaEqProps]
subtractv_nil [lemma, in AlphaEqProps]
subtractv_subset [lemma, in SubstAux]
subvars [definition, in variables]
subvars_disjoint_r [lemma, in variables]
subvars_disjoint_l [lemma, in variables]
subvars_cons_lr [lemma, in variables]
subvars_not_in [lemma, in variables]
subvars_eqvars [lemma, in variables]
subvars_nil_r [lemma, in variables]
subvars_cons_r_weak_if_not_in [lemma, in variables]
subvars_app_trivial_r [lemma, in variables]
subvars_app_trivial_l [lemma, in variables]
subvars_trans [lemma, in variables]
subvars_swap_r [lemma, in variables]
subvars_app_remove_nvars_r [lemma, in variables]
subvars_app_l [lemma, in variables]
subvars_snoc_weak [lemma, in variables]
subvars_nil_l_iff [lemma, in variables]
subvars_nil_l [lemma, in variables]
subvars_cons_r [lemma, in variables]
subvars_cons_l [lemma, in variables]
subvars_remove_nvars [lemma, in variables]
subvars_flat_map [lemma, in variables]
subvars_comm_r [lemma, in variables]
subvars_singleton_r [lemma, in variables]
subvars_singleton_l [lemma, in variables]
subvars_app_weak_l [lemma, in variables]
subvars_prop [lemma, in variables]
subvars_refl [lemma, in variables]
subvars_eq [lemma, in variables]
sub_vars [definition, in variables]
sum_assoc [lemma, in UsefulTypes]
sum_sym [lemma, in tactics]
Swap [library]
swapAbs [definition, in AlphaEquality]
swapBndngVarsCommute [lemma, in AlphaEquality]
swapCommonBinders [lemma, in SwapProps]
swapDisjChain [lemma, in SwapProps]
swapEmbedAbs [definition, in AlphaRen]
swapEmbedLAbs [definition, in AlphaRen]
SwapEmbedSameBinders [lemma, in SwapProps]
SwapEmbedSpec [lemma, in SwapProps]
swapEmbed_prop_s1_aux [lemma, in SwapProps]
swapLAbs [definition, in AlphaEquality]
swapLBoundVarsCommute [lemma, in AlphaEquality]
swapLLVar [definition, in Swap]
swapLVar [definition, in Swap]
swapLVarApp [lemma, in SwapProps]
swapLVarDisjChain [lemma, in SwapProps]
swapLVarDisjoint [lemma, in SwapProps]
swapLVarDisjoint2 [lemma, in SwapProps]
swapLVarNoChange [lemma, in SwapProps]
swapLVarRevCancel [lemma, in SwapProps]
swapLVarRevNoRep [lemma, in SwapProps]
swapLVarSwitch [lemma, in SwapProps]
swapLVar_subset [lemma, in SwapProps]
swapLVar_subtractv [lemma, in SwapProps]
swapLVar_flat_map [lemma, in SwapProps]
swapLVar_app [lemma, in SwapProps]
Swapping [definition, in Swap]
swapPreservesSize [lemma, in SwapProps]
SwapProps [section, in SwapProps]
SwapProps [library]
swapRevNoRep [lemma, in SwapProps]
swapSub [definition, in SubstAuxAlphaEq]
swapSubApp [lemma, in SubstAuxAlphaEq]
swapSubFilterCommute [lemma, in SubstAuxAlphaEq]
swapSubRevCancel [lemma, in SubstAuxAlphaEq]
swapSubRevNoRep [lemma, in SubstAuxAlphaEq]
swapSubSwitch [lemma, in SubstAuxAlphaEq]
swapSwap [definition, in Swap]
swapSwitch [lemma, in SwapProps]
swapVar [definition, in Swap]
swapVarDisjChain [lemma, in SwapProps]
swapVarImplies [lemma, in SwapProps]
swapvarImplies2 [lemma, in SwapProps]
swapVarIn [lemma, in SwapProps]
swapVarInj [lemma, in SwapProps]
swapVarInOrEq [lemma, in SwapProps]
swapVarInOrEq2 [lemma, in SwapProps]
swapVarNoChange [lemma, in SwapProps]
swapVarNoChange2 [lemma, in SwapProps]
swapVarNonChangeRev [lemma, in SwapProps]
swapVarRevNoRep [lemma, in SwapProps]
swapVarSwitch [lemma, in SwapProps]
swapVar_in [lemma, in AlphaEqProps]
swapVar_unchanged [lemma, in AlphaEqProps]
swapVar_e1stronger [lemma, in SwapProps]
swapVar_s2stronger2 [lemma, in SwapProps]
swapVar_s2stronger [lemma, in SwapProps]
swapVar_app [lemma, in SwapProps]
swapVar_S2app [lemma, in SwapProps]
swapVar_S2 [lemma, in SwapProps]
swapVar_prop_s1 [lemma, in SwapProps]
swap_prop_e1Stronger [lemma, in SwapProps]
swap_app [lemma, in SwapProps]
swap_prop_s2Stronger [lemma, in SwapProps]
swap_prop_s3 [lemma, in SwapProps]
swap_prop_s1 [lemma, in SwapProps]
swap_prop_s1_aux [lemma, in SwapProps]
symm_rel [definition, in bin_rels]
SYMPN [abbreviation, in LetrecEx]
SYMTN [abbreviation, in LetrecEx]
S_lt_inj [lemma, in UsefulTypes]
S_le_inj [lemma, in UsefulTypes]
S_inj [lemma, in UsefulTypes]
T
tactics [library]tailEquivariant [lemma, in SwapProps]
tail_subset [lemma, in SubstAux]
tAllVars [definition, in Term]
tAlphaEq [inductive, in AlphaEquality]
tAlphaEqDecidable [lemma, in AlphaDecider]
tAlphaEqEquivariantRev [lemma, in AlphaEqProps]
tAlphaEqG [definition, in AlphaDecider]
tAlphaEqMut [definition, in AlphaEquality]
talphaEqRefl [lemma, in AlphaEqProps]
tAlphaEqTransEauto [lemma, in AlphaEqProps]
tAlphaEqual [definition, in AlphaEquality]
tBndngVarsDeep [definition, in Term]
tcase [definition, in Term]
TERM [definition, in LetrecEx]
term [constructor, in LetrecEx]
Term [inductive, in Term]
Term [library]
termAbs [constructor, in AlphaEquality]
Terminal [inductive, in LetrecEx]
Terminal [projection, in CFGV]
TermInd [definition, in Term]
TermIndNoPat [lemma, in Term]
TermInMix [definition, in Term]
TermProd [inductive, in LetrecEx]
TermProd [projection, in CFGV]
term_mut [definition, in Term]
tfreevars [definition, in Term]
tFresh [definition, in Swap]
tFreshSubset [lemma, in Swap]
tFresh_app_l [lemma, in AlphaEqProps]
tFresh_app [lemma, in AlphaEqProps]
tiff_is_prod_implies2 [lemma, in eq_rel]
tiff_is_prod_implies1 [lemma, in eq_rel]
tiff_snd [definition, in eq_rel]
tiff_fst [definition, in eq_rel]
tiff_trans [lemma, in eq_rel]
tleaf [constructor, in Term]
tnode [constructor, in Term]
TNonTerminal [inductive, in LetrecEx]
TNonTerminal [projection, in CFGV]
tpLhs [definition, in CFGV]
tpLhsRhs [definition, in LetrecEx]
tpLhsRhs [projection, in CFGV]
tpRhsAugIsPat [definition, in CFGV]
tpRhsSym [definition, in CFGV]
transport [definition, in UsefulTypes]
transRel [definition, in AlphaEqProps]
trans_rel [definition, in bin_rels]
tRenAlpha [definition, in AlphaRen]
tRenWithSpec [lemma, in AlphaRen]
trivial_if [lemma, in UsefulTypes]
true_eq_nvar [lemma, in variables]
tSemType [projection, in CFGV]
tSize [definition, in Term]
tSSubst [definition, in SSubst]
tSSubstAux [definition, in SubstAux]
tSSubstAuxSubFilter [lemma, in SubstAux]
tSSubstAuxSubUnfold [lemma, in SubstAux]
tSSubstAux_sub_trivial [lemma, in SubstAux]
tSSubstAux_sub [definition, in SubstAux]
tSwap [definition, in Swap]
tSwapBndngVarsDisjoint [lemma, in SwapProps]
two_as_app [lemma, in list]
typ [projection, in GVariables]
typeCast [definition, in UsefulTypes]
TypeC_S [lemma, in eq_rel]
t_c_iff [definition, in eq_rel]
t_iff_sym [lemma, in eq_rel]
t_iff_refl [lemma, in eq_rel]
t_iff_cons [constructor, in eq_rel]
t_iff [inductive, in eq_rel]
U
UIPReflDeq [lemma, in UsefulTypes]universe [library]
UsefulTypes [library]
V
validBsl [definition, in CFGV]ValidIndices [definition, in CFGV]
ValidIndicesDecidable [lemma, in CFGV]
ValidNthSrc [definition, in CFGV]
VAR [abbreviation, in LetrecEx]
variables [library]
varSem [projection, in CFGV]
VarSubSym [definition, in SubstAux]
VarSym [inductive, in LetrecEx]
VarSym [projection, in CFGV]
VarType [record, in GVariables]
vcAbstraction [abbreviation, in AlphaEqProps]
vcDeq [abbreviation, in AlphaEquality]
vcType [abbreviation, in AlphaEquality]
vcType [abbreviation, in AlphaEqProps]
vcType [abbreviation, in SwapProps]
vFreshDiff [definition, in CFGV]
vFreshDiffSpec [lemma, in CFGV]
vFreshVar [definition, in CFGV]
vFreshVarSpec [lemma, in CFGV]
vleaf [constructor, in Term]
void [inductive, in eq_rel]
vSubstType [definition, in LetrecEx]
vSubstType [projection, in CFGV]
vsym [constructor, in LetrecEx]
vType [definition, in CFGV]
Z
zip [abbreviation, in AlphaEquality]other
_ -- _ (list_scope) [notation, in Term]>> _ _ _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ (ltac_scope) [notation, in LibTactics]
>> _ (ltac_scope) [notation, in LibTactics]
>> (ltac_scope) [notation, in LibTactics]
___ (ltac_scope) [notation, in LibTactics]
__ (ltac_scope) [notation, in LibTactics]
exists _ _ _ _ _ _ _ _ _ _ , _ (type_scope) [notation, in LibTactics]
exists _ _ _ _ _ _ _ _ _ , _ (type_scope) [notation, in LibTactics]
exists _ _ _ _ _ _ _ _ , _ (type_scope) [notation, in LibTactics]
exists _ _ _ _ _ _ _ , _ (type_scope) [notation, in LibTactics]
exists _ _ _ _ _ _ , _ (type_scope) [notation, in LibTactics]
exists _ _ _ _ _ , _ (type_scope) [notation, in LibTactics]
exists _ _ _ _ , _ (type_scope) [notation, in LibTactics]
exists _ _ _ , _ (type_scope) [notation, in LibTactics]
exists _ _ , _ (type_scope) [notation, in LibTactics]
exists _ , _ (type_scope) [notation, in LibTactics]
_ =$= _ [notation, in SSubst]
_ <~> _ [notation, in eq_rel]
_ <==> _ [notation, in eq_rel]
_ <=> _ [notation, in eq_rel]
_ =' _ [notation, in LibTactics]
_ [+] _ [notation, in universe]
_ # _ [notation, in universe]
exI( _ , _ ) [notation, in universe]
injL( _ ) [notation, in universe]
injR( _ ) [notation, in universe]
nosimpl _ [notation, in LibTactics]
Register _ _ [notation, in LibTactics]
Something [notation, in tactics]
! _ [notation, in universe]
[univ] [notation, in universe]
[ _ , .. , _ ] [notation, in UsefulTypes]
{ _ , _ , _ , _ , _ , _ : _ $ _ } [notation, in UsefulTypes]
{ _ , _ , _ , _ , _ : _ $ _ } [notation, in UsefulTypes]
{ _ , _ , _ , _ : _ $ _ } [notation, in UsefulTypes]
{ _ , _ , _ : _ $ _ } [notation, in UsefulTypes]
{ _ , _ : _ $ _ } [notation, in UsefulTypes]
{ _ : _ $ _ } [notation, in universe]
Notation Index
G
_ === _ [in SSubst]_ == _ [in SSubst]
other
_ -- _ (list_scope) [in Term]>> _ _ _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ (ltac_scope) [in LibTactics]
>> _ _ (ltac_scope) [in LibTactics]
>> _ (ltac_scope) [in LibTactics]
>> (ltac_scope) [in LibTactics]
___ (ltac_scope) [in LibTactics]
__ (ltac_scope) [in LibTactics]
exists _ _ _ _ _ _ _ _ _ _ , _ (type_scope) [in LibTactics]
exists _ _ _ _ _ _ _ _ _ , _ (type_scope) [in LibTactics]
exists _ _ _ _ _ _ _ _ , _ (type_scope) [in LibTactics]
exists _ _ _ _ _ _ _ , _ (type_scope) [in LibTactics]
exists _ _ _ _ _ _ , _ (type_scope) [in LibTactics]
exists _ _ _ _ _ , _ (type_scope) [in LibTactics]
exists _ _ _ _ , _ (type_scope) [in LibTactics]
exists _ _ _ , _ (type_scope) [in LibTactics]
exists _ _ , _ (type_scope) [in LibTactics]
exists _ , _ (type_scope) [in LibTactics]
_ =$= _ [in SSubst]
_ <~> _ [in eq_rel]
_ <==> _ [in eq_rel]
_ <=> _ [in eq_rel]
_ =' _ [in LibTactics]
_ [+] _ [in universe]
_ # _ [in universe]
exI( _ , _ ) [in universe]
injL( _ ) [in universe]
injR( _ ) [in universe]
nosimpl _ [in LibTactics]
Register _ _ [in LibTactics]
Something [in tactics]
! _ [in universe]
[univ] [in universe]
[ _ , .. , _ ] [in UsefulTypes]
{ _ , _ , _ , _ , _ , _ : _ $ _ } [in UsefulTypes]
{ _ , _ , _ , _ , _ : _ $ _ } [in UsefulTypes]
{ _ , _ , _ , _ : _ $ _ } [in UsefulTypes]
{ _ , _ , _ : _ $ _ } [in UsefulTypes]
{ _ , _ : _ $ _ } [in UsefulTypes]
{ _ : _ $ _ } [in universe]
Module Index
L
LibTacticsCompatibility [in LibTactics]S
SimplifyForPaper [in Term]Variable Index
A
AssociationList.DeqKey [in AssociationList]AssociationList.Key [in AssociationList]
AssociationList.Value [in AssociationList]
G
GramVC.G [in SSubst]GramVC.G [in SubstAuxAlphaEq]
GramVC.G [in AlphaEquality]
GramVC.G [in SubstAux]
GramVC.vc [in SSubst]
GramVC.vc [in SubstAuxAlphaEq]
GramVC.vc [in AlphaEquality]
GramVC.vc [in SubstAux]
P
projT [in UsefulTypes]S
skip_axiom [in LibTactics]Library Index
A
AlphaDeciderAlphaEqProps
AlphaEquality
AlphaRen
AssociationList
B
bin_relsC
CFGVE
eq_releverything
G
GVariablesL
LetrecExLetrecFEx
LibTactics
list
S
SSubstSubstAux
SubstAuxAlphaEq
Swap
SwapProps
T
tacticsTerm
U
universeUsefulTypes
V
variablesLemma Index
A
albndDeepMakeAbPSubset [in SubstAuxAlphaEq]albndDeepMakeAbTSubset [in SubstAuxAlphaEq]
ALDomCombine [in AssociationList]
ALDomFilterCommute [in AssociationList]
ALEndoMapFilterCommute [in AssociationList]
ALFilterAppAsDiff [in AssociationList]
ALFilterAppR [in AssociationList]
ALFilterAppSub [in AssociationList]
ALFilterDom [in AssociationList]
ALFilterLIn [in AssociationList]
ALFilterSubset [in AssociationList]
ALFilterSwap [in AssociationList]
ALFilter_nil_r [in AssociationList]
ALFindApp [in AssociationList]
ALFindDef2Same [in AssociationList]
ALFindEndoMapSome [in AssociationList]
ALFindFilterNone [in AssociationList]
ALFindFilterSome [in AssociationList]
ALFindMapNone [in AssociationList]
ALFindMapSome [in AssociationList]
ALFindNone [in AssociationList]
ALFindNoneKeepFirstSingleton [in AssociationList]
ALFindRangeMapNone [in AssociationList]
ALFindRangeMapSome [in AssociationList]
ALFindSome [in AssociationList]
ALFindSomeKeepFirstSingleton [in AssociationList]
ALFind2 [in AssociationList]
ALInEta [in AssociationList]
ALKeepFirstAppLin [in AssociationList]
ALKeepFirstFilterDiff [in AssociationList]
ALKeepFirstLin [in AssociationList]
ALKeepFirstLinApp [in AssociationList]
ALKeepFirstNil [in AssociationList]
ALKeepFirstSubst [in AssociationList]
AllButBindersSubset [in Term]
AllVarsEquivariant [in SwapProps]
ALMapFilterCommute [in AssociationList]
ALMapRangeFilterCommute [in AssociationList]
ALMapRangeFindCommute [in AssociationList]
AlphaEqAbsPSameParam [in AlphaEqProps]
AlphaEqAbsTSameParam [in AlphaEqProps]
alphaEqAlphaSubst [in SubstAuxAlphaEq]
alphaEqDecidable [in AlphaDecider]
AlphaEqNilAbsP [in AlphaEqProps]
AlphaEqNilAbsT [in AlphaEqProps]
alphaEqRefl [in AlphaEqProps]
AlphaEqSubstApp [in SubstAuxAlphaEq]
AlphaEqSubstRefl [in SubstAuxAlphaEq]
alphaEqSwapNonFree [in AlphaEqProps]
alphaEqSym [in AlphaEqProps]
alphaEqTransitive [in AlphaEqProps]
alphaEquiVariant [in AlphaEqProps]
alpha_preserves_free_vars [in AlphaEqProps]
ALRangeCombine [in AssociationList]
ALRangeRelApp [in AssociationList]
ALRangeRelFilter [in AssociationList]
ALRangeRelFind [in AssociationList]
ALRangeRelRefl [in AssociationList]
ALRangeRelSameDom [in AssociationList]
alSSubstAux_MakeAbstractionsPNode [in SubstAuxAlphaEq]
alSSubstAux_MakeAbstractionsTNode [in SubstAuxAlphaEq]
ALSwitchCombine [in AssociationList]
andb_eq_true [in UsefulTypes]
andb_true [in UsefulTypes]
and_true_r [in UsefulTypes]
and_true_l [in UsefulTypes]
and_tiff_compat_l [in UsefulTypes]
apply_eq [in UsefulTypes]
app_if [in list]
app_eq_nil_iff [in list]
app_split [in list]
app_subset [in list]
assert_memvar_false [in variables]
assert_sub_vars [in variables]
assert_eq_vars [in variables]
assert_memvar [in variables]
assert_of_andb [in UsefulTypes]
assert_andb [in UsefulTypes]
assert_orb [in UsefulTypes]
assert_memberb [in list]
assert_beq_list [in list]
assert_eqsetb [in list]
assert_subsetb [in list]
assert_nullb [in list]
AvRenamingSubset [in AlphaRen]
B
ball_map_true [in list]ball_true [in list]
beq_var_sym [in variables]
beq_var_false [in variables]
beq_var_false_not_eq [in variables]
beq_var_true [in variables]
beq_var_eq [in variables]
beq_var_refl [in variables]
beq_nat_sym [in UsefulTypes]
beq_list_refl [in list]
betterAbsPElim [in AlphaEqProps]
betterAbsTElim [in AlphaEqProps]
bindersAllvarsSubset [in Term]
bindersDeep_in_allvars [in Term]
bindersSSubstAuxNoCnange [in SubstAux]
bindersSubsetDeep [in Term]
binrel_list_cons [in list]
binrel_list_nil [in list]
bin_rel_list_refl [in list]
bndngPatIndicesValid [in CFGV]
bndngPatIndicesValid2 [in CFGV]
bndngVarsDeepEquivariant [in SwapProps]
bool2_Equi [in UsefulTypes]
bsNthValid [in CFGV]
C
change_bvars_rangewspec [in SSubst]change_bvars_range_spec [in SSubst]
combine_t_iff_proofs_not [in eq_rel]
combine_t_iff_proofs_sum [in eq_rel]
combine_t_iff_proofs_prod [in eq_rel]
combine_t_iff_proofs_t_iff [in eq_rel]
combine_t_iff_proofs_imp [in eq_rel]
combine_cons [in list]
combine_eq [in list]
combine_in_right [in list]
combine_app_app [in list]
combine_nil [in list]
combine_app_eq [in list]
combine_in_left2 [in list]
combine_in_left [in list]
comp_ind_type [in UsefulTypes]
comp_ind [in UsefulTypes]
constantMapEq [in UsefulTypes]
cons_inj [in list]
cons_snoc [in list]
cons_app [in list]
cons_eq [in list]
cons_as_app [in list]
cons_subset [in list]
CType_S [in eq_rel]
D
decidable_prod [in UsefulTypes]decideAbsP [in AlphaDecider]
decideAbsT [in AlphaDecider]
dec_disjoint [in list]
dep_pair_eq [in UsefulTypes]
DeqDeqp [in UsefulTypes]
deqGSym [in CFGV]
deqMixP [in CFGV]
deqSigTSemType [in CFGV]
deqSigVType [in CFGV]
DeqSym [in UsefulTypes]
DeqTrue [in UsefulTypes]
DeqVtype [in CFGV]
deq_nvar [in variables]
deq_prod [in UsefulTypes]
deq_list [in list]
diffSameNil [in list]
diff_cons_r_ni [in list]
diff_cons_r [in list]
diff_dup2 [in list]
diff_dup [in list]
diff_move [in list]
diff_repeat [in list]
diff_app_l [in list]
diff_app_r [in list]
diff_comm [in list]
diff_remove [in list]
diff_nil [in list]
disjointDeepShallowPlusAlready [in Term]
DisjointEquivariant [in SwapProps]
DisjointEquivariantRev [in SwapProps]
disjointSwapLVar [in SwapProps]
disjoint_remove_nvars2 [in variables]
disjoint_remove_nvars [in variables]
disjoint_remove_nvars_l [in variables]
disjoint_flatten_tl [in SubstAux]
disjoint_app_lr [in list]
disjoint_diff_l [in list]
disjoint_remove_l [in list]
disjoint_flat_map_r [in list]
disjoint_flat_map_l [in list]
disjoint_app_r [in list]
disjoint_app_l [in list]
disjoint_singleton_r [in list]
disjoint_singleton_l [in list]
disjoint_snoc_l [in list]
disjoint_snoc_r [in list]
disjoint_iff_diff [in list]
disjoint_cons_l [in list]
disjoint_cons_r [in list]
disjoint_sym [in list]
disjoint_sym_impl [in list]
disjoint_nil_l_iff [in list]
disjoint_nil_l [in list]
disjoint_nil_r_iff [in list]
disjoint_nil_r [in list]
dmemvar [in variables]
dont_touch_forall3 [in eq_rel]
dont_touch_forall2 [in eq_rel]
dont_touch_forall [in eq_rel]
dup_lemma [in LibTactics]
E
eqsetCommute [in list]eqsetCommute3 [in list]
eqSetDeepShallowPlusAlready [in Term]
eqsetSubset [in list]
eqset_subtractv_if_right [in AlphaEqProps]
eqset_subtractv_if_left [in AlphaEqProps]
eqset_sym [in list]
eqset_trans [in list]
eqset_diff_if_right [in list]
eqset_diff_if_left [in list]
eqset_app_if [in list]
eqset_same [in list]
equipollent_Deq [in UsefulTypes]
EquivariantSSubstAux [in SubstAuxAlphaEq]
eqvars_remove_nvars_implies [in variables]
eqvars_cons_lr [in variables]
eqvars_disjoint_r [in variables]
eqvars_app [in variables]
eqvars_remove_nvars [in variables]
eqvars_trans [in variables]
eqvars_nil [in variables]
eqvars_refl [in variables]
eqvars_remove_nvar [in variables]
eqvars_cons_l_iff [in variables]
eqvars_disjoint [in variables]
eqvars_sym [in variables]
eqvars_prop [in variables]
eq_var_iff [in variables]
eq_vars_sym [in variables]
eq_vars_nil [in variables]
eq_var_dec [in variables]
eq_subtractv [in AlphaEqProps]
eq_subtractv_if_right [in AlphaEqProps]
eq_subtractv_if_left [in AlphaEqProps]
eq_snoc [in list]
eq_cons [in list]
eq_gmapds [in list]
eq_gmaps [in list]
eq_maps2 [in list]
eq_set_empty [in list]
eq_set_refl2 [in list]
eq_set_refl [in list]
eq_set_iff_eq_set2 [in list]
eq_list2 [in list]
eq_list [in list]
eq_maps [in list]
eq_flat_maps [in list]
eq_lists [in list]
ex_fresh_var [in variables]
F
false_in_combine_repeat [in list]FilterLIn [in list]
filter_app [in list]
filter_snoc [in list]
Finite_Deq [in UsefulTypes]
Fin_decidable [in UsefulTypes]
Fin_eq [in UsefulTypes]
firstn_nil [in list]
first_index [in list]
flat_map_snoc [in list]
flat_map_app [in list]
flat_map_as_appl_map [in list]
flat_map_map [in list]
flat_map_empty [in list]
fold_assert [in UsefulTypes]
fold_subset [in list]
forall_num_lt_d [in UsefulTypes]
freevarsEquivariant [in SwapProps]
freeVarsSupp [in AlphaEqProps]
freeVarsSuppAux [in AlphaEqProps]
freeVarsSuppAux2 [in AlphaEqProps]
freevars_in_allvars [in AlphaEqProps]
freevars_swap_eq [in AlphaEqProps]
free_vars_SSubstAux [in SubstAux]
FreshDistRenSpec [in GVariables]
FreshDistRenWSpec [in GVariables]
FreshDistVarsSpec [in CFGV]
FreshDistVarsSpec [in GVariables]
freshStringAuxSpec [in GVariables]
freshStringSpec [in GVariables]
fresh_vars [in variables]
fresh_distinct_vars_spec1 [in variables]
fresh_distinct_vars_spec [in variables]
fresh_var_nil [in variables]
fresh_var_nvarx [in variables]
fresh_var_aux_0 [in variables]
fresh_var_not_in [in variables]
fresh_var_aux_sorted_not_in [in variables]
fresh_var_aux_le [in variables]
fst_split_as_map [in list]
FVSSubst [in SSubst]
G
GAlphaInd [in AlphaEquality]getBVarsNthRange [in Term]
getBVarsNthRangeContra [in Term]
getBVarsNth_swap [in SwapProps]
GFreshDistRenWSpec [in CFGV]
GInductionS [in Term]
gmap [in list]
gmap_eq_d [in list]
gmap_length [in list]
H
hide_hyp [in tactics]I
iff_push_down_impliesT [in UsefulTypes]iff_push_down_forallT [in UsefulTypes]
iff_push_down_forall [in UsefulTypes]
iff_intro_swap [in LibTactics]
iff_symm [in tactics]
implies_lforall [in list]
implies_in_combine [in list]
injection_surjection_equipollent [in UsefulTypes]
injective_fun_swapVar [in SwapProps]
injRightsigT [in UsefulTypes]
insert_in [in variables]
intersect_vars [in variables]
intersect_single_l [in list]
intersect_nil_l [in list]
intersect_cons_l [in list]
in_insert [in variables]
in_remove_nvar [in variables]
in_remove_nvars [in variables]
in_nvar_list_dec [in variables]
in_ALRange_ALFilter_implies [in SubstAux]
in_cons_iff [in list]
in_cons_if [in list]
in_cons_left [in list]
in_combine_right_eauto [in list]
in_combine_left_eauto [in list]
in_nth3 [in list]
in_single_iff [in list]
in_combine_repeat [in list]
in_firstn [in list]
in_repeat [in list]
in_combine [in list]
in_list1_elim [in list]
in_list1 [in list]
in_list2_elim [in list]
in_list2 [in list]
in_single [in list]
in_deq_t [in list]
in_deq [in list]
in_subset [in list]
in_snoc [in list]
in_nth [in list]
in_app_deq [in list]
in_map_iff [in list]
in_app_iff [in list]
in_diff [in list]
in_remove [in list]
isReflSwapping_cons [in SwapProps]
is_first_index_unique [in list]
L
last_snoc [in list]lBoundVarsLength [in Term]
lBoundVarsLenSameifNth [in Term]
lBoundVarsmBndngVars [in Term]
lBoundVarsSameifNth [in Term]
lBoundVarsSameSSubstAux [in SubstAux]
lBoundVars_equivariant [in SwapProps]
lBoundVars_swap [in SwapProps]
lbShallowNoChange [in AlphaRen]
leavesLVarUnchanged1 [in SwapProps]
left_id_injection [in UsefulTypes]
lengthAppendStr [in GVariables]
length_pRhsAugIsPat [in CFGV]
length_combine_eq [in list]
length_filter [in list]
length_app [in list]
length_snoc [in list]
length0 [in list]
length1 [in list]
length2 [in list]
length3 [in list]
length4 [in list]
len_flat_map [in list]
le_binrel_list_un [in list]
lforallApp [in list]
lForallSame [in list]
lheadEquivariant [in SwapProps]
lift_bin_rel_ifdp [in bin_rels]
lift_bin_rel_if [in bin_rels]
LInEquivariant [in SwapProps]
LInSeqIff [in list]
Lin_eauto2 [in list]
Lin_eauto1 [in list]
lin_lift [in list]
lin_flat_map [in list]
lKeepDisjoint [in list]
lKeepSubset [in list]
lmaxSpec [in GVariables]
lmaxSpecLen [in GVariables]
ltac_database_provide [in LibTactics]
ltac_something_show [in tactics]
ltac_something_hide [in tactics]
ltac_something_eq [in tactics]
M
MakeAbsPNodeCommute [in AlphaEquality]MakeAbsPnodeSame [in AlphaEqProps]
MakeAbsTNodeCommute [in AlphaEquality]
MakeLAbsSwapCommute [in AlphaEquality]
MakeLAbsSwapCommute [in AlphaRen]
map_length [in GVariables]
map_firstn [in list]
map_cons [in list]
map_diff_commute [in list]
map_remove_commute [in list]
map_eq_injective [in list]
map_gmap_eq [in list]
map_eq_length_eq [in list]
map_combine [in list]
map_snoc [in list]
map_map [in list]
map_flat_map [in list]
maxl_prop [in list]
max_or [in UsefulTypes]
max_prop2 [in UsefulTypes]
max_prop1 [in UsefulTypes]
mBndngVarsAsNth [in Term]
mBndngVarsSameIfNth [in Term]
mBndngVarsShallowSame [in AlphaRen]
memberb_din [in list]
memberb_app [in list]
memvar_dmemvar [in variables]
memvar_singleton_diff_r [in variables]
memvar_singleton [in variables]
memvar_app [in variables]
minus0 [in UsefulTypes]
min_eq [in UsefulTypes]
MixMapLength [in Term]
mLSwapTermEmbedSameBinders [in AlphaRen]
mLSwapTermEmbedSameLBV [in AlphaRen]
mLSwapTermEmbedSameNthBinder [in AlphaRen]
monotoneFilter [in list]
monotoneSetFnFlatMap [in list]
monotoneSetFnMap [in list]
monotone_eauto [in list]
mRenBindersSpec3 [in AlphaRen]
mRenlBinderShallowSame [in AlphaRen]
N
nat_compare_dec [in list]nat2string [in GVariables]
ndRenAlAxAlpha [in AlphaRen]
ndRenAlAxSpecDisj [in AlphaRen]
ndRenAlAxSpecDisjAux [in AlphaRen]
negb_eq_true [in UsefulTypes]
NegLInEquivariant [in SwapProps]
nil_subset_iff [in list]
nil_subset [in list]
nil_snoc_false [in list]
NoRepeatsEquivariant [in SwapProps]
not_over_not_lin_nvar [in variables]
not_eq_beq_var_false [in variables]
not_false_is_true [in UsefulTypes]
not_over_or [in UsefulTypes]
not_or [in UsefulTypes]
not_of_assert [in UsefulTypes]
not_assert [in UsefulTypes]
not_in_subset [in list]
no_repeats_singleton [in list]
no_repeat_dec [in list]
no_rep_flat_map_seq2 [in list]
no_rep_flat_map_seq1 [in list]
no_repeats_app [in list]
no_repeats_cons [in list]
no_repeats_index_unique2 [in list]
no_repeats_index_unique [in list]
nth_in2 [in list]
nth_select3 [in list]
nth_select2 [in list]
nth_select1 [in list]
nth_in [in list]
nth2 [in list]
nth2_equiv [in list]
nth3 [in list]
null_remove_nvars_subvars [in variables]
null_remove_nvars [in variables]
null_subset [in list]
null_diff_subset [in list]
null_map [in list]
null_app [in list]
null_cons [in list]
null_iff_nil [in list]
null_diff [in list]
null_nil_iff [in list]
null_nil [in list]
O
oneSwapVar_prop_s1 [in SwapProps]or_false_l [in UsefulTypes]
or_false_r [in UsefulTypes]
or_true_r [in UsefulTypes]
or_true_l [in UsefulTypes]
P
pairInProofs [in list]pairInProofsCons [in list]
pair_inj [in UsefulTypes]
pAlphaEqEquivariantRev [in AlphaEqProps]
pAlphaEqTransEauto [in AlphaEqProps]
pAlphaSwapEmSwap [in AlphaEqProps]
PatIndNoEmbed [in Term]
pBndngVars_swap [in SwapProps]
pFreshSubset [in Swap]
pFresh_app [in AlphaEqProps]
pRenBindersAlpha [in AlphaRen]
prod_comm [in UsefulTypes]
prod_assoc [in UsefulTypes]
prod_sym [in tactics]
ptrhs_aux_nonNT [in CFGV]
R
rangeFreeVarsApp [in SubstAux]rangeFreeVarsEquivariant [in SubstAuxAlphaEq]
rangeFreeVarsKeepFirstAppImplies [in SubstAux]
rangeFreeVarsKeepFirstAppL [in SubstAux]
rangeFreeVarsKeepFirstAppR [in SubstAux]
rangeFreeVars_ALFilter_subset [in SubstAux]
rangeFreeVars_cons [in SubstAux]
remove_nvar_comm [in variables]
remove_nvar_insert [in variables]
remove_nvars_eq [in variables]
remove_nvar_cons [in variables]
remove_nvars_cons_r [in variables]
remove_nvars_cons_l_weak [in variables]
remove_nvars_cons [in variables]
remove_nvars_move [in variables]
remove_nvars_dup [in variables]
remove_nvars_comm [in variables]
remove_nvars_flat_map [in variables]
remove_nvars_app_l [in variables]
remove_nvars_app_r [in variables]
remove_nvars_nil_r [in variables]
remove_var_nil [in variables]
remove_nvars_nil_l [in variables]
remove_nvars_unchanged [in variables]
remove_nvar_nil [in variables]
remove_dup [in list]
remove_repeat [in list]
remove_comm [in list]
remove_app [in list]
remove_trivial [in list]
RenAlphaAlpha [in AlphaRen]
RenAlphaAvoid [in AlphaRen]
RenAlphaNoChange [in AlphaRen]
renBindersLBVLenSame [in AlphaRen]
renBindersSameLength [in AlphaRen]
RenBindersSpec [in AlphaRen]
RenBindersSpec2 [in AlphaRen]
RenBindersSpec3 [in AlphaRen]
repeat_length [in list]
revSubest1 [in list]
revSubest2 [in list]
rev_list_ind [in list]
rev_list_dest2 [in list]
rev_list_dest [in list]
rev_list_indT [in list]
S
sdkfd [in Term]select_in [in list]
select_lt [in list]
seq_length [in GVariables]
simple_combine_app_app [in AlphaEqProps]
simpl_fst [in list]
singleton_as_snoc [in list]
singleton_subset [in list]
SizePositive [in Term]
snoc_inj [in list]
snoc_cases [in list]
snoc_append_l [in list]
snoc_append_r [in list]
snoc_as_append [in list]
snoc1 [in list]
some_inj [in list]
sort_issorted [in variables]
sort_eqvars [in variables]
split_cons [in list]
split_eta [in list]
split_length_eq [in list]
SSubstAuxAppAwap [in SubstAux]
SSubstAuxBVarsDisjoint [in SubstAux]
SSubstAuxNestAsApp [in SubstAux]
SSubstAuxNestSwap [in SubstAux]
SSubstAuxNilNoChange [in SubstAux]
SSubstAuxSubFilter [in SubstAux]
SSubstAuxTrivial [in SubstAux]
SSubstFilter [in SSubst]
SSubstFVarsDisjoint [in SSubst]
SSubstNestAsApp [in SSubst]
SSubstNestSwap [in SSubst]
SSubstRespectsAlpha [in SSubst]
SSubstRespectsAlpha1 [in SSubst]
SSubstRespectsAlpha2 [in SSubst]
SSubstSubRespectsAlpha [in SSubst]
StringVar [in GVariables]
subAlphaSameFV [in SubstAuxAlphaEq]
subsetAlbindersDeep [in SubstAuxAlphaEq]
subsetAppEauto [in list]
subsetAppEauto2 [in list]
subsetAppEauto3 [in list]
subsetb_subset [in list]
subsetConsEauto [in list]
subsetFlatMap2Eauto [in list]
subsetSingleFlatMap [in list]
subset_disjoint_r [in list]
subset_app_lr [in list]
subset_eq [in list]
subset_eauto [in list]
subset_singleton_r [in list]
subset_disjointLR [in list]
subset_disjoint [in list]
subset_diff [in list]
subset_flat_map [in list]
subset_cons_l [in list]
subset_snoc_l [in list]
subset_snoc_r [in list]
subset_app [in list]
subset_app_l [in list]
subset_app_r [in list]
subset_cons2 [in list]
subset_cons1 [in list]
subset_cons_nil [in list]
subset_trans [in list]
subset_nil_l_iff [in list]
subset_nil_l [in list]
subset_refl_iff [in list]
subset_refl [in list]
SubstAuxRespectsAlpha [in SubstAuxAlphaEq]
SubstAuxRespectsAlpha2 [in SubstAuxAlphaEq]
SubstFilterDisjAux [in SubstAuxAlphaEq]
SubstSubAsSubstAux [in SSubst]
SubstSubFVarsDisjoint [in SSubst]
subSwapAlpha [in SubstAuxAlphaEq]
subtractv_cons [in Term]
subtractv_disjoint [in Term]
subtractv_disjoint_subset [in Term]
subtractv_app_r [in Term]
subtractv_app_l [in AlphaEqProps]
subtractv_nil_l [in AlphaEqProps]
subtractv_nil [in AlphaEqProps]
subtractv_subset [in SubstAux]
subvars_disjoint_r [in variables]
subvars_disjoint_l [in variables]
subvars_cons_lr [in variables]
subvars_not_in [in variables]
subvars_eqvars [in variables]
subvars_nil_r [in variables]
subvars_cons_r_weak_if_not_in [in variables]
subvars_app_trivial_r [in variables]
subvars_app_trivial_l [in variables]
subvars_trans [in variables]
subvars_swap_r [in variables]
subvars_app_remove_nvars_r [in variables]
subvars_app_l [in variables]
subvars_snoc_weak [in variables]
subvars_nil_l_iff [in variables]
subvars_nil_l [in variables]
subvars_cons_r [in variables]
subvars_cons_l [in variables]
subvars_remove_nvars [in variables]
subvars_flat_map [in variables]
subvars_comm_r [in variables]
subvars_singleton_r [in variables]
subvars_singleton_l [in variables]
subvars_app_weak_l [in variables]
subvars_prop [in variables]
subvars_refl [in variables]
subvars_eq [in variables]
sum_assoc [in UsefulTypes]
sum_sym [in tactics]
swapBndngVarsCommute [in AlphaEquality]
swapCommonBinders [in SwapProps]
swapDisjChain [in SwapProps]
SwapEmbedSameBinders [in SwapProps]
SwapEmbedSpec [in SwapProps]
swapEmbed_prop_s1_aux [in SwapProps]
swapLBoundVarsCommute [in AlphaEquality]
swapLVarApp [in SwapProps]
swapLVarDisjChain [in SwapProps]
swapLVarDisjoint [in SwapProps]
swapLVarDisjoint2 [in SwapProps]
swapLVarNoChange [in SwapProps]
swapLVarRevCancel [in SwapProps]
swapLVarRevNoRep [in SwapProps]
swapLVarSwitch [in SwapProps]
swapLVar_subset [in SwapProps]
swapLVar_subtractv [in SwapProps]
swapLVar_flat_map [in SwapProps]
swapLVar_app [in SwapProps]
swapPreservesSize [in SwapProps]
swapRevNoRep [in SwapProps]
swapSubApp [in SubstAuxAlphaEq]
swapSubFilterCommute [in SubstAuxAlphaEq]
swapSubRevCancel [in SubstAuxAlphaEq]
swapSubRevNoRep [in SubstAuxAlphaEq]
swapSubSwitch [in SubstAuxAlphaEq]
swapSwitch [in SwapProps]
swapVarDisjChain [in SwapProps]
swapVarImplies [in SwapProps]
swapvarImplies2 [in SwapProps]
swapVarIn [in SwapProps]
swapVarInj [in SwapProps]
swapVarInOrEq [in SwapProps]
swapVarInOrEq2 [in SwapProps]
swapVarNoChange [in SwapProps]
swapVarNoChange2 [in SwapProps]
swapVarNonChangeRev [in SwapProps]
swapVarRevNoRep [in SwapProps]
swapVarSwitch [in SwapProps]
swapVar_in [in AlphaEqProps]
swapVar_unchanged [in AlphaEqProps]
swapVar_e1stronger [in SwapProps]
swapVar_s2stronger2 [in SwapProps]
swapVar_s2stronger [in SwapProps]
swapVar_app [in SwapProps]
swapVar_S2app [in SwapProps]
swapVar_S2 [in SwapProps]
swapVar_prop_s1 [in SwapProps]
swap_prop_e1Stronger [in SwapProps]
swap_app [in SwapProps]
swap_prop_s2Stronger [in SwapProps]
swap_prop_s3 [in SwapProps]
swap_prop_s1 [in SwapProps]
swap_prop_s1_aux [in SwapProps]
S_lt_inj [in UsefulTypes]
S_le_inj [in UsefulTypes]
S_inj [in UsefulTypes]
T
tailEquivariant [in SwapProps]tail_subset [in SubstAux]
tAlphaEqDecidable [in AlphaDecider]
tAlphaEqEquivariantRev [in AlphaEqProps]
talphaEqRefl [in AlphaEqProps]
tAlphaEqTransEauto [in AlphaEqProps]
TermIndNoPat [in Term]
tFreshSubset [in Swap]
tFresh_app_l [in AlphaEqProps]
tFresh_app [in AlphaEqProps]
tiff_is_prod_implies2 [in eq_rel]
tiff_is_prod_implies1 [in eq_rel]
tiff_trans [in eq_rel]
tRenWithSpec [in AlphaRen]
trivial_if [in UsefulTypes]
true_eq_nvar [in variables]
tSSubstAuxSubFilter [in SubstAux]
tSSubstAuxSubUnfold [in SubstAux]
tSSubstAux_sub_trivial [in SubstAux]
tSwapBndngVarsDisjoint [in SwapProps]
two_as_app [in list]
TypeC_S [in eq_rel]
t_iff_sym [in eq_rel]
t_iff_refl [in eq_rel]
U
UIPReflDeq [in UsefulTypes]V
ValidIndicesDecidable [in CFGV]vFreshDiffSpec [in CFGV]
vFreshVarSpec [in CFGV]
Constructor Index
A
aCons [in LetrecEx]alAbP [in AlphaEquality]
alAbT [in AlphaEquality]
alembed [in AlphaEquality]
alnode [in AlphaEquality]
alpnode [in AlphaEquality]
alpt [in AlphaEquality]
alpvar [in AlphaEquality]
alt [in AlphaEquality]
alv [in AlphaEquality]
aNil [in LetrecEx]
app [in LetrecEx]
asgn [in LetrecEx]
asgnP [in LetrecEx]
asgnRhs [in LetrecEx]
asgnRhsE [in LetrecEx]
B
boxer [in LibTactics]C
cast [in eq_rel]cast2 [in eq_rel]
E
embed [in Term]G
gsymPN [in CFGV]gsymT [in CFGV]
gsymTN [in CFGV]
gsymV [in CFGV]
I
issorted_cons [in variables]issorted_nil [in variables]
L
lAlAbsCons [in AlphaEquality]lAlAbsNil [in AlphaEquality]
lam [in LetrecEx]
lasgn [in LetrecEx]
letr [in LetrecEx]
ltac_mark [in LibTactics]
ltac_wilds [in LibTactics]
ltac_wild [in LibTactics]
ltac_no_arg [in LibTactics]
M
mnil [in Term]mpcons [in Term]
mtcons [in Term]
N
no_rep_cons [in list]no_rep_nil [in list]
nvar [in variables]
P
patAbs [in AlphaEquality]pnode [in Term]
ptleaf [in Term]
pvleaf [in Term]
T
term [in LetrecEx]termAbs [in AlphaEquality]
tleaf [in Term]
tnode [in Term]
t_iff_cons [in eq_rel]
V
vleaf [in Term]vsym [in LetrecEx]
Inductive Index
A
Abstraction [in AlphaEquality]AlphaEqAbs [in AlphaEquality]
B
Boxer [in LibTactics]C
Cast [in eq_rel]Cast2 [in eq_rel]
E
EmbedProd [in LetrecEx]G
GSym [in CFGV]I
issorted [in variables]L
lAlphaEqAbs [in AlphaEquality]ltac_Mark [in LibTactics]
ltac_Wilds [in LibTactics]
ltac_Wild [in LibTactics]
ltac_No_arg [in LibTactics]
M
Mixture [in Term]N
no_repeats [in list]NVar [in variables]
P
pAlphaEq [in AlphaEquality]PatProd [in LetrecEx]
Pattern [in Term]
PNonTerminal [in LetrecEx]
T
tAlphaEq [in AlphaEquality]Term [in Term]
Terminal [in LetrecEx]
TermProd [in LetrecEx]
TNonTerminal [in LetrecEx]
t_iff [in eq_rel]
V
VarSym [in LetrecEx]void [in eq_rel]
Projection Index
B
bindingInfo [in CFGV]bindingInfoCorrect [in CFGV]
D
deqEm [in CFGV]deqNT [in CFGV]
deqPPr [in CFGV]
deqPr [in CFGV]
deqPT [in CFGV]
deqT [in CFGV]
deqTSem [in CFGV]
DeqVarSym [in CFGV]
E
EmbedProd [in CFGV]epLhsRhs [in CFGV]
eqdec [in GVariables]
F
fresh [in GVariables]freshCorrect [in GVariables]
P
PatProd [in CFGV]PNonTerminal [in CFGV]
ppLhsRhs [in CFGV]
T
Terminal [in CFGV]TermProd [in CFGV]
TNonTerminal [in CFGV]
tpLhsRhs [in CFGV]
tSemType [in CFGV]
typ [in GVariables]
V
varSem [in CFGV]VarSym [in CFGV]
vSubstType [in CFGV]
Section Index
A
AlphaProps [in AlphaEqProps]AssociationList [in AssociationList]
G
Gram [in Term]GramVC [in SSubst]
GramVC [in SubstAuxAlphaEq]
GramVC [in AlphaEquality]
GramVC [in SubstAux]
GramVC.SSubstRespectsAlpha [in SSubst]
GramVC.S1Term1Sub [in SSubst]
GramVC.S1Term1Sub1Lv [in SSubst]
GramVC.S1Term2Sub [in SSubst]
S
SwapProps [in SwapProps]Abbreviation Index
D
deq_nat [in UsefulTypes]Dom [in SSubst]
F
filter [in SSubst]fv [in SSubst]
fvr [in SSubst]
I
inll [in LetrecEx]inlr [in LetrecEx]
inrr [in LetrecEx]
K
keepFirst [in SSubst]S
SYMPN [in LetrecEx]SYMTN [in LetrecEx]
V
VAR [in LetrecEx]vcAbstraction [in AlphaEqProps]
vcDeq [in AlphaEquality]
vcType [in AlphaEquality]
vcType [in AlphaEqProps]
vcType [in SwapProps]
Z
zip [in AlphaEquality]Definition Index
A
Abcase [in AlphaEqProps]abindersDeep [in SubstAuxAlphaEq]
addl [in list]
albindersDeep [in SubstAuxAlphaEq]
ALDom [in AssociationList]
ALFilter [in AssociationList]
ALFind [in AssociationList]
ALFindDef [in AssociationList]
ALFindDef2 [in AssociationList]
ALKeepFirst [in AssociationList]
allBndngVars [in Term]
allVarsSub [in SubstAuxAlphaEq]
ALMap [in AssociationList]
ALMapRange [in AssociationList]
ALpcase [in AlphaEqProps]
alphaEqAbsMut [in AlphaEquality]
AlphaEqSubst [in SubstAuxAlphaEq]
ALRange [in AssociationList]
ALRangeRel [in AssociationList]
alSSubstAux [in SubstAuxAlphaEq]
ALSwitch [in AssociationList]
ALtcase [in AlphaEqProps]
appl [in list]
assert [in UsefulTypes]
AssocList [in AssociationList]
aSSubstAux [in SubstAuxAlphaEq]
AvRenaming [in AlphaRen]
B
ball [in list]beq_var [in variables]
beq_list [in list]
bijection [in UsefulTypes]
bindCount [in CFGV]
bindingInfo [in LetrecEx]
bindingSourcesNth [in CFGV]
binrel_list [in list]
bin_rel_and [in bin_rels]
bin_rel [in bin_rels]
bndngPatIndices [in CFGV]
C
change_bvars_range [in SSubst]constantFn [in UsefulTypes]
Csurjection [in UsefulTypes]
c_t_iff [in eq_rel]
D
decDisjointV [in CFGV]decidable [in UsefulTypes]
dec_disjointv [in variables]
Deq [in UsefulTypes]
DeqBool [in UsefulTypes]
DeqP [in UsefulTypes]
Deq2Bool [in UsefulTypes]
diff [in list]
diffEmbedNode [in AlphaDecider]
diffPProdsNode [in AlphaDecider]
diffPVarClasses [in AlphaDecider]
diffTProdsNode [in AlphaDecider]
diffVarClasses [in AlphaDecider]
disjoint [in list]
E
epLhs [in CFGV]epLhsRhs [in LetrecEx]
epRhs [in CFGV]
eqset [in list]
eqsetb [in list]
eqset2 [in list]
equipollent [in UsefulTypes]
EquiVariantFn [in Swap]
EquiVariantFn2 [in Swap]
EquiVariantFn3 [in Swap]
EquiVariantRel [in Swap]
EquiVariantRelSame [in Swap]
EquiVariantRelUn [in Swap]
eqvars [in variables]
eq_vars [in variables]
eq_existsT [in UsefulTypes]
eq_bin_rel [in bin_rels]
eq_set2 [in list]
eq_set [in list]
eq' [in LibTactics]
F
Fin [in UsefulTypes]Finite [in UsefulTypes]
finite [in list]
flatten [in CFGV]
flatten [in list]
freevars_labs [in AlphaEqProps]
freevars_abs [in AlphaEqProps]
FreshDistinctRenamings [in GVariables]
FreshDistinctVars [in GVariables]
freshString [in GVariables]
freshStringAux [in GVariables]
fresh_distinct_vars [in variables]
fresh_var [in variables]
fresh_var_aux [in variables]
G
getBVarsNth [in Term]GFreshVars [in CFGV]
GInduction [in Term]
gmapd [in list]
gsymNotNT [in CFGV]
gsymNotP [in CFGV]
I
In [in list]indep_bin_rel [in bin_rels]
injection [in UsefulTypes]
injective_fun [in UsefulTypes]
insert [in variables]
intersect [in list]
isEmbed [in AlphaDecider]
isInl [in UsefulTypes]
isInlInl [in UsefulTypes]
isInr [in UsefulTypes]
isPNode [in AlphaDecider]
isReflSwapping [in SwapProps]
isVLeaf [in AlphaDecider]
is_greatest_rel_sat [in bin_rels]
is_ge_any_rel_sat [in bin_rels]
is_first_index [in list]
L
LAbcase [in AlphaEqProps]lAlphaEqAbsMut [in AlphaEquality]
lBoundVars [in Term]
lBoundVarsOld [in Term]
leavesLVarUnchanged [in SwapProps]
leavesVarUnchanged [in SwapProps]
left_identity [in UsefulTypes]
letrecCFGV [in LetrecEx]
letr_xyz [in LetrecEx]
le_var [in variables]
le_bin_rel [in bin_rels]
lForall [in list]
lforall [in list]
lhead [in list]
liftInl [in UsefulTypes]
liftNth [in UsefulTypes]
liftPointwise [in list]
liftRelPtwise [in Term]
LIn [in list]
lKeep [in list]
lmax [in GVariables]
ltac_to_generalize [in LibTactics]
ltac_tag_subst [in LibTactics]
ltac_nat_from_int [in LibTactics]
ltac_database [in LibTactics]
ltac_something [in tactics]
lt_var [in variables]
lVars [in AlphaRen]
lvKeep [in Term]
M
MakeAbstractions [in AlphaEquality]MakeAbstractionsPNode [in AlphaEquality]
MakeAbstractionsTNode [in AlphaEquality]
MakeAbstractionsTNodeAux [in AlphaEquality]
mAllButBinders [in Term]
mAllVars [in Term]
mAlphaEq [in AlphaEquality]
mAlreadyBndBinders [in Term]
maxl [in list]
mBndngVars [in Term]
mBndngVarsDeep [in Term]
mcase [in Term]
memberb [in list]
memvar [in variables]
mfreevars [in Term]
mFresh [in Swap]
MixInd [in Term]
MixMap [in Term]
MixtureParam [in CFGV]
mix_mut [in Term]
mkAsgn [in LetrecEx]
mkLAsgn [in LetrecEx]
mkLetr [in LetrecEx]
mkVTerm [in LetrecEx]
mLSwapTermEmbed [in AlphaRen]
monotoneSetFn [in list]
MParamCorrectb [in CFGV]
mRenAlpha [in AlphaRen]
mRenBinders [in AlphaRen]
mSize [in Term]
mSSubstAux [in SubstAux]
mSwap [in Swap]
mSwapEmbed [in Swap]
N
nodeRenAlphaAux [in AlphaRen]not_in_prefix [in list]
null [in list]
nullb [in list]
nvara [in variables]
nvarb [in variables]
nvarc [in variables]
nvard [in variables]
nvarf [in variables]
nvarg [in variables]
nvarh [in variables]
nvari [in variables]
nvarj [in variables]
nvark [in variables]
nvarl [in variables]
nvarVarType [in GVariables]
nvarx [in variables]
nvary [in variables]
nvarz [in variables]
O
oneSwapVar [in Swap]P
pAllButBinders [in Term]pAllVars [in Term]
pAlphaEqG [in AlphaDecider]
pAlphaEqMut [in AlphaEquality]
pAlreadyBndBinders [in Term]
PAT [in LetrecEx]
PatInd [in Term]
PatInMix [in Term]
pat_mut [in Term]
pBndngVars [in Term]
pBndngVarsDeep [in Term]
pcase [in Term]
pfreevars [in Term]
pFresh [in Swap]
ppLhs [in CFGV]
ppLhsRhs [in LetrecEx]
ppRhsSym [in CFGV]
pRenAlpha [in AlphaRen]
pRenBinders [in AlphaRen]
prhsIsBound [in CFGV]
prhs_aux [in CFGV]
pSize [in Term]
pSSubstAux [in SubstAux]
pSwap [in Swap]
pSwapEmbed [in Swap]
ptrhs_aux [in CFGV]
R
rangeFreeVars [in SubstAux]refl_rel [in bin_rels]
removev [in Term]
remove_nvar [in variables]
remove_nvars [in variables]
repeat [in list]
rm [in LibTactics]
S
select [in list]shead [in GVariables]
sigTDeq [in UsefulTypes]
SimplifyForPaper.allBndngVars [in Term]
snoc [in list]
sort [in variables]
SSubstitution [in SubstAux]
SubFilter [in SubstAux]
SubKeepFirst [in SubstAux]
subset [in list]
subsetb [in list]
SubstSub [in SSubst]
subtractv [in Term]
subvars [in variables]
sub_vars [in variables]
swapAbs [in AlphaEquality]
swapEmbedAbs [in AlphaRen]
swapEmbedLAbs [in AlphaRen]
swapLAbs [in AlphaEquality]
swapLLVar [in Swap]
swapLVar [in Swap]
Swapping [in Swap]
swapSub [in SubstAuxAlphaEq]
swapSwap [in Swap]
swapVar [in Swap]
symm_rel [in bin_rels]
T
tAllVars [in Term]tAlphaEqG [in AlphaDecider]
tAlphaEqMut [in AlphaEquality]
tAlphaEqual [in AlphaEquality]
tBndngVarsDeep [in Term]
tcase [in Term]
TERM [in LetrecEx]
TermInd [in Term]
TermInMix [in Term]
term_mut [in Term]
tfreevars [in Term]
tFresh [in Swap]
tiff_snd [in eq_rel]
tiff_fst [in eq_rel]
tpLhs [in CFGV]
tpLhsRhs [in LetrecEx]
tpRhsAugIsPat [in CFGV]
tpRhsSym [in CFGV]
transport [in UsefulTypes]
transRel [in AlphaEqProps]
trans_rel [in bin_rels]
tRenAlpha [in AlphaRen]
tSize [in Term]
tSSubst [in SSubst]
tSSubstAux [in SubstAux]
tSSubstAux_sub [in SubstAux]
tSwap [in Swap]
typeCast [in UsefulTypes]
t_c_iff [in eq_rel]
V
validBsl [in CFGV]ValidIndices [in CFGV]
ValidNthSrc [in CFGV]
VarSubSym [in SubstAux]
vFreshDiff [in CFGV]
vFreshVar [in CFGV]
vSubstType [in LetrecEx]
vType [in CFGV]
Record Index
C
CFGV [in CFGV]V
VarType [in GVariables]| 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 | (1255 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 | (51 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| 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 | (13 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 | (24 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 | (736 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 | (52 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 | (28 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 | (27 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) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (18 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 | (290 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) |
This page has been generated by coqdoc