| 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 | (1383 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 | (41 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 | (40 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 | (16 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 | (277 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 | (705 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 | (38 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 | (46 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 | (14 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 | (13 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 | (180 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 | (13 entries) |
Global Index
A
Abs_Inv [lemma, in DecSyn.admissible]Abs_Pi_Inv [lemma, in DecSyn.algorithmic]
admissible [library]
algorithmic [library]
algor_ind [definition, in DecSyn.common]
algo_dom_neu_neu_nonconf [lemma, in DecSyn.algorithmic]
algo_dom_hf_hne [lemma, in DecSyn.algorithmic]
algo_dom_r_algo_dom [lemma, in DecSyn.common]
algo_dom_salgo_dom [lemma, in DecSyn.common]
algo_dom_sym [lemma, in DecSyn.common]
algo_dom_no_hred [lemma, in DecSyn.common]
algo_dom_r_inv [lemma, in DecSyn.common]
algo_ind [definition, in DecSyn.common]
algo_dom_r_sind [definition, in DecSyn.common]
algo_dom_r_ind [definition, in DecSyn.common]
algo_dom_sind [definition, in DecSyn.common]
algo_dom_ind [definition, in DecSyn.common]
algo_dom_r [inductive, in DecSyn.common]
algo_dom [inductive, in DecSyn.common]
ap [definition, in DecSyn.Autosubst2.unscoped]
apc [definition, in DecSyn.Autosubst2.unscoped]
App_Inv [lemma, in DecSyn.admissible]
A_Conf' [lemma, in DecSyn.algorithmic]
A_HRedR' [lemma, in DecSyn.common]
A_HRedsR [lemma, in DecSyn.common]
A_HRedsL [lemma, in DecSyn.common]
A_HRedR [constructor, in DecSyn.common]
A_HRedL [constructor, in DecSyn.common]
A_NfNf [constructor, in DecSyn.common]
A_Conf [constructor, in DecSyn.common]
A_IndCong [constructor, in DecSyn.common]
A_ProjCong [constructor, in DecSyn.common]
A_AppCong [constructor, in DecSyn.common]
A_VarCong [constructor, in DecSyn.common]
A_NatCong [constructor, in DecSyn.common]
A_BindCong [constructor, in DecSyn.common]
A_UnivCong [constructor, in DecSyn.common]
A_SucSuc [constructor, in DecSyn.common]
A_ZeroZero [constructor, in DecSyn.common]
A_NeuPair [constructor, in DecSyn.common]
A_PairNeu [constructor, in DecSyn.common]
A_PairPair [constructor, in DecSyn.common]
A_NeuAbs [constructor, in DecSyn.common]
A_AbsNeu [constructor, in DecSyn.common]
A_AbsAbs [constructor, in DecSyn.common]
B
BindSpace [definition, in DecSyn.logrel]Bind_Univ_Inv [lemma, in DecSyn.algorithmic]
bind_inst [lemma, in DecSyn.structural]
Bind_Inv [lemma, in DecSyn.structural]
BTag_eq_dec [definition, in DecSyn.executable]
C
ce_neu_neu_helper [lemma, in DecSyn.algorithmic]CE_Nf [lemma, in DecSyn.algorithmic]
CE_HRedR [lemma, in DecSyn.algorithmic]
CE_HRedL [lemma, in DecSyn.algorithmic]
CE_HRed [constructor, in DecSyn.algorithmic]
CE_IndCong [constructor, in DecSyn.algorithmic]
CE_AppCong [constructor, in DecSyn.algorithmic]
CE_ProjCong [constructor, in DecSyn.algorithmic]
CE_VarCong [constructor, in DecSyn.algorithmic]
CE_NeuNeu [constructor, in DecSyn.algorithmic]
CE_NatCong [constructor, in DecSyn.algorithmic]
CE_BindCong [constructor, in DecSyn.algorithmic]
CE_UnivCong [constructor, in DecSyn.algorithmic]
CE_NeuPair [constructor, in DecSyn.algorithmic]
CE_PairNeu [constructor, in DecSyn.algorithmic]
CE_PairPair [constructor, in DecSyn.algorithmic]
CE_NeuAbs [constructor, in DecSyn.algorithmic]
CE_AbsNeu [constructor, in DecSyn.algorithmic]
CE_AbsAbs [constructor, in DecSyn.algorithmic]
CE_SucSuc [constructor, in DecSyn.algorithmic]
CE_ZeroZero [constructor, in DecSyn.algorithmic]
check_sub_hredr [lemma, in DecSyn.executable]
check_sub_hredl [lemma, in DecSyn.executable]
check_sub_irrel [lemma, in DecSyn.executable]
check_sub_conf [lemma, in DecSyn.executable]
check_sub_neuneu [lemma, in DecSyn.executable]
check_sub_nfnf [lemma, in DecSyn.executable]
check_sub_univ_univ [lemma, in DecSyn.executable]
check_sub_sig_sig [lemma, in DecSyn.executable]
check_sub_pi_pi [lemma, in DecSyn.executable]
check_sub_r [definition, in DecSyn.executable]
check_sub [definition, in DecSyn.executable]
check_equal_conf [lemma, in DecSyn.executable]
check_equal_univ [lemma, in DecSyn.executable]
check_equal_hredr [lemma, in DecSyn.executable]
check_equal_ind_ind [lemma, in DecSyn.executable]
check_equal_app_app [lemma, in DecSyn.executable]
check_equal_proj_proj [lemma, in DecSyn.executable]
check_equal_bind_bind [lemma, in DecSyn.executable]
check_equal_neu_pair [lemma, in DecSyn.executable]
check_equal_pair_neu [lemma, in DecSyn.executable]
check_equal_pair_pair [lemma, in DecSyn.executable]
check_equal_neu_abs [lemma, in DecSyn.executable]
check_equal_abs_neu [lemma, in DecSyn.executable]
check_equal_abs_abs [lemma, in DecSyn.executable]
check_equal_hredl [lemma, in DecSyn.executable]
check_equal_irrel [lemma, in DecSyn.executable]
check_equal_nfnf [lemma, in DecSyn.executable]
check_equal_r [definition, in DecSyn.executable]
check_equal [definition, in DecSyn.executable]
check_sub_complete [lemma, in DecSyn.executable_correct]
check_sub_sound [lemma, in DecSyn.executable_correct]
check_equal_complete [lemma, in DecSyn.executable_correct]
check_equal_sound [lemma, in DecSyn.executable_correct]
check_sub_r_wt [definition, in DecSyn.conv_dec]
CLE_HRedR [lemma, in DecSyn.algorithmic]
CLE_HRedL [lemma, in DecSyn.algorithmic]
CLE_HRed [constructor, in DecSyn.algorithmic]
CLE_NeuNeu [constructor, in DecSyn.algorithmic]
CLE_NatCong [constructor, in DecSyn.algorithmic]
CLE_SigCong [constructor, in DecSyn.algorithmic]
CLE_PiCong [constructor, in DecSyn.algorithmic]
CLE_UnivCong [constructor, in DecSyn.algorithmic]
CombineNotations [module, in DecSyn.Autosubst2.unscoped]
_ >> _ (fscope) [notation, in DecSyn.Autosubst2.unscoped]
_ .: _ (subst_scope) [notation, in DecSyn.Autosubst2.unscoped]
common [library]
Conv_dec [lemma, in DecSyn.conv_dec]
conv_dec [library]
CoqEq [inductive, in DecSyn.algorithmic]
coqeqr_no_hred [lemma, in DecSyn.executable_correct]
coqeq_complete [lemma, in DecSyn.algorithmic]
coqeq_sound [lemma, in DecSyn.algorithmic]
coqeq_complete' [lemma, in DecSyn.algorithmic]
coqeq_sound_mutual [lemma, in DecSyn.algorithmic]
coqeq_symmetric_mutual [lemma, in DecSyn.algorithmic]
coqeq_r_ind [definition, in DecSyn.algorithmic]
coqeq_ind [definition, in DecSyn.algorithmic]
coqeq_neu_ind [definition, in DecSyn.algorithmic]
CoqEq_R_sind [definition, in DecSyn.algorithmic]
CoqEq_R_ind [definition, in DecSyn.algorithmic]
CoqEq_Neu_sind [definition, in DecSyn.algorithmic]
CoqEq_Neu_ind [definition, in DecSyn.algorithmic]
CoqEq_sind [definition, in DecSyn.algorithmic]
CoqEq_ind [definition, in DecSyn.algorithmic]
CoqEq_R [inductive, in DecSyn.algorithmic]
CoqEq_Neu [inductive, in DecSyn.algorithmic]
coqeq_neuneu' [lemma, in DecSyn.executable_correct]
coqeq_neuneu [lemma, in DecSyn.executable_correct]
coqeq_no_hred [lemma, in DecSyn.executable_correct]
CoqLEq [inductive, in DecSyn.algorithmic]
coqleq_sound [lemma, in DecSyn.algorithmic]
coqleq_complete [lemma, in DecSyn.algorithmic]
coqleq_complete_unty [lemma, in DecSyn.algorithmic]
coqleq_complete' [lemma, in DecSyn.algorithmic]
coqleq_sound_mutual [lemma, in DecSyn.algorithmic]
coqleq_r_ind [definition, in DecSyn.algorithmic]
coqleq_ind [definition, in DecSyn.algorithmic]
CoqLEq_R_sind [definition, in DecSyn.algorithmic]
CoqLEq_R_ind [definition, in DecSyn.algorithmic]
CoqLEq_sind [definition, in DecSyn.algorithmic]
CoqLEq_ind [definition, in DecSyn.algorithmic]
CoqLEq_R [inductive, in DecSyn.algorithmic]
coqleq_no_hred [lemma, in DecSyn.executable_correct]
Core [module, in DecSyn.Autosubst2.syntax]
core [library]
Core.BTag [inductive, in DecSyn.Autosubst2.syntax]
Core.BTag_sind [definition, in DecSyn.Autosubst2.syntax]
Core.BTag_rec [definition, in DecSyn.Autosubst2.syntax]
Core.BTag_ind [definition, in DecSyn.Autosubst2.syntax]
Core.BTag_rect [definition, in DecSyn.Autosubst2.syntax]
Core.compRenRen_PTm [definition, in DecSyn.Autosubst2.syntax]
Core.compRenSubst_PTm [definition, in DecSyn.Autosubst2.syntax]
Core.compSubstRen_PTm [definition, in DecSyn.Autosubst2.syntax]
Core.compSubstSubst_PTm [definition, in DecSyn.Autosubst2.syntax]
Core.congr_PInd [lemma, in DecSyn.Autosubst2.syntax]
Core.congr_PSuc [lemma, in DecSyn.Autosubst2.syntax]
Core.congr_PZero [lemma, in DecSyn.Autosubst2.syntax]
Core.congr_PNat [lemma, in DecSyn.Autosubst2.syntax]
Core.congr_PUniv [lemma, in DecSyn.Autosubst2.syntax]
Core.congr_PBind [lemma, in DecSyn.Autosubst2.syntax]
Core.congr_PProj [lemma, in DecSyn.Autosubst2.syntax]
Core.congr_PPair [lemma, in DecSyn.Autosubst2.syntax]
Core.congr_PApp [lemma, in DecSyn.Autosubst2.syntax]
Core.congr_PAbs [lemma, in DecSyn.Autosubst2.syntax]
Core.congr_PR [lemma, in DecSyn.Autosubst2.syntax]
Core.congr_PL [lemma, in DecSyn.Autosubst2.syntax]
Core.congr_PSig [lemma, in DecSyn.Autosubst2.syntax]
Core.congr_PPi [lemma, in DecSyn.Autosubst2.syntax]
Core.extRen_PTm [definition, in DecSyn.Autosubst2.syntax]
Core.ext_PTm [definition, in DecSyn.Autosubst2.syntax]
Core.idSubst_PTm [definition, in DecSyn.Autosubst2.syntax]
Core.instId'_PTm_pointwise [lemma, in DecSyn.Autosubst2.syntax]
Core.instId'_PTm [lemma, in DecSyn.Autosubst2.syntax]
Core.PAbs [constructor, in DecSyn.Autosubst2.syntax]
Core.PApp [constructor, in DecSyn.Autosubst2.syntax]
Core.PBind [constructor, in DecSyn.Autosubst2.syntax]
Core.PInd [constructor, in DecSyn.Autosubst2.syntax]
Core.PL [constructor, in DecSyn.Autosubst2.syntax]
Core.PNat [constructor, in DecSyn.Autosubst2.syntax]
Core.PPair [constructor, in DecSyn.Autosubst2.syntax]
Core.PPi [constructor, in DecSyn.Autosubst2.syntax]
Core.PProj [constructor, in DecSyn.Autosubst2.syntax]
Core.PR [constructor, in DecSyn.Autosubst2.syntax]
Core.PSig [constructor, in DecSyn.Autosubst2.syntax]
Core.PSuc [constructor, in DecSyn.Autosubst2.syntax]
Core.PTag [inductive, in DecSyn.Autosubst2.syntax]
Core.PTag_sind [definition, in DecSyn.Autosubst2.syntax]
Core.PTag_rec [definition, in DecSyn.Autosubst2.syntax]
Core.PTag_ind [definition, in DecSyn.Autosubst2.syntax]
Core.PTag_rect [definition, in DecSyn.Autosubst2.syntax]
Core.PTm [inductive, in DecSyn.Autosubst2.syntax]
Core.PTm_sind [definition, in DecSyn.Autosubst2.syntax]
Core.PTm_rec [definition, in DecSyn.Autosubst2.syntax]
Core.PTm_ind [definition, in DecSyn.Autosubst2.syntax]
Core.PTm_rect [definition, in DecSyn.Autosubst2.syntax]
Core.PUniv [constructor, in DecSyn.Autosubst2.syntax]
Core.PZero [constructor, in DecSyn.Autosubst2.syntax]
Core.renRen_PTm [lemma, in DecSyn.Autosubst2.syntax]
Core.renRen'_PTm_pointwise [lemma, in DecSyn.Autosubst2.syntax]
Core.renSubst_PTm_pointwise [lemma, in DecSyn.Autosubst2.syntax]
Core.renSubst_PTm [lemma, in DecSyn.Autosubst2.syntax]
Core.ren_PTm_morphism2 [instance, in DecSyn.Autosubst2.syntax]
Core.ren_PTm_morphism [instance, in DecSyn.Autosubst2.syntax]
Core.Ren_PTm [instance, in DecSyn.Autosubst2.syntax]
Core.ren_PTm [definition, in DecSyn.Autosubst2.syntax]
Core.rinstId'_PTm_pointwise [lemma, in DecSyn.Autosubst2.syntax]
Core.rinstId'_PTm [lemma, in DecSyn.Autosubst2.syntax]
Core.rinstInst_up_PTm_PTm [lemma, in DecSyn.Autosubst2.syntax]
Core.rinstInst'_PTm_pointwise [lemma, in DecSyn.Autosubst2.syntax]
Core.rinstInst'_PTm [lemma, in DecSyn.Autosubst2.syntax]
Core.rinst_inst_PTm [definition, in DecSyn.Autosubst2.syntax]
Core.substRen_PTm_pointwise [lemma, in DecSyn.Autosubst2.syntax]
Core.substRen_PTm [lemma, in DecSyn.Autosubst2.syntax]
Core.substSubst_PTm_pointwise [lemma, in DecSyn.Autosubst2.syntax]
Core.substSubst_PTm [lemma, in DecSyn.Autosubst2.syntax]
Core.subst_PTm_morphism2 [instance, in DecSyn.Autosubst2.syntax]
Core.subst_PTm_morphism [instance, in DecSyn.Autosubst2.syntax]
Core.Subst_PTm [instance, in DecSyn.Autosubst2.syntax]
Core.subst_PTm [definition, in DecSyn.Autosubst2.syntax]
Core.upExtRen_PTm_PTm [lemma, in DecSyn.Autosubst2.syntax]
Core.upExt_PTm_PTm [lemma, in DecSyn.Autosubst2.syntax]
Core.upId_PTm_PTm [lemma, in DecSyn.Autosubst2.syntax]
Core.upRen_PTm_PTm [lemma, in DecSyn.Autosubst2.syntax]
Core.Up_PTm_PTm [instance, in DecSyn.Autosubst2.syntax]
Core.up_PTm [projection, in DecSyn.Autosubst2.syntax]
Core.Up_PTm [record, in DecSyn.Autosubst2.syntax]
Core.up_PTm [constructor, in DecSyn.Autosubst2.syntax]
Core.Up_PTm [inductive, in DecSyn.Autosubst2.syntax]
Core.up_subst_subst_PTm_PTm [lemma, in DecSyn.Autosubst2.syntax]
Core.up_subst_ren_PTm_PTm [lemma, in DecSyn.Autosubst2.syntax]
Core.up_ren_subst_PTm_PTm [lemma, in DecSyn.Autosubst2.syntax]
Core.up_ren_ren_PTm_PTm [lemma, in DecSyn.Autosubst2.syntax]
Core.up_PTm_PTm [lemma, in DecSyn.Autosubst2.syntax]
Core.VarInstance_PTm [instance, in DecSyn.Autosubst2.syntax]
Core.varLRen'_PTm_pointwise [lemma, in DecSyn.Autosubst2.syntax]
Core.varLRen'_PTm [lemma, in DecSyn.Autosubst2.syntax]
Core.varL'_PTm_pointwise [lemma, in DecSyn.Autosubst2.syntax]
Core.varL'_PTm [lemma, in DecSyn.Autosubst2.syntax]
Core.VarPTm [constructor, in DecSyn.Autosubst2.syntax]
[ _ ] (fscope) [notation, in DecSyn.Autosubst2.syntax]
⟨ _ ⟩ (fscope) [notation, in DecSyn.Autosubst2.syntax]
_ __PTm (subst_scope) [notation, in DecSyn.Autosubst2.syntax]
_ __PTm (subst_scope) [notation, in DecSyn.Autosubst2.syntax]
var (subst_scope) [notation, in DecSyn.Autosubst2.syntax]
_ ⟨ _ ⟩ (subst_scope) [notation, in DecSyn.Autosubst2.syntax]
↑__PTm (subst_scope) [notation, in DecSyn.Autosubst2.syntax]
↑__PTm (subst_scope) [notation, in DecSyn.Autosubst2.syntax]
_ [ _ ] (subst_scope) [notation, in DecSyn.Autosubst2.syntax]
cosn [library]
CR [definition, in DecSyn.logrel]
ctx_eq_subst_one [lemma, in DecSyn.structural]
Cumulativity [lemma, in DecSyn.structural]
D
DJoin [module, in DecSyn.fp_red]DJoin.AbsCong [lemma, in DecSyn.fp_red]
DJoin.abs_inj [lemma, in DecSyn.fp_red]
DJoin.AppCong [lemma, in DecSyn.fp_red]
DJoin.BindCong [lemma, in DecSyn.fp_red]
DJoin.bind_inj [lemma, in DecSyn.fp_red]
DJoin.bind_univ_noconf [lemma, in DecSyn.fp_red]
DJoin.cong [lemma, in DecSyn.fp_red]
DJoin.cong' [lemma, in DecSyn.fp_red]
DJoin.ejoin_abs_inj [lemma, in DecSyn.fp_red]
DJoin.ejoin_pair_inj [lemma, in DecSyn.fp_red]
DJoin.FromEJoin [lemma, in DecSyn.fp_red]
DJoin.FromRedSNs [lemma, in DecSyn.fp_red]
DJoin.FromRReds [lemma, in DecSyn.fp_red]
DJoin.FromRRed0 [lemma, in DecSyn.fp_red]
DJoin.FromRRed1 [lemma, in DecSyn.fp_red]
DJoin.hne_proj_inj [lemma, in DecSyn.fp_red]
DJoin.hne_app_inj [lemma, in DecSyn.fp_red]
DJoin.hne_nat_noconf [lemma, in DecSyn.fp_red]
DJoin.hne_bind_noconf [lemma, in DecSyn.fp_red]
DJoin.hne_univ_noconf [lemma, in DecSyn.fp_red]
DJoin.IndCong [lemma, in DecSyn.fp_red]
DJoin.PairCong [lemma, in DecSyn.fp_red]
DJoin.pair_inj [lemma, in DecSyn.fp_red]
DJoin.ProjCong [lemma, in DecSyn.fp_red]
DJoin.R [definition, in DecSyn.fp_red]
DJoin.refl [lemma, in DecSyn.fp_red]
DJoin.renaming [lemma, in DecSyn.fp_red]
DJoin.sne_univ_noconf [lemma, in DecSyn.fp_red]
DJoin.sne_bind_noconf [lemma, in DecSyn.fp_red]
DJoin.sne_nat_noconf [lemma, in DecSyn.fp_red]
DJoin.standardization [lemma, in DecSyn.fp_red]
DJoin.standardization_lo [lemma, in DecSyn.fp_red]
DJoin.substing [lemma, in DecSyn.fp_red]
DJoin.SucCong [lemma, in DecSyn.fp_red]
DJoin.suc_inj [lemma, in DecSyn.fp_red]
DJoin.symmetric [lemma, in DecSyn.fp_red]
DJoin.ToEJoin [lemma, in DecSyn.fp_red]
DJoin.transitive [lemma, in DecSyn.fp_red]
DJoin.univ_inj [lemma, in DecSyn.fp_red]
DJoin.var_inj [lemma, in DecSyn.fp_red]
DJoin.weakening [lemma, in DecSyn.fp_red]
E
EJoin [module, in DecSyn.fp_red]EJoin.bind_inj [lemma, in DecSyn.fp_red]
EJoin.hne_proj_inj [lemma, in DecSyn.fp_red]
EJoin.hne_app_inj [lemma, in DecSyn.fp_red]
EJoin.ind_inj [lemma, in DecSyn.fp_red]
EJoin.R [definition, in DecSyn.fp_red]
EJoin.suc_inj [lemma, in DecSyn.fp_red]
EPar [module, in DecSyn.fp_red]
epar_sn_preservation [lemma, in DecSyn.fp_red]
EPar.AbsCong [constructor, in DecSyn.fp_red]
EPar.AppCong [constructor, in DecSyn.fp_red]
EPar.AppEta [constructor, in DecSyn.fp_red]
EPar.AppEta' [lemma, in DecSyn.fp_red]
EPar.BindCong [constructor, in DecSyn.fp_red]
EPar.IndCong [constructor, in DecSyn.fp_red]
EPar.morphing [lemma, in DecSyn.fp_red]
EPar.morphing_up [lemma, in DecSyn.fp_red]
EPar.morphing_ext [lemma, in DecSyn.fp_red]
EPar.morphing_ren [lemma, in DecSyn.fp_red]
EPar.NatCong [constructor, in DecSyn.fp_red]
EPar.PairCong [constructor, in DecSyn.fp_red]
EPar.PairEta [constructor, in DecSyn.fp_red]
EPar.ProjCong [constructor, in DecSyn.fp_red]
EPar.R [inductive, in DecSyn.fp_red]
EPar.refl [lemma, in DecSyn.fp_red]
EPar.renaming [lemma, in DecSyn.fp_red]
EPar.R_sind [definition, in DecSyn.fp_red]
EPar.R_ind [definition, in DecSyn.fp_red]
EPar.substing [lemma, in DecSyn.fp_red]
EPar.SucCong [constructor, in DecSyn.fp_red]
EPar.Univ [constructor, in DecSyn.fp_red]
EPar.VarTm [constructor, in DecSyn.fp_red]
EPar.ZeroCong [constructor, in DecSyn.fp_red]
Eq [inductive, in DecSyn.typing]
eq_ind [definition, in DecSyn.typing]
Eq_sind [definition, in DecSyn.typing]
Eq_ind [definition, in DecSyn.typing]
ERed [module, in DecSyn.fp_red]
EReds [module, in DecSyn.fp_red]
EReds.AbsCong [lemma, in DecSyn.fp_red]
EReds.AppCong [lemma, in DecSyn.fp_red]
EReds.app_inv [lemma, in DecSyn.fp_red]
EReds.BindCong [lemma, in DecSyn.fp_red]
EReds.bind_inv [lemma, in DecSyn.fp_red]
EReds.FromEPar [lemma, in DecSyn.fp_red]
EReds.FromEPars [lemma, in DecSyn.fp_red]
EReds.IndCong [lemma, in DecSyn.fp_red]
EReds.ind_inv [lemma, in DecSyn.fp_red]
EReds.PairCong [lemma, in DecSyn.fp_red]
EReds.ProjCong [lemma, in DecSyn.fp_red]
EReds.proj_inv [lemma, in DecSyn.fp_red]
EReds.renaming [lemma, in DecSyn.fp_red]
EReds.substing [lemma, in DecSyn.fp_red]
EReds.SucCong [lemma, in DecSyn.fp_red]
EReds.suc_inv [lemma, in DecSyn.fp_red]
EReds.zero_inv [lemma, in DecSyn.fp_red]
ered_confluence [lemma, in DecSyn.fp_red]
ered_local_confluence [lemma, in DecSyn.fp_red]
ered_sn [lemma, in DecSyn.fp_red]
ered_size [lemma, in DecSyn.fp_red]
ERed.AbsCong [constructor, in DecSyn.fp_red]
ERed.abs_back_preservation [lemma, in DecSyn.fp_red]
ERed.antirenaming [lemma, in DecSyn.fp_red]
ERed.AppCong0 [constructor, in DecSyn.fp_red]
ERed.AppCong1 [constructor, in DecSyn.fp_red]
ERed.AppEta [constructor, in DecSyn.fp_red]
ERed.AppEta' [lemma, in DecSyn.fp_red]
ERed.BindCong0 [constructor, in DecSyn.fp_red]
ERed.BindCong1 [constructor, in DecSyn.fp_red]
ERed.IndCong0 [constructor, in DecSyn.fp_red]
ERed.IndCong1 [constructor, in DecSyn.fp_red]
ERed.IndCong2 [constructor, in DecSyn.fp_red]
ERed.IndCong3 [constructor, in DecSyn.fp_red]
ERed.nf_preservation [lemma, in DecSyn.fp_red]
ERed.PairCong0 [constructor, in DecSyn.fp_red]
ERed.PairCong1 [constructor, in DecSyn.fp_red]
ERed.PairEta [constructor, in DecSyn.fp_red]
ERed.ProjCong [constructor, in DecSyn.fp_red]
ERed.R [inductive, in DecSyn.fp_red]
ERed.renaming [lemma, in DecSyn.fp_red]
ERed.R_sind [definition, in DecSyn.fp_red]
ERed.R_ind [definition, in DecSyn.fp_red]
ERed.substing [lemma, in DecSyn.fp_red]
ERed.subst_differ_one_ren_up [lemma, in DecSyn.fp_red]
ERed.SucCong [constructor, in DecSyn.fp_red]
ERed.tm_free_ren_any [lemma, in DecSyn.fp_red]
ERed.tm_i_free [definition, in DecSyn.fp_red]
ERed.ToEPar [lemma, in DecSyn.fp_red]
ESub [module, in DecSyn.fp_red]
ESub.pi_inj [lemma, in DecSyn.fp_red]
ESub.R [definition, in DecSyn.fp_red]
ESub.sig_inj [lemma, in DecSyn.fp_red]
ESub.suc_inj [lemma, in DecSyn.fp_red]
executable [library]
executable_correct [library]
Extra [module, in DecSyn.Autosubst2.syntax]
E_PairExt [constructor, in DecSyn.typing]
E_FunExt [constructor, in DecSyn.typing]
E_IndSuc [constructor, in DecSyn.typing]
E_IndZero [constructor, in DecSyn.typing]
E_ProjPair2 [constructor, in DecSyn.typing]
E_ProjPair1 [constructor, in DecSyn.typing]
E_AppAbs [constructor, in DecSyn.typing]
E_Conv [constructor, in DecSyn.typing]
E_SucCong [constructor, in DecSyn.typing]
E_IndCong [constructor, in DecSyn.typing]
E_Proj2 [constructor, in DecSyn.typing]
E_Proj1 [constructor, in DecSyn.typing]
E_App [constructor, in DecSyn.typing]
E_Bind [constructor, in DecSyn.typing]
E_Transitive [constructor, in DecSyn.typing]
E_Symmetric [constructor, in DecSyn.typing]
E_Refl [constructor, in DecSyn.typing]
E_PairEta [lemma, in DecSyn.admissible]
E_ProjPair2 [lemma, in DecSyn.admissible]
E_ProjPair1 [lemma, in DecSyn.admissible]
E_AppEta [lemma, in DecSyn.admissible]
E_PairExt [lemma, in DecSyn.admissible]
E_FunExt [lemma, in DecSyn.admissible]
E_Proj2 [lemma, in DecSyn.admissible]
E_App [lemma, in DecSyn.admissible]
E_Bind [lemma, in DecSyn.admissible]
E_AppAbs [lemma, in DecSyn.admissible]
E_Pair [lemma, in DecSyn.preservation]
E_Abs [lemma, in DecSyn.preservation]
E_Conv_E [lemma, in DecSyn.algorithmic]
E_IndSuc' [lemma, in DecSyn.structural]
E_IndZero' [lemma, in DecSyn.structural]
E_ProjPair2' [lemma, in DecSyn.structural]
E_AppAbs' [lemma, in DecSyn.structural]
E_App' [lemma, in DecSyn.structural]
E_Bind' [lemma, in DecSyn.structural]
E_Proj2' [lemma, in DecSyn.structural]
E_IndCong' [lemma, in DecSyn.structural]
F
fancy_hred [definition, in DecSyn.common]fp_red [library]
funcomp [definition, in DecSyn.Autosubst2.core]
funcomp_morphism2 [instance, in DecSyn.Autosubst2.core]
funcomp_morphism [instance, in DecSyn.Autosubst2.core]
funcomp_assoc [lemma, in DecSyn.Autosubst2.core]
fundamental_theorem [lemma, in DecSyn.soundness]
H
here [constructor, in DecSyn.common]here' [lemma, in DecSyn.common]
hf_not_hne [lemma, in DecSyn.algorithmic]
hf_hred_lored [lemma, in DecSyn.algorithmic]
hf_no_hred [lemma, in DecSyn.common]
hne_ind_inj [lemma, in DecSyn.algorithmic]
hne_nf_ne [lemma, in DecSyn.algorithmic]
hne_no_hred [lemma, in DecSyn.common]
HRed [module, in DecSyn.algorithmic]
hred [definition, in DecSyn.common]
HRed [module, in DecSyn.common]
HReds [module, in DecSyn.algorithmic]
hreds_nf_refl [lemma, in DecSyn.common]
HReds.preservation [lemma, in DecSyn.algorithmic]
HReds.ToEq [lemma, in DecSyn.algorithmic]
hred_none [lemma, in DecSyn.executable]
hred_hne [lemma, in DecSyn.algorithmic]
hred_deter [lemma, in DecSyn.common]
hred_sound [lemma, in DecSyn.common]
hred_complete [lemma, in DecSyn.common]
HRed.AppAbs [constructor, in DecSyn.common]
HRed.AppCong [constructor, in DecSyn.common]
HRed.IndCong [constructor, in DecSyn.common]
HRed.IndSuc [constructor, in DecSyn.common]
HRed.IndZero [constructor, in DecSyn.common]
HRed.nf [definition, in DecSyn.common]
HRed.preservation [lemma, in DecSyn.algorithmic]
HRed.ProjCong [constructor, in DecSyn.common]
HRed.ProjPair [constructor, in DecSyn.common]
HRed.R [inductive, in DecSyn.common]
HRed.R_sind [definition, in DecSyn.common]
HRed.R_ind [definition, in DecSyn.common]
HRed.ToEq [lemma, in DecSyn.algorithmic]
HRed.ToRRed [lemma, in DecSyn.algorithmic]
I
id [definition, in DecSyn.Autosubst2.unscoped]ids [projection, in DecSyn.Autosubst2.unscoped]
ids [constructor, in DecSyn.Autosubst2.unscoped]
idsRen [instance, in DecSyn.Autosubst2.unscoped]
Ind_Inv [lemma, in DecSyn.preservation]
ind_motive_okay [definition, in DecSyn.logrel]
interface [module, in DecSyn.Autosubst2.syntax]
isabs [definition, in DecSyn.common]
isabs_ren [definition, in DecSyn.common]
isbind [definition, in DecSyn.common]
ishf [definition, in DecSyn.common]
ishf_ren [definition, in DecSyn.common]
ishne [definition, in DecSyn.common]
ishne_ren [definition, in DecSyn.common]
isnat [definition, in DecSyn.common]
ispair [definition, in DecSyn.common]
ispair_ren [definition, in DecSyn.common]
issuc [definition, in DecSyn.common]
isuniv [definition, in DecSyn.common]
iszero [definition, in DecSyn.common]
L
LEq [inductive, in DecSyn.typing]LEq_sind [definition, in DecSyn.typing]
LEq_ind [definition, in DecSyn.typing]
le_ind [definition, in DecSyn.typing]
list_comp [definition, in DecSyn.Autosubst2.core]
list_id [definition, in DecSyn.Autosubst2.core]
list_ext [definition, in DecSyn.Autosubst2.core]
LogRel [module, in DecSyn.logrel]
logrel [library]
LogRelFacts [module, in DecSyn.logrel]
LogRelFactsImpl [module, in DecSyn.logrel]
LogRelFactsImpl.adequacy [lemma, in DecSyn.logrel]
LogRelFactsImpl.back_closs [lemma, in DecSyn.logrel]
LogRelFactsImpl.back_clos [lemma, in DecSyn.logrel]
LogRelFactsImpl.bindspace_impl [lemma, in DecSyn.logrel]
LogRelFactsImpl.Bind_nopf [lemma, in DecSyn.logrel]
LogRelFactsImpl.Bind_inv_nopf [lemma, in DecSyn.logrel]
LogRelFactsImpl.Bind_inv [lemma, in DecSyn.logrel]
LogRelFactsImpl.case [lemma, in DecSyn.logrel]
LogRelFactsImpl.CR_SNat [lemma, in DecSyn.logrel]
LogRelFactsImpl.CR_okay [lemma, in DecSyn.logrel]
LogRelFactsImpl.cumulative [lemma, in DecSyn.logrel]
LogRelFactsImpl.functional [lemma, in DecSyn.logrel]
LogRelFactsImpl.InterpUniv_Functional [lemma, in DecSyn.logrel]
LogRelFactsImpl.InterpUniv_Join [lemma, in DecSyn.logrel]
LogRelFactsImpl.join [lemma, in DecSyn.logrel]
LogRelFactsImpl.Nat_inv [lemma, in DecSyn.logrel]
LogRelFactsImpl.N_Exps [lemma, in DecSyn.logrel]
LogRelFactsImpl.SNe_inv [lemma, in DecSyn.logrel]
LogRelFactsImpl.sub [lemma, in DecSyn.logrel]
LogRelFactsImpl.sub' [lemma, in DecSyn.logrel]
LogRelFactsImpl.sub0 [lemma, in DecSyn.logrel]
LogRelFactsImpl.Univ_inv [lemma, in DecSyn.logrel]
LogRelFacts.adequacy [axiom, in DecSyn.logrel]
LogRelFacts.back_closs [axiom, in DecSyn.logrel]
LogRelFacts.back_clos [axiom, in DecSyn.logrel]
LogRelFacts.Bind_nopf [axiom, in DecSyn.logrel]
LogRelFacts.Bind_inv_nopf [axiom, in DecSyn.logrel]
LogRelFacts.Bind_inv [axiom, in DecSyn.logrel]
LogRelFacts.case [axiom, in DecSyn.logrel]
LogRelFacts.cumulative [axiom, in DecSyn.logrel]
LogRelFacts.functional [axiom, in DecSyn.logrel]
LogRelFacts.join [axiom, in DecSyn.logrel]
LogRelFacts.Nat_inv [axiom, in DecSyn.logrel]
LogRelFacts.SNe_inv [axiom, in DecSyn.logrel]
LogRelFacts.sub [axiom, in DecSyn.logrel]
LogRelFacts.Univ_inv [axiom, in DecSyn.logrel]
LogRelImpl [module, in DecSyn.logrel]
LogRelImpl.InterpExt [inductive, in DecSyn.logrel]
LogRelImpl.InterpExt_lt_eq [lemma, in DecSyn.logrel]
LogRelImpl.InterpExt_lt_impl [lemma, in DecSyn.logrel]
LogRelImpl.InterpExt_Univ' [lemma, in DecSyn.logrel]
LogRelImpl.InterpExt_sind [definition, in DecSyn.logrel]
LogRelImpl.InterpExt_ind [definition, in DecSyn.logrel]
LogRelImpl.InterpExt_Conv [constructor, in DecSyn.logrel]
LogRelImpl.InterpExt_Step [constructor, in DecSyn.logrel]
LogRelImpl.InterpExt_Univ [constructor, in DecSyn.logrel]
LogRelImpl.InterpExt_Nat [constructor, in DecSyn.logrel]
LogRelImpl.InterpExt_Bind [constructor, in DecSyn.logrel]
LogRelImpl.InterpExt_Ne [constructor, in DecSyn.logrel]
LogRelImpl.InterpUniv [definition, in DecSyn.logrel]
LogRelImpl.InterpUniv_Conv [lemma, in DecSyn.logrel]
LogRelImpl.InterpUniv_Nat [lemma, in DecSyn.logrel]
LogRelImpl.InterpUniv_Step [lemma, in DecSyn.logrel]
LogRelImpl.InterpUniv_Univ [lemma, in DecSyn.logrel]
LogRelImpl.InterpUniv_Bind [lemma, in DecSyn.logrel]
LogRelImpl.InterpUniv_Ne [lemma, in DecSyn.logrel]
LogRelImpl.InterpUniv_ind [lemma, in DecSyn.logrel]
LogRelImpl.InterpUniv_nolt [lemma, in DecSyn.logrel]
LogRelImpl.InterpUniv_rec_nolt [lemma, in DecSyn.logrel]
LogRelImpl.InterpUniv_rec_acc_irrel [lemma, in DecSyn.logrel]
LogRelImpl.InterpUniv_rec [definition, in DecSyn.logrel]
_ <? _ [notation, in DecSyn.logrel]
⟦ _ ⟧ _ ↘ _ [notation, in DecSyn.logrel]
⟦ _ ⟧ _ ;; _ ↘ _ [notation, in DecSyn.logrel]
LogRel.InterpUniv [axiom, in DecSyn.logrel]
LogRel.InterpUniv_ind [axiom, in DecSyn.logrel]
LogRel.InterpUniv_Conv [axiom, in DecSyn.logrel]
LogRel.InterpUniv_Nat [axiom, in DecSyn.logrel]
LogRel.InterpUniv_Step [axiom, in DecSyn.logrel]
LogRel.InterpUniv_Univ [axiom, in DecSyn.logrel]
LogRel.InterpUniv_Bind [axiom, in DecSyn.logrel]
LogRel.InterpUniv_Ne [axiom, in DecSyn.logrel]
⟦ _ ⟧ _ ↘ _ [notation, in DecSyn.logrel]
lookup [inductive, in DecSyn.common]
lookup_deter [lemma, in DecSyn.common]
lookup_sind [definition, in DecSyn.common]
lookup_ind [definition, in DecSyn.common]
LoRed [module, in DecSyn.fp_red]
LoReds [module, in DecSyn.fp_red]
loreds_hne_preservation [lemma, in DecSyn.algorithmic]
loreds_embed [lemma, in DecSyn.algorithmic]
LoReds.AbsCong [lemma, in DecSyn.fp_red]
LoReds.AppCong [lemma, in DecSyn.fp_red]
LoReds.BindCong [lemma, in DecSyn.fp_red]
LoReds.FromSN [lemma, in DecSyn.fp_red]
LoReds.FromSN_mutual [lemma, in DecSyn.fp_red]
LoReds.hf_ne_imp [lemma, in DecSyn.fp_red]
LoReds.hf_preservation [lemma, in DecSyn.fp_red]
LoReds.IndCong [lemma, in DecSyn.fp_red]
LoReds.PairCong [lemma, in DecSyn.fp_red]
LoReds.ProjCong [lemma, in DecSyn.fp_red]
LoReds.SucCong [lemma, in DecSyn.fp_red]
LoReds.ToRReds [lemma, in DecSyn.fp_red]
lored_nsteps_pair_inv [lemma, in DecSyn.algorithmic]
lored_nsteps_proj_cong [lemma, in DecSyn.algorithmic]
lored_nsteps_app_cong [lemma, in DecSyn.algorithmic]
lored_nsteps_proj_inv [lemma, in DecSyn.algorithmic]
lored_nsteps_app_inv [lemma, in DecSyn.algorithmic]
lored_nsteps_ind_inv [lemma, in DecSyn.algorithmic]
lored_nsteps_bind_inv [lemma, in DecSyn.algorithmic]
lored_hne_preservation [lemma, in DecSyn.algorithmic]
lored_nsteps_abs_inv [lemma, in DecSyn.algorithmic]
lored_nsteps_suc_inv [lemma, in DecSyn.algorithmic]
lored_nsteps_renaming [lemma, in DecSyn.algorithmic]
lored_embed [lemma, in DecSyn.algorithmic]
LoRed.AbsCong [constructor, in DecSyn.fp_red]
LoRed.AppAbs [constructor, in DecSyn.fp_red]
LoRed.AppAbs' [lemma, in DecSyn.fp_red]
LoRed.AppCong0 [constructor, in DecSyn.fp_red]
LoRed.AppCong1 [constructor, in DecSyn.fp_red]
LoRed.BindCong0 [constructor, in DecSyn.fp_red]
LoRed.BindCong1 [constructor, in DecSyn.fp_red]
LoRed.hf_preservation [lemma, in DecSyn.fp_red]
LoRed.IndCong0 [constructor, in DecSyn.fp_red]
LoRed.IndCong1 [constructor, in DecSyn.fp_red]
LoRed.IndCong2 [constructor, in DecSyn.fp_red]
LoRed.IndCong3 [constructor, in DecSyn.fp_red]
LoRed.IndSuc [constructor, in DecSyn.fp_red]
LoRed.IndSuc' [lemma, in DecSyn.fp_red]
LoRed.IndZero [constructor, in DecSyn.fp_red]
LoRed.PairCong0 [constructor, in DecSyn.fp_red]
LoRed.PairCong1 [constructor, in DecSyn.fp_red]
LoRed.ProjCong [constructor, in DecSyn.fp_red]
LoRed.ProjPair [constructor, in DecSyn.fp_red]
LoRed.R [inductive, in DecSyn.fp_red]
LoRed.renaming [lemma, in DecSyn.fp_red]
LoRed.R_sind [definition, in DecSyn.fp_red]
LoRed.R_ind [definition, in DecSyn.fp_red]
LoRed.SucCong [constructor, in DecSyn.fp_red]
LoRed.ToRRed [lemma, in DecSyn.fp_red]
LRFacts [module, in DecSyn.logrel]
M
morphing [lemma, in DecSyn.structural]morphing_id [lemma, in DecSyn.structural]
morphing_wt' [lemma, in DecSyn.structural]
morphing_wt [lemma, in DecSyn.structural]
morphing_up [lemma, in DecSyn.structural]
morphing_ext [lemma, in DecSyn.structural]
morphing_ren [lemma, in DecSyn.structural]
morphing_ok [definition, in DecSyn.structural]
morphing_SemWt_Univ [lemma, in DecSyn.logrel]
morphing_SemWt [lemma, in DecSyn.logrel]
N
Nat_Inv [lemma, in DecSyn.algorithmic]ne [definition, in DecSyn.fp_red]
NeEPar [module, in DecSyn.fp_red]
NeEPars [module, in DecSyn.fp_red]
NeEPars.R_nonelim_nf [lemma, in DecSyn.fp_red]
NeEPars.ToEReds [lemma, in DecSyn.fp_red]
NeEPar.AppEta [constructor, in DecSyn.fp_red]
NeEPar.epar_nonelim_ind [definition, in DecSyn.fp_red]
NeEPar.epar_elim_ind [definition, in DecSyn.fp_red]
NeEPar.NAbsCong [constructor, in DecSyn.fp_red]
NeEPar.NAppCong [constructor, in DecSyn.fp_red]
NeEPar.NBindCong [constructor, in DecSyn.fp_red]
NeEPar.NIndCong [constructor, in DecSyn.fp_red]
NeEPar.NNatCong [constructor, in DecSyn.fp_red]
NeEPar.NPairCong [constructor, in DecSyn.fp_red]
NeEPar.NProjCong [constructor, in DecSyn.fp_red]
NeEPar.NSucCong [constructor, in DecSyn.fp_red]
NeEPar.NUniv [constructor, in DecSyn.fp_red]
NeEPar.NVarTm [constructor, in DecSyn.fp_red]
NeEPar.NZeroCong [constructor, in DecSyn.fp_red]
NeEPar.PairEta [constructor, in DecSyn.fp_red]
NeEPar.R_elim_nonelim [lemma, in DecSyn.fp_red]
NeEPar.R_nonelim_nothf [lemma, in DecSyn.fp_red]
NeEPar.R_elim_nf [lemma, in DecSyn.fp_red]
NeEPar.R_elim_sind [definition, in DecSyn.fp_red]
NeEPar.R_elim_ind [definition, in DecSyn.fp_red]
NeEPar.R_nonelim_sind [definition, in DecSyn.fp_red]
NeEPar.R_nonelim_ind [definition, in DecSyn.fp_red]
NeEPar.R_elim [inductive, in DecSyn.fp_red]
NeEPar.R_inj [constructor, in DecSyn.fp_red]
NeEPar.R_nonelim [inductive, in DecSyn.fp_red]
NeEPar.ToEPar [lemma, in DecSyn.fp_red]
neuneu_nonconf [definition, in DecSyn.common]
ne_nf_embed [lemma, in DecSyn.fp_red]
ne_nf_ren [lemma, in DecSyn.fp_red]
ne_nf [lemma, in DecSyn.fp_red]
ne_hne [lemma, in DecSyn.algorithmic]
nf [definition, in DecSyn.fp_red]
NoForbid [module, in DecSyn.fp_red]
NoForbid_FactSN [module, in DecSyn.fp_red]
NoForbid_Fact.P_RReds [lemma, in DecSyn.fp_red]
NoForbid_Fact.P_EPars [lemma, in DecSyn.fp_red]
NoForbid_Fact [module, in DecSyn.fp_red]
NoForbid_FactSig.P_RReds [axiom, in DecSyn.fp_red]
NoForbid_FactSig.P_EPars [axiom, in DecSyn.fp_red]
NoForbid_FactSig [module, in DecSyn.fp_red]
NoForbid.P [axiom, in DecSyn.fp_red]
NoForbid.PApp_imp [axiom, in DecSyn.fp_red]
NoForbid.PInd_imp [axiom, in DecSyn.fp_red]
NoForbid.PProj_imp [axiom, in DecSyn.fp_red]
NoForbid.P_renaming [axiom, in DecSyn.fp_red]
NoForbid.P_ProjInv [axiom, in DecSyn.fp_red]
NoForbid.P_PairInv [axiom, in DecSyn.fp_red]
NoForbid.P_IndInv [axiom, in DecSyn.fp_red]
NoForbid.P_BindInv [axiom, in DecSyn.fp_red]
NoForbid.P_SucInv [axiom, in DecSyn.fp_red]
NoForbid.P_AbsInv [axiom, in DecSyn.fp_red]
NoForbid.P_AppInv [axiom, in DecSyn.fp_red]
NoForbid.P_RRed [axiom, in DecSyn.fp_red]
NoForbid.P_EPar [axiom, in DecSyn.fp_red]
nostuck [definition, in DecSyn.cosn]
nostuck_antisubstitution [lemma, in DecSyn.cosn]
N_IndSuc' [lemma, in DecSyn.fp_red]
N_β' [lemma, in DecSyn.fp_red]
N_IndCong [constructor, in DecSyn.fp_red]
N_IndSuc [constructor, in DecSyn.fp_red]
N_IndZero [constructor, in DecSyn.fp_red]
N_ProjCong [constructor, in DecSyn.fp_red]
N_ProjPairR [constructor, in DecSyn.fp_red]
N_ProjPairL [constructor, in DecSyn.fp_red]
N_AppL [constructor, in DecSyn.fp_red]
N_β [constructor, in DecSyn.fp_red]
N_Suc [constructor, in DecSyn.fp_red]
N_Zero [constructor, in DecSyn.fp_red]
N_Nat [constructor, in DecSyn.fp_red]
N_Univ [constructor, in DecSyn.fp_red]
N_Bind [constructor, in DecSyn.fp_red]
N_Exp [constructor, in DecSyn.fp_red]
N_SNe [constructor, in DecSyn.fp_red]
N_Abs [constructor, in DecSyn.fp_red]
N_Pair [constructor, in DecSyn.fp_red]
N_Ind [constructor, in DecSyn.fp_red]
N_Proj [constructor, in DecSyn.fp_red]
N_App [constructor, in DecSyn.fp_red]
N_Var [constructor, in DecSyn.fp_red]
N_Projs [lemma, in DecSyn.logrel]
O
option_comp [definition, in DecSyn.Autosubst2.core]option_ext [definition, in DecSyn.Autosubst2.core]
option_id [definition, in DecSyn.Autosubst2.core]
option_map [definition, in DecSyn.Autosubst2.core]
P
Pair_Inv [lemma, in DecSyn.admissible]Pair_Sig_Inv [lemma, in DecSyn.algorithmic]
PAppBind_imp [lemma, in DecSyn.fp_red]
PAppPair_imp [lemma, in DecSyn.fp_red]
PApp_imp [lemma, in DecSyn.fp_red]
PInd_imp [lemma, in DecSyn.fp_red]
pointwise_forall [lemma, in DecSyn.Autosubst2.core]
PProjAbs_imp [lemma, in DecSyn.fp_red]
PProjBind_imp [lemma, in DecSyn.fp_red]
PProj_imp [lemma, in DecSyn.fp_red]
preservation [library]
ProdSpace [definition, in DecSyn.logrel]
prod_comp [definition, in DecSyn.Autosubst2.core]
prod_ext [definition, in DecSyn.Autosubst2.core]
prod_id [definition, in DecSyn.Autosubst2.core]
prod_map [definition, in DecSyn.Autosubst2.core]
Proj1_Inv [lemma, in DecSyn.admissible]
Proj2_Inv [lemma, in DecSyn.admissible]
PTag_eq_dec [definition, in DecSyn.executable]
R
redsns_preservation [lemma, in DecSyn.logrel]redsn_preservation_mutual [lemma, in DecSyn.logrel]
red_uniquenf [lemma, in DecSyn.fp_red]
red_confluence [lemma, in DecSyn.fp_red]
red_sn_preservation [lemma, in DecSyn.fp_red]
regularity [lemma, in DecSyn.structural]
regularity_sub0 [lemma, in DecSyn.structural]
renaming [lemma, in DecSyn.structural]
renaming_comp [lemma, in DecSyn.admissible]
renaming_su' [lemma, in DecSyn.structural]
renaming_wt' [lemma, in DecSyn.structural]
renaming_wt [lemma, in DecSyn.structural]
renaming_up [lemma, in DecSyn.structural]
renaming_shift [lemma, in DecSyn.common]
renaming_ok [definition, in DecSyn.common]
renaming_SemWt [lemma, in DecSyn.logrel]
RenNotations [module, in DecSyn.Autosubst2.unscoped]
⟨ _ ; _ ⟩ (fscope) [notation, in DecSyn.Autosubst2.unscoped]
⟨ _ ⟩ (fscope) [notation, in DecSyn.Autosubst2.unscoped]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in DecSyn.Autosubst2.unscoped]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in DecSyn.Autosubst2.unscoped]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [notation, in DecSyn.Autosubst2.unscoped]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in DecSyn.Autosubst2.unscoped]
_ ⟨ _ ⟩ (subst_scope) [notation, in DecSyn.Autosubst2.unscoped]
ren_injective [lemma, in DecSyn.common]
ren_inj [definition, in DecSyn.common]
ren1 [projection, in DecSyn.Autosubst2.unscoped]
Ren1 [record, in DecSyn.Autosubst2.unscoped]
ren1 [constructor, in DecSyn.Autosubst2.unscoped]
Ren1 [inductive, in DecSyn.Autosubst2.unscoped]
ren2 [projection, in DecSyn.Autosubst2.unscoped]
Ren2 [record, in DecSyn.Autosubst2.unscoped]
ren2 [constructor, in DecSyn.Autosubst2.unscoped]
Ren2 [inductive, in DecSyn.Autosubst2.unscoped]
ren3 [projection, in DecSyn.Autosubst2.unscoped]
Ren3 [record, in DecSyn.Autosubst2.unscoped]
ren3 [constructor, in DecSyn.Autosubst2.unscoped]
Ren3 [inductive, in DecSyn.Autosubst2.unscoped]
ren4 [projection, in DecSyn.Autosubst2.unscoped]
Ren4 [record, in DecSyn.Autosubst2.unscoped]
ren4 [constructor, in DecSyn.Autosubst2.unscoped]
Ren4 [inductive, in DecSyn.Autosubst2.unscoped]
ren5 [projection, in DecSyn.Autosubst2.unscoped]
Ren5 [record, in DecSyn.Autosubst2.unscoped]
ren5 [constructor, in DecSyn.Autosubst2.unscoped]
Ren5 [inductive, in DecSyn.Autosubst2.unscoped]
RERed [module, in DecSyn.fp_red]
REReds [module, in DecSyn.fp_red]
REReds.AbsCong [lemma, in DecSyn.fp_red]
REReds.AppCong [lemma, in DecSyn.fp_red]
REReds.BindCong [lemma, in DecSyn.fp_red]
REReds.bind_inv [lemma, in DecSyn.fp_red]
REReds.bind_preservation [lemma, in DecSyn.fp_red]
REReds.cong [lemma, in DecSyn.fp_red]
REReds.cong_up2 [lemma, in DecSyn.fp_red]
REReds.cong_up [lemma, in DecSyn.fp_red]
REReds.cong' [lemma, in DecSyn.fp_red]
REReds.FromEReds [lemma, in DecSyn.fp_red]
REReds.FromRReds [lemma, in DecSyn.fp_red]
REReds.hne_ind_inv [lemma, in DecSyn.fp_red]
REReds.hne_proj_inv [lemma, in DecSyn.fp_red]
REReds.hne_app_inv [lemma, in DecSyn.fp_red]
REReds.hne_preservation [lemma, in DecSyn.fp_red]
REReds.IndCong [lemma, in DecSyn.fp_red]
REReds.nat_inv [lemma, in DecSyn.fp_red]
REReds.nat_preservation [lemma, in DecSyn.fp_red]
REReds.PairCong [lemma, in DecSyn.fp_red]
REReds.ProjCong [lemma, in DecSyn.fp_red]
REReds.sne_preservation [lemma, in DecSyn.fp_red]
REReds.sn_preservation [lemma, in DecSyn.fp_red]
REReds.substing [lemma, in DecSyn.fp_red]
REReds.SucCong [lemma, in DecSyn.fp_red]
REReds.suc_inv [lemma, in DecSyn.fp_red]
REReds.ToEReds [lemma, in DecSyn.fp_red]
REReds.univ_inv [lemma, in DecSyn.fp_red]
REReds.univ_preservation [lemma, in DecSyn.fp_red]
REReds.var_inv [lemma, in DecSyn.fp_red]
REReds.zero_inv [lemma, in DecSyn.fp_red]
rered_confluence [lemma, in DecSyn.fp_red]
rered_standardization' [lemma, in DecSyn.fp_red]
rered_standardization [lemma, in DecSyn.fp_red]
RERed.AbsCong [constructor, in DecSyn.fp_red]
RERed.AppAbs [constructor, in DecSyn.fp_red]
RERed.AppCong0 [constructor, in DecSyn.fp_red]
RERed.AppCong1 [constructor, in DecSyn.fp_red]
RERed.AppEta [constructor, in DecSyn.fp_red]
RERed.BindCong0 [constructor, in DecSyn.fp_red]
RERed.BindCong1 [constructor, in DecSyn.fp_red]
RERed.bind_preservation [lemma, in DecSyn.fp_red]
RERed.FromBeta [lemma, in DecSyn.fp_red]
RERed.FromEta [lemma, in DecSyn.fp_red]
RERed.hne_preservation [lemma, in DecSyn.fp_red]
RERed.IndCong0 [constructor, in DecSyn.fp_red]
RERed.IndCong1 [constructor, in DecSyn.fp_red]
RERed.IndCong2 [constructor, in DecSyn.fp_red]
RERed.IndCong3 [constructor, in DecSyn.fp_red]
RERed.IndSuc [constructor, in DecSyn.fp_red]
RERed.IndZero [constructor, in DecSyn.fp_red]
RERed.nat_preservation [lemma, in DecSyn.fp_red]
RERed.PairCong0 [constructor, in DecSyn.fp_red]
RERed.PairCong1 [constructor, in DecSyn.fp_red]
RERed.PairEta [constructor, in DecSyn.fp_red]
RERed.ProjCong [constructor, in DecSyn.fp_red]
RERed.ProjPair [constructor, in DecSyn.fp_red]
RERed.R [inductive, in DecSyn.fp_red]
RERed.R_sind [definition, in DecSyn.fp_red]
RERed.R_ind [definition, in DecSyn.fp_red]
RERed.sne_preservation [lemma, in DecSyn.fp_red]
RERed.sn_preservation [lemma, in DecSyn.fp_red]
RERed.substing [lemma, in DecSyn.fp_red]
RERed.SucCong [constructor, in DecSyn.fp_red]
RERed.ToBetaEta [lemma, in DecSyn.fp_red]
RERed.ToBetaEtaPar [lemma, in DecSyn.fp_red]
RERed.univ_preservation [lemma, in DecSyn.fp_red]
RPar [module, in DecSyn.fp_red]
RPar.AbsCong [constructor, in DecSyn.fp_red]
RPar.AppAbs [constructor, in DecSyn.fp_red]
RPar.AppAbs' [lemma, in DecSyn.fp_red]
RPar.AppCong [constructor, in DecSyn.fp_red]
RPar.BindCong [constructor, in DecSyn.fp_red]
RPar.cong [lemma, in DecSyn.fp_red]
RPar.diamond [lemma, in DecSyn.fp_red]
RPar.FromRRed [lemma, in DecSyn.fp_red]
RPar.IndCong [constructor, in DecSyn.fp_red]
RPar.IndSuc [constructor, in DecSyn.fp_red]
RPar.IndSuc' [lemma, in DecSyn.fp_red]
RPar.IndZero [constructor, in DecSyn.fp_red]
RPar.morphing [lemma, in DecSyn.fp_red]
RPar.morphing_up [lemma, in DecSyn.fp_red]
RPar.morphing_ext [lemma, in DecSyn.fp_red]
RPar.morphing_ren [lemma, in DecSyn.fp_red]
RPar.NatCong [constructor, in DecSyn.fp_red]
RPar.PairCong [constructor, in DecSyn.fp_red]
RPar.ProjCong [constructor, in DecSyn.fp_red]
RPar.ProjPair [constructor, in DecSyn.fp_red]
RPar.ProjPair' [lemma, in DecSyn.fp_red]
RPar.R [inductive, in DecSyn.fp_red]
RPar.refl [lemma, in DecSyn.fp_red]
RPar.renaming [lemma, in DecSyn.fp_red]
RPar.R_sind [definition, in DecSyn.fp_red]
RPar.R_ind [definition, in DecSyn.fp_red]
RPar.substing [lemma, in DecSyn.fp_red]
RPar.SucCong [constructor, in DecSyn.fp_red]
RPar.triangle [lemma, in DecSyn.fp_red]
RPar.Univ [constructor, in DecSyn.fp_red]
RPar.VarTm [constructor, in DecSyn.fp_red]
RPar.ZeroCong [constructor, in DecSyn.fp_red]
RRed [module, in DecSyn.fp_red]
RReds [module, in DecSyn.fp_red]
RReds.AbsCong [lemma, in DecSyn.fp_red]
RReds.abs_preservation [lemma, in DecSyn.fp_red]
RReds.AppCong [lemma, in DecSyn.fp_red]
RReds.BindCong [lemma, in DecSyn.fp_red]
RReds.FromRedSNs [lemma, in DecSyn.fp_red]
RReds.FromRPar [lemma, in DecSyn.fp_red]
RReds.IndCong [lemma, in DecSyn.fp_red]
RReds.nf_refl [lemma, in DecSyn.fp_red]
RReds.PairCong [lemma, in DecSyn.fp_red]
RReds.ProjCong [lemma, in DecSyn.fp_red]
RReds.renaming [lemma, in DecSyn.fp_red]
RReds.RParIff [lemma, in DecSyn.fp_red]
RReds.SucCong [lemma, in DecSyn.fp_red]
RRed_Eq [lemma, in DecSyn.preservation]
RRed.AbsCong [constructor, in DecSyn.fp_red]
RRed.abs_preservation [lemma, in DecSyn.fp_red]
RRed.antirenaming [lemma, in DecSyn.fp_red]
RRed.AppAbs [constructor, in DecSyn.fp_red]
RRed.AppAbs' [lemma, in DecSyn.fp_red]
RRed.AppCong0 [constructor, in DecSyn.fp_red]
RRed.AppCong1 [constructor, in DecSyn.fp_red]
RRed.BindCong0 [constructor, in DecSyn.fp_red]
RRed.BindCong1 [constructor, in DecSyn.fp_red]
RRed.FromRedSN [lemma, in DecSyn.fp_red]
RRed.IndCong0 [constructor, in DecSyn.fp_red]
RRed.IndCong1 [constructor, in DecSyn.fp_red]
RRed.IndCong2 [constructor, in DecSyn.fp_red]
RRed.IndCong3 [constructor, in DecSyn.fp_red]
RRed.IndSuc [constructor, in DecSyn.fp_red]
RRed.IndSuc' [lemma, in DecSyn.fp_red]
RRed.IndZero [constructor, in DecSyn.fp_red]
RRed.nf_imp [lemma, in DecSyn.fp_red]
RRed.PairCong0 [constructor, in DecSyn.fp_red]
RRed.PairCong1 [constructor, in DecSyn.fp_red]
RRed.ProjCong [constructor, in DecSyn.fp_red]
RRed.ProjPair [constructor, in DecSyn.fp_red]
RRed.R [inductive, in DecSyn.fp_red]
RRed.renaming [lemma, in DecSyn.fp_red]
RRed.R_sind [definition, in DecSyn.fp_red]
RRed.R_ind [definition, in DecSyn.fp_red]
RRed.substing [lemma, in DecSyn.fp_red]
RRed.SucCong [constructor, in DecSyn.fp_red]
S
safe [record, in DecSyn.cosn]Safe_NoForbid.P_IndInv [lemma, in DecSyn.cosn]
Safe_NoForbid.P_renaming [lemma, in DecSyn.cosn]
Safe_NoForbid.P_AbsInv [lemma, in DecSyn.cosn]
Safe_NoForbid.P_SucInv [lemma, in DecSyn.cosn]
Safe_NoForbid.P_BindInv [lemma, in DecSyn.cosn]
Safe_NoForbid.P_ProjInv [lemma, in DecSyn.cosn]
Safe_NoForbid.P_PairInv [lemma, in DecSyn.cosn]
Safe_NoForbid.P_AppInv [lemma, in DecSyn.cosn]
Safe_NoForbid.PInd_imp [lemma, in DecSyn.cosn]
Safe_NoForbid.PProj_imp [lemma, in DecSyn.cosn]
Safe_NoForbid.PApp_imp [lemma, in DecSyn.cosn]
Safe_NoForbid.P_RRed [lemma, in DecSyn.cosn]
Safe_NoForbid.P_EPar [lemma, in DecSyn.cosn]
Safe_NoForbid.P [definition, in DecSyn.cosn]
Safe_NoForbid [module, in DecSyn.cosn]
safe_omega [lemma, in DecSyn.cosn]
safe_rereds [lemma, in DecSyn.cosn]
safe_rered [lemma, in DecSyn.cosn]
safe_rred [lemma, in DecSyn.cosn]
safe_ind_imp [lemma, in DecSyn.cosn]
safe_proj_imp [lemma, in DecSyn.cosn]
safe_app_imp [lemma, in DecSyn.cosn]
safe_suc_inv [lemma, in DecSyn.cosn]
safe_pair_inv1 [lemma, in DecSyn.cosn]
safe_pair_inv0 [lemma, in DecSyn.cosn]
safe_bind_inv1 [lemma, in DecSyn.cosn]
safe_bind_inv0 [lemma, in DecSyn.cosn]
safe_ind_inv3 [lemma, in DecSyn.cosn]
safe_ind_inv2 [lemma, in DecSyn.cosn]
safe_ind_inv1 [lemma, in DecSyn.cosn]
safe_ind_inv0 [lemma, in DecSyn.cosn]
safe_proj_inv [lemma, in DecSyn.cosn]
safe_abs_inv [lemma, in DecSyn.cosn]
safe_app_inv1 [lemma, in DecSyn.cosn]
safe_app_inv0 [lemma, in DecSyn.cosn]
safe_antisubstitution [lemma, in DecSyn.cosn]
safe_coind [lemma, in DecSyn.cosn]
safe_red [projection, in DecSyn.cosn]
safe_nostuck [projection, in DecSyn.cosn]
salgor_ind [definition, in DecSyn.common]
salgo_dom_no_hred [lemma, in DecSyn.common]
salgo_dom_r_inv [lemma, in DecSyn.common]
salgo_ind [definition, in DecSyn.common]
salgo_dom_r_sind [definition, in DecSyn.common]
salgo_dom_r_ind [definition, in DecSyn.common]
salgo_dom_sind [definition, in DecSyn.common]
salgo_dom_ind [definition, in DecSyn.common]
salgo_dom_r [inductive, in DecSyn.common]
salgo_dom [inductive, in DecSyn.common]
SBind_inst [lemma, in DecSyn.logrel]
SBind_inv1 [lemma, in DecSyn.logrel]
scons [definition, in DecSyn.Autosubst2.unscoped]
scons_morphism2 [instance, in DecSyn.Autosubst2.unscoped]
scons_morphism [instance, in DecSyn.Autosubst2.unscoped]
scons_comp' [lemma, in DecSyn.Autosubst2.unscoped]
scons_eta_id' [lemma, in DecSyn.Autosubst2.unscoped]
scons_eta' [lemma, in DecSyn.Autosubst2.unscoped]
SemEq [definition, in DecSyn.logrel]
SemEq_SN_Join [lemma, in DecSyn.logrel]
SemEq_SemWt [lemma, in DecSyn.logrel]
SemLEq [definition, in DecSyn.logrel]
SemLEq_SN_Sub [lemma, in DecSyn.logrel]
SemLEq_SemWt [lemma, in DecSyn.logrel]
SemWff [inductive, in DecSyn.logrel]
SemWff_lookup [lemma, in DecSyn.logrel]
SemWff_sind [definition, in DecSyn.logrel]
SemWff_ind [definition, in DecSyn.logrel]
SemWff_cons [constructor, in DecSyn.logrel]
SemWff_nil [constructor, in DecSyn.logrel]
SemWt [definition, in DecSyn.logrel]
SemWt_SN [lemma, in DecSyn.logrel]
SemWt_SemLEq [lemma, in DecSyn.logrel]
SemWt_SemEq [lemma, in DecSyn.logrel]
SemWt_Univ [lemma, in DecSyn.logrel]
SE_App [lemma, in DecSyn.logrel]
SE_Nat [lemma, in DecSyn.logrel]
SE_FunExt [lemma, in DecSyn.logrel]
SE_PairExt [lemma, in DecSyn.logrel]
SE_PairEta [lemma, in DecSyn.logrel]
SE_ProjPair2 [lemma, in DecSyn.logrel]
SE_ProjPair1 [lemma, in DecSyn.logrel]
SE_IndSuc [lemma, in DecSyn.logrel]
SE_IndZero [lemma, in DecSyn.logrel]
SE_IndCong [lemma, in DecSyn.logrel]
SE_SucCong [lemma, in DecSyn.logrel]
SE_Proj2 [lemma, in DecSyn.logrel]
SE_Proj1 [lemma, in DecSyn.logrel]
SE_Pair [lemma, in DecSyn.logrel]
SE_Conv [lemma, in DecSyn.logrel]
SE_Conv' [lemma, in DecSyn.logrel]
SE_AppAbs [lemma, in DecSyn.logrel]
SE_AppEta [lemma, in DecSyn.logrel]
SE_Abs [lemma, in DecSyn.logrel]
SE_Bind [lemma, in DecSyn.logrel]
SE_Bind' [lemma, in DecSyn.logrel]
SE_Transitive [lemma, in DecSyn.logrel]
SE_Symmetric [lemma, in DecSyn.logrel]
SE_Refl [lemma, in DecSyn.logrel]
shift [definition, in DecSyn.Autosubst2.unscoped]
size_PTm_ren [lemma, in DecSyn.fp_red]
size_PTm [definition, in DecSyn.fp_red]
smorphing_ext [lemma, in DecSyn.logrel]
smorphing_ren [lemma, in DecSyn.logrel]
smorphing_ok_refl [lemma, in DecSyn.logrel]
smorphing_ok [definition, in DecSyn.logrel]
SN [inductive, in DecSyn.fp_red]
SNat [inductive, in DecSyn.fp_red]
SNat_sind [definition, in DecSyn.fp_red]
SNat_ind [definition, in DecSyn.fp_red]
SNat_SN [lemma, in DecSyn.logrel]
SNe [inductive, in DecSyn.fp_red]
sne_ind [definition, in DecSyn.fp_red]
SNe_sind [definition, in DecSyn.fp_red]
SNe_ind [definition, in DecSyn.fp_red]
SN_UniqueNF [module, in DecSyn.fp_red]
SN_NoForbid.P_IndInv [lemma, in DecSyn.fp_red]
SN_NoForbid.P_renaming [lemma, in DecSyn.fp_red]
SN_NoForbid.P_AbsInv [lemma, in DecSyn.fp_red]
SN_NoForbid.P_SucInv [lemma, in DecSyn.fp_red]
SN_NoForbid.P_BindInv [lemma, in DecSyn.fp_red]
SN_NoForbid.P_ProjInv [lemma, in DecSyn.fp_red]
SN_NoForbid.P_PairInv [lemma, in DecSyn.fp_red]
SN_NoForbid.P_AppInv [lemma, in DecSyn.fp_red]
SN_NoForbid.PInd_imp [lemma, in DecSyn.fp_red]
SN_NoForbid.PProj_imp [lemma, in DecSyn.fp_red]
SN_NoForbid.PApp_imp [lemma, in DecSyn.fp_red]
SN_NoForbid.P_RRed [lemma, in DecSyn.fp_red]
SN_NoForbid.P_EPar [lemma, in DecSyn.fp_red]
SN_NoForbid.P [definition, in DecSyn.fp_red]
SN_NoForbid [module, in DecSyn.fp_red]
SN_IndInv [lemma, in DecSyn.fp_red]
SN_ProjInv [lemma, in DecSyn.fp_red]
SN_AppInv [lemma, in DecSyn.fp_red]
sn_unmorphing [lemma, in DecSyn.fp_red]
sn_antirenaming [lemma, in DecSyn.fp_red]
sn_renaming [lemma, in DecSyn.fp_red]
SN_Proj [lemma, in DecSyn.fp_red]
sn_ind [definition, in DecSyn.fp_red]
SN_sind [definition, in DecSyn.fp_red]
SN_ind [definition, in DecSyn.fp_red]
sn_algo_dom [lemma, in DecSyn.algorithmic]
sn_term_metric [lemma, in DecSyn.algorithmic]
sn_bot_up2 [lemma, in DecSyn.logrel]
sn_bot_up [lemma, in DecSyn.logrel]
sn_unmorphing' [lemma, in DecSyn.logrel]
soundness [library]
sred_ind [definition, in DecSyn.fp_red]
SSu_Sig_Proj2 [lemma, in DecSyn.logrel]
SSu_Pi_Proj2 [lemma, in DecSyn.logrel]
SSu_Sig_Proj1 [lemma, in DecSyn.logrel]
SSu_Pi_Proj1 [lemma, in DecSyn.logrel]
SSu_Sig [lemma, in DecSyn.logrel]
SSu_Pi [lemma, in DecSyn.logrel]
SSu_Univ [lemma, in DecSyn.logrel]
SSu_Transitive [lemma, in DecSyn.logrel]
SSu_Eq [lemma, in DecSyn.logrel]
stm_conf_sym [lemma, in DecSyn.common]
stm_conf [definition, in DecSyn.common]
stm_tm_nonconf [lemma, in DecSyn.common]
stm_nonconf [definition, in DecSyn.common]
structural [library]
ST_Univ [lemma, in DecSyn.logrel]
ST_Univ' [lemma, in DecSyn.logrel]
ST_Ind [lemma, in DecSyn.logrel]
ST_Suc [lemma, in DecSyn.logrel]
ST_Zero [lemma, in DecSyn.logrel]
ST_Nat [lemma, in DecSyn.logrel]
ST_Conv [lemma, in DecSyn.logrel]
ST_Conv_E [lemma, in DecSyn.logrel]
ST_Conv' [lemma, in DecSyn.logrel]
ST_Proj2 [lemma, in DecSyn.logrel]
ST_Proj1 [lemma, in DecSyn.logrel]
ST_Pair [lemma, in DecSyn.logrel]
ST_App' [lemma, in DecSyn.logrel]
ST_App [lemma, in DecSyn.logrel]
ST_Abs [lemma, in DecSyn.logrel]
ST_Bind [lemma, in DecSyn.logrel]
ST_Bind' [lemma, in DecSyn.logrel]
ST_Var [lemma, in DecSyn.logrel]
ST_Var' [lemma, in DecSyn.logrel]
Sub [module, in DecSyn.fp_red]
subject_reduction [lemma, in DecSyn.preservation]
substing_wt [lemma, in DecSyn.structural]
SubstNotations [module, in DecSyn.Autosubst2.unscoped]
_ [ _ ; _ ] (subst_scope) [notation, in DecSyn.Autosubst2.unscoped]
_ [ _ ] (subst_scope) [notation, in DecSyn.Autosubst2.unscoped]
subst_scons_id [lemma, in DecSyn.common]
subst1 [projection, in DecSyn.Autosubst2.unscoped]
Subst1 [record, in DecSyn.Autosubst2.unscoped]
subst1 [constructor, in DecSyn.Autosubst2.unscoped]
Subst1 [inductive, in DecSyn.Autosubst2.unscoped]
subst2 [projection, in DecSyn.Autosubst2.unscoped]
Subst2 [record, in DecSyn.Autosubst2.unscoped]
subst2 [constructor, in DecSyn.Autosubst2.unscoped]
Subst2 [inductive, in DecSyn.Autosubst2.unscoped]
subst3 [projection, in DecSyn.Autosubst2.unscoped]
Subst3 [record, in DecSyn.Autosubst2.unscoped]
subst3 [constructor, in DecSyn.Autosubst2.unscoped]
Subst3 [inductive, in DecSyn.Autosubst2.unscoped]
subst4 [projection, in DecSyn.Autosubst2.unscoped]
Subst4 [record, in DecSyn.Autosubst2.unscoped]
subst4 [constructor, in DecSyn.Autosubst2.unscoped]
Subst4 [inductive, in DecSyn.Autosubst2.unscoped]
subst5 [projection, in DecSyn.Autosubst2.unscoped]
Subst5 [record, in DecSyn.Autosubst2.unscoped]
subst5 [constructor, in DecSyn.Autosubst2.unscoped]
Subst5 [inductive, in DecSyn.Autosubst2.unscoped]
subvar_inj [lemma, in DecSyn.algorithmic]
Sub_Bind_InvL [lemma, in DecSyn.algorithmic]
Sub_Univ_InvR [lemma, in DecSyn.algorithmic]
Sub_Bind_InvR [lemma, in DecSyn.algorithmic]
Sub.bind_inj [lemma, in DecSyn.fp_red]
Sub.bind_univ_noconf [lemma, in DecSyn.fp_red]
Sub.bind_nat_noconf [lemma, in DecSyn.fp_red]
Sub.bind_sne_noconf [lemma, in DecSyn.fp_red]
Sub.cong [lemma, in DecSyn.fp_red]
Sub.FromJoin [lemma, in DecSyn.fp_red]
Sub.hne_bind_noconf [lemma, in DecSyn.fp_red]
Sub.nat_bind_noconf [lemma, in DecSyn.fp_red]
Sub.nat_univ_noconf [lemma, in DecSyn.fp_red]
Sub.nat_sne_noconf [lemma, in DecSyn.fp_red]
Sub.PiCong [lemma, in DecSyn.fp_red]
Sub.R [definition, in DecSyn.fp_red]
Sub.refl [lemma, in DecSyn.fp_red]
Sub.SigCong [lemma, in DecSyn.fp_red]
Sub.sne_univ_noconf [lemma, in DecSyn.fp_red]
Sub.sne_bind_noconf [lemma, in DecSyn.fp_red]
Sub.sne_nat_noconf [lemma, in DecSyn.fp_red]
Sub.standardization [lemma, in DecSyn.fp_red]
Sub.standardization_lo [lemma, in DecSyn.fp_red]
Sub.substing [lemma, in DecSyn.fp_red]
Sub.suc_inj [lemma, in DecSyn.fp_red]
Sub.ToESub [lemma, in DecSyn.fp_red]
Sub.ToJoin [lemma, in DecSyn.fp_red]
Sub.transitive [lemma, in DecSyn.fp_red]
Sub.UnivCong [lemma, in DecSyn.fp_red]
Sub.univ_inj [lemma, in DecSyn.fp_red]
Sub.univ_bind_noconf [lemma, in DecSyn.fp_red]
Sub.univ_nat_noconf [lemma, in DecSyn.fp_red]
Sub.univ_sne_noconf [lemma, in DecSyn.fp_red]
Sub1 [module, in DecSyn.fp_red]
Sub1.bind_preservation [lemma, in DecSyn.fp_red]
Sub1.commutativity_Rs [lemma, in DecSyn.fp_red]
Sub1.commutativity_Ls [lemma, in DecSyn.fp_red]
Sub1.commutativity0 [lemma, in DecSyn.fp_red]
Sub1.hne_refl [lemma, in DecSyn.fp_red]
Sub1.PiCong [constructor, in DecSyn.fp_red]
Sub1.R [inductive, in DecSyn.fp_red]
Sub1.refl [lemma, in DecSyn.fp_red]
Sub1.Refl [constructor, in DecSyn.fp_red]
Sub1.renaming [lemma, in DecSyn.fp_red]
Sub1.R_sind [definition, in DecSyn.fp_red]
Sub1.R_ind [definition, in DecSyn.fp_red]
Sub1.SigCong [constructor, in DecSyn.fp_red]
Sub1.sne_preservation [lemma, in DecSyn.fp_red]
Sub1.sn_preservation [lemma, in DecSyn.fp_red]
Sub1.substing [lemma, in DecSyn.fp_red]
Sub1.transitive [lemma, in DecSyn.fp_red]
Sub1.transitive0 [lemma, in DecSyn.fp_red]
Sub1.Univ [constructor, in DecSyn.fp_red]
Sub1.univ_preservation [lemma, in DecSyn.fp_red]
Suc_Inv [lemma, in DecSyn.preservation]
SumSpace [definition, in DecSyn.logrel]
Su_Sig_Proj2 [constructor, in DecSyn.typing]
Su_Pi_Proj2 [constructor, in DecSyn.typing]
Su_Sig_Proj1 [constructor, in DecSyn.typing]
Su_Pi_Proj1 [constructor, in DecSyn.typing]
Su_Eq [constructor, in DecSyn.typing]
Su_Sig [constructor, in DecSyn.typing]
Su_Pi [constructor, in DecSyn.typing]
Su_Univ [constructor, in DecSyn.typing]
Su_Transitive [constructor, in DecSyn.typing]
Su_Sig_Proj2_Var [lemma, in DecSyn.structural]
Su_Pi_Proj2_Var [lemma, in DecSyn.structural]
Su_Sig_Proj2' [lemma, in DecSyn.structural]
Su_Pi_Proj2' [lemma, in DecSyn.structural]
Su_Wt [lemma, in DecSyn.structural]
synsub_to_usub [lemma, in DecSyn.soundness]
syntax [library]
S_Red [constructor, in DecSyn.fp_red]
S_Suc [constructor, in DecSyn.fp_red]
S_Neu [constructor, in DecSyn.fp_red]
S_Zero [constructor, in DecSyn.fp_red]
S_HRedR' [lemma, in DecSyn.common]
S_HRedsR [lemma, in DecSyn.common]
S_HRedsL [lemma, in DecSyn.common]
S_HRedR [constructor, in DecSyn.common]
S_HRedL [constructor, in DecSyn.common]
S_NfNf [constructor, in DecSyn.common]
S_Conf [constructor, in DecSyn.common]
S_NeuNeu [constructor, in DecSyn.common]
S_NatCong [constructor, in DecSyn.common]
S_SigCong [constructor, in DecSyn.common]
S_PiCong [constructor, in DecSyn.common]
S_UnivCong [constructor, in DecSyn.common]
T
term_metric_algo_dom [lemma, in DecSyn.algorithmic]term_metric_ind [lemma, in DecSyn.algorithmic]
term_metric_proj [lemma, in DecSyn.algorithmic]
term_metric_app [lemma, in DecSyn.algorithmic]
term_metric_pair_neu [lemma, in DecSyn.algorithmic]
term_metric_abs_neu [lemma, in DecSyn.algorithmic]
term_metric_suc [lemma, in DecSyn.algorithmic]
term_metric_bind [lemma, in DecSyn.algorithmic]
term_metric_pair [lemma, in DecSyn.algorithmic]
term_metric_abs [lemma, in DecSyn.algorithmic]
term_metric_case [lemma, in DecSyn.algorithmic]
term_metric_sym [lemma, in DecSyn.algorithmic]
term_metric [definition, in DecSyn.algorithmic]
there [constructor, in DecSyn.common]
there' [lemma, in DecSyn.common]
tm_omega [definition, in DecSyn.cosn]
tm_conf_sym [lemma, in DecSyn.common]
tm_stm_conf [lemma, in DecSyn.common]
tm_conf [definition, in DecSyn.common]
tm_nonconf [definition, in DecSyn.common]
TRedSN [inductive, in DecSyn.fp_red]
TRedSN_sind [definition, in DecSyn.fp_red]
TRedSN_ind [definition, in DecSyn.fp_red]
TRedSN' [inductive, in DecSyn.fp_red]
TRedSN'_sind [definition, in DecSyn.fp_red]
TRedSN'_ind [definition, in DecSyn.fp_red]
typing [library]
T_Conv [constructor, in DecSyn.typing]
T_Ind [constructor, in DecSyn.typing]
T_Suc [constructor, in DecSyn.typing]
T_Zero [constructor, in DecSyn.typing]
T_Nat [constructor, in DecSyn.typing]
T_Univ [constructor, in DecSyn.typing]
T_Proj2 [constructor, in DecSyn.typing]
T_Proj1 [constructor, in DecSyn.typing]
T_Pair [constructor, in DecSyn.typing]
T_App [constructor, in DecSyn.typing]
T_Abs [constructor, in DecSyn.typing]
T_Bind [constructor, in DecSyn.typing]
T_Var [constructor, in DecSyn.typing]
T_Eta [lemma, in DecSyn.admissible]
T_Abs [lemma, in DecSyn.admissible]
T_Once [constructor, in DecSyn.fp_red]
T_Refl [constructor, in DecSyn.fp_red]
T_AbsBind_Imp [lemma, in DecSyn.algorithmic]
T_PairUniv_Imp' [lemma, in DecSyn.algorithmic]
T_SucUniv_Imp' [lemma, in DecSyn.algorithmic]
T_ZeroUniv_Imp' [lemma, in DecSyn.algorithmic]
T_AbsUniv_Imp' [lemma, in DecSyn.algorithmic]
T_AbsUniv_Imp [lemma, in DecSyn.algorithmic]
T_PairUniv_Imp [lemma, in DecSyn.algorithmic]
T_PairSuc_Imp [lemma, in DecSyn.algorithmic]
T_PairZero_Imp [lemma, in DecSyn.algorithmic]
T_PairNat_Imp [lemma, in DecSyn.algorithmic]
T_PairBind_Imp [lemma, in DecSyn.algorithmic]
T_AbsNat_Imp [lemma, in DecSyn.algorithmic]
T_AbsSuc_Imp [lemma, in DecSyn.algorithmic]
T_AbsZero_Imp [lemma, in DecSyn.algorithmic]
T_AbsPair_Imp [lemma, in DecSyn.algorithmic]
T_Univ_Raise [lemma, in DecSyn.algorithmic]
T_Abs_Neu_Inv [lemma, in DecSyn.algorithmic]
T_Abs_Inv [lemma, in DecSyn.algorithmic]
T_Conv_E [lemma, in DecSyn.algorithmic]
T_Bind' [lemma, in DecSyn.structural]
T_Proj2' [lemma, in DecSyn.structural]
T_Ind' [lemma, in DecSyn.structural]
T_Pair' [lemma, in DecSyn.structural]
T_App' [lemma, in DecSyn.structural]
T_Nat' [lemma, in DecSyn.structural]
U
UniqueNF [module, in DecSyn.fp_red]UniqueNF.η_postponement_star [lemma, in DecSyn.fp_red]
UniqueNF.η_postponement_strengthened [lemma, in DecSyn.fp_red]
UniqueNF.η_postponement [lemma, in DecSyn.fp_red]
UniqueNF.η_split [lemma, in DecSyn.fp_red]
Univ_Inv [lemma, in DecSyn.algorithmic]
unscoped [library]
UnscopedNotations [module, in DecSyn.Autosubst2.unscoped]
↑ (subst_scope) [notation, in DecSyn.Autosubst2.unscoped]
_ .. (subst_scope) [notation, in DecSyn.Autosubst2.unscoped]
up_allfv [definition, in DecSyn.Autosubst2.unscoped]
up_ren_ren [lemma, in DecSyn.Autosubst2.unscoped]
up_ren [definition, in DecSyn.Autosubst2.unscoped]
up_injective [lemma, in DecSyn.common]
V
Var [record, in DecSyn.Autosubst2.unscoped]Var [inductive, in DecSyn.Autosubst2.unscoped]
var_zero [definition, in DecSyn.Autosubst2.unscoped]
Var_Inv [lemma, in DecSyn.structural]
W
weakening_su [lemma, in DecSyn.structural]weakening_wt' [lemma, in DecSyn.structural]
weakening_wt [lemma, in DecSyn.structural]
weakening_Sem_Univ [lemma, in DecSyn.logrel]
weakening_Sem [lemma, in DecSyn.logrel]
Wff [inductive, in DecSyn.typing]
Wff_sind [definition, in DecSyn.typing]
Wff_ind [definition, in DecSyn.typing]
Wff_Cons [constructor, in DecSyn.typing]
Wff_Nil [constructor, in DecSyn.typing]
Wff_Cons' [lemma, in DecSyn.structural]
wff_mutual [lemma, in DecSyn.structural]
wf_ind [definition, in DecSyn.typing]
Wt [inductive, in DecSyn.typing]
wt_ind [definition, in DecSyn.typing]
Wt_sind [definition, in DecSyn.typing]
Wt_ind [definition, in DecSyn.typing]
Wt_Univ [lemma, in DecSyn.structural]
Z
Zero_Inv [lemma, in DecSyn.algorithmic]other
_ ⊢ _ ≲ _ [notation, in DecSyn.typing]_ ⊢ _ ≡ _ ∈ _ [notation, in DecSyn.typing]
_ ⊢ _ ∈ _ [notation, in DecSyn.typing]
_ ⋖ _ [notation, in DecSyn.algorithmic]
_ ≪ _ [notation, in DecSyn.algorithmic]
_ ∼ _ [notation, in DecSyn.algorithmic]
_ ⇔ _ [notation, in DecSyn.algorithmic]
_ ↔ _ [notation, in DecSyn.algorithmic]
_ ⊨ _ ≲ _ [notation, in DecSyn.logrel]
_ ⊨ _ ≡ _ ∈ _ [notation, in DecSyn.logrel]
_ ⊨ _ ∈ _ [notation, in DecSyn.logrel]
_ ≐ _ [notation, in DecSyn.logrel]
list_map [notation, in DecSyn.Autosubst2.core]
⊢ _ [notation, in DecSyn.typing]
⊨ _ [notation, in DecSyn.logrel]
Γ_eq'_refl [lemma, in DecSyn.logrel]
Γ_eq'_cons [lemma, in DecSyn.logrel]
Γ_eq_sub [lemma, in DecSyn.logrel]
Γ_sub'_SemWt [lemma, in DecSyn.logrel]
Γ_sub'_cons [lemma, in DecSyn.logrel]
Γ_sub'_refl [lemma, in DecSyn.logrel]
Γ_eq' [definition, in DecSyn.logrel]
Γ_sub' [definition, in DecSyn.logrel]
ρ_ok_ext [lemma, in DecSyn.logrel]
ρ_ok_renaming [lemma, in DecSyn.logrel]
ρ_ok_cons' [lemma, in DecSyn.logrel]
ρ_ok_cons [lemma, in DecSyn.logrel]
ρ_ok_id [lemma, in DecSyn.logrel]
ρ_ok [definition, in DecSyn.logrel]
Notation Index
C
_ >> _ (fscope) [in DecSyn.Autosubst2.unscoped]_ .: _ (subst_scope) [in DecSyn.Autosubst2.unscoped]
[ _ ] (fscope) [in DecSyn.Autosubst2.syntax]
⟨ _ ⟩ (fscope) [in DecSyn.Autosubst2.syntax]
_ __PTm (subst_scope) [in DecSyn.Autosubst2.syntax]
_ __PTm (subst_scope) [in DecSyn.Autosubst2.syntax]
var (subst_scope) [in DecSyn.Autosubst2.syntax]
_ ⟨ _ ⟩ (subst_scope) [in DecSyn.Autosubst2.syntax]
↑__PTm (subst_scope) [in DecSyn.Autosubst2.syntax]
↑__PTm (subst_scope) [in DecSyn.Autosubst2.syntax]
_ [ _ ] (subst_scope) [in DecSyn.Autosubst2.syntax]
L
_ <? _ [in DecSyn.logrel]⟦ _ ⟧ _ ↘ _ [in DecSyn.logrel]
⟦ _ ⟧ _ ;; _ ↘ _ [in DecSyn.logrel]
⟦ _ ⟧ _ ↘ _ [in DecSyn.logrel]
R
⟨ _ ; _ ⟩ (fscope) [in DecSyn.Autosubst2.unscoped]⟨ _ ⟩ (fscope) [in DecSyn.Autosubst2.unscoped]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [in DecSyn.Autosubst2.unscoped]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [in DecSyn.Autosubst2.unscoped]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [in DecSyn.Autosubst2.unscoped]
_ ⟨ _ ; _ ⟩ (subst_scope) [in DecSyn.Autosubst2.unscoped]
_ ⟨ _ ⟩ (subst_scope) [in DecSyn.Autosubst2.unscoped]
S
_ [ _ ; _ ] (subst_scope) [in DecSyn.Autosubst2.unscoped]_ [ _ ] (subst_scope) [in DecSyn.Autosubst2.unscoped]
U
↑ (subst_scope) [in DecSyn.Autosubst2.unscoped]_ .. (subst_scope) [in DecSyn.Autosubst2.unscoped]
other
_ ⊢ _ ≲ _ [in DecSyn.typing]_ ⊢ _ ≡ _ ∈ _ [in DecSyn.typing]
_ ⊢ _ ∈ _ [in DecSyn.typing]
_ ⋖ _ [in DecSyn.algorithmic]
_ ≪ _ [in DecSyn.algorithmic]
_ ∼ _ [in DecSyn.algorithmic]
_ ⇔ _ [in DecSyn.algorithmic]
_ ↔ _ [in DecSyn.algorithmic]
_ ⊨ _ ≲ _ [in DecSyn.logrel]
_ ⊨ _ ≡ _ ∈ _ [in DecSyn.logrel]
_ ⊨ _ ∈ _ [in DecSyn.logrel]
_ ≐ _ [in DecSyn.logrel]
list_map [in DecSyn.Autosubst2.core]
⊢ _ [in DecSyn.typing]
⊨ _ [in DecSyn.logrel]
Module Index
C
CombineNotations [in DecSyn.Autosubst2.unscoped]Core [in DecSyn.Autosubst2.syntax]
D
DJoin [in DecSyn.fp_red]E
EJoin [in DecSyn.fp_red]EPar [in DecSyn.fp_red]
ERed [in DecSyn.fp_red]
EReds [in DecSyn.fp_red]
ESub [in DecSyn.fp_red]
Extra [in DecSyn.Autosubst2.syntax]
H
HRed [in DecSyn.algorithmic]HRed [in DecSyn.common]
HReds [in DecSyn.algorithmic]
I
interface [in DecSyn.Autosubst2.syntax]L
LogRel [in DecSyn.logrel]LogRelFacts [in DecSyn.logrel]
LogRelFactsImpl [in DecSyn.logrel]
LogRelImpl [in DecSyn.logrel]
LoRed [in DecSyn.fp_red]
LoReds [in DecSyn.fp_red]
LRFacts [in DecSyn.logrel]
N
NeEPar [in DecSyn.fp_red]NeEPars [in DecSyn.fp_red]
NoForbid [in DecSyn.fp_red]
NoForbid_FactSN [in DecSyn.fp_red]
NoForbid_Fact [in DecSyn.fp_red]
NoForbid_FactSig [in DecSyn.fp_red]
R
RenNotations [in DecSyn.Autosubst2.unscoped]RERed [in DecSyn.fp_red]
REReds [in DecSyn.fp_red]
RPar [in DecSyn.fp_red]
RRed [in DecSyn.fp_red]
RReds [in DecSyn.fp_red]
S
Safe_NoForbid [in DecSyn.cosn]SN_UniqueNF [in DecSyn.fp_red]
SN_NoForbid [in DecSyn.fp_red]
Sub [in DecSyn.fp_red]
SubstNotations [in DecSyn.Autosubst2.unscoped]
Sub1 [in DecSyn.fp_red]
U
UniqueNF [in DecSyn.fp_red]UnscopedNotations [in DecSyn.Autosubst2.unscoped]
Library Index
A
admissiblealgorithmic
C
commonconv_dec
core
cosn
E
executableexecutable_correct
F
fp_redL
logrelP
preservationS
soundnessstructural
syntax
T
typingU
unscopedConstructor Index
A
A_HRedR [in DecSyn.common]A_HRedL [in DecSyn.common]
A_NfNf [in DecSyn.common]
A_Conf [in DecSyn.common]
A_IndCong [in DecSyn.common]
A_ProjCong [in DecSyn.common]
A_AppCong [in DecSyn.common]
A_VarCong [in DecSyn.common]
A_NatCong [in DecSyn.common]
A_BindCong [in DecSyn.common]
A_UnivCong [in DecSyn.common]
A_SucSuc [in DecSyn.common]
A_ZeroZero [in DecSyn.common]
A_NeuPair [in DecSyn.common]
A_PairNeu [in DecSyn.common]
A_PairPair [in DecSyn.common]
A_NeuAbs [in DecSyn.common]
A_AbsNeu [in DecSyn.common]
A_AbsAbs [in DecSyn.common]
C
CE_HRed [in DecSyn.algorithmic]CE_IndCong [in DecSyn.algorithmic]
CE_AppCong [in DecSyn.algorithmic]
CE_ProjCong [in DecSyn.algorithmic]
CE_VarCong [in DecSyn.algorithmic]
CE_NeuNeu [in DecSyn.algorithmic]
CE_NatCong [in DecSyn.algorithmic]
CE_BindCong [in DecSyn.algorithmic]
CE_UnivCong [in DecSyn.algorithmic]
CE_NeuPair [in DecSyn.algorithmic]
CE_PairNeu [in DecSyn.algorithmic]
CE_PairPair [in DecSyn.algorithmic]
CE_NeuAbs [in DecSyn.algorithmic]
CE_AbsNeu [in DecSyn.algorithmic]
CE_AbsAbs [in DecSyn.algorithmic]
CE_SucSuc [in DecSyn.algorithmic]
CE_ZeroZero [in DecSyn.algorithmic]
CLE_HRed [in DecSyn.algorithmic]
CLE_NeuNeu [in DecSyn.algorithmic]
CLE_NatCong [in DecSyn.algorithmic]
CLE_SigCong [in DecSyn.algorithmic]
CLE_PiCong [in DecSyn.algorithmic]
CLE_UnivCong [in DecSyn.algorithmic]
Core.PAbs [in DecSyn.Autosubst2.syntax]
Core.PApp [in DecSyn.Autosubst2.syntax]
Core.PBind [in DecSyn.Autosubst2.syntax]
Core.PInd [in DecSyn.Autosubst2.syntax]
Core.PL [in DecSyn.Autosubst2.syntax]
Core.PNat [in DecSyn.Autosubst2.syntax]
Core.PPair [in DecSyn.Autosubst2.syntax]
Core.PPi [in DecSyn.Autosubst2.syntax]
Core.PProj [in DecSyn.Autosubst2.syntax]
Core.PR [in DecSyn.Autosubst2.syntax]
Core.PSig [in DecSyn.Autosubst2.syntax]
Core.PSuc [in DecSyn.Autosubst2.syntax]
Core.PUniv [in DecSyn.Autosubst2.syntax]
Core.PZero [in DecSyn.Autosubst2.syntax]
Core.up_PTm [in DecSyn.Autosubst2.syntax]
Core.VarPTm [in DecSyn.Autosubst2.syntax]
E
EPar.AbsCong [in DecSyn.fp_red]EPar.AppCong [in DecSyn.fp_red]
EPar.AppEta [in DecSyn.fp_red]
EPar.BindCong [in DecSyn.fp_red]
EPar.IndCong [in DecSyn.fp_red]
EPar.NatCong [in DecSyn.fp_red]
EPar.PairCong [in DecSyn.fp_red]
EPar.PairEta [in DecSyn.fp_red]
EPar.ProjCong [in DecSyn.fp_red]
EPar.SucCong [in DecSyn.fp_red]
EPar.Univ [in DecSyn.fp_red]
EPar.VarTm [in DecSyn.fp_red]
EPar.ZeroCong [in DecSyn.fp_red]
ERed.AbsCong [in DecSyn.fp_red]
ERed.AppCong0 [in DecSyn.fp_red]
ERed.AppCong1 [in DecSyn.fp_red]
ERed.AppEta [in DecSyn.fp_red]
ERed.BindCong0 [in DecSyn.fp_red]
ERed.BindCong1 [in DecSyn.fp_red]
ERed.IndCong0 [in DecSyn.fp_red]
ERed.IndCong1 [in DecSyn.fp_red]
ERed.IndCong2 [in DecSyn.fp_red]
ERed.IndCong3 [in DecSyn.fp_red]
ERed.PairCong0 [in DecSyn.fp_red]
ERed.PairCong1 [in DecSyn.fp_red]
ERed.PairEta [in DecSyn.fp_red]
ERed.ProjCong [in DecSyn.fp_red]
ERed.SucCong [in DecSyn.fp_red]
E_PairExt [in DecSyn.typing]
E_FunExt [in DecSyn.typing]
E_IndSuc [in DecSyn.typing]
E_IndZero [in DecSyn.typing]
E_ProjPair2 [in DecSyn.typing]
E_ProjPair1 [in DecSyn.typing]
E_AppAbs [in DecSyn.typing]
E_Conv [in DecSyn.typing]
E_SucCong [in DecSyn.typing]
E_IndCong [in DecSyn.typing]
E_Proj2 [in DecSyn.typing]
E_Proj1 [in DecSyn.typing]
E_App [in DecSyn.typing]
E_Bind [in DecSyn.typing]
E_Transitive [in DecSyn.typing]
E_Symmetric [in DecSyn.typing]
E_Refl [in DecSyn.typing]
H
here [in DecSyn.common]HRed.AppAbs [in DecSyn.common]
HRed.AppCong [in DecSyn.common]
HRed.IndCong [in DecSyn.common]
HRed.IndSuc [in DecSyn.common]
HRed.IndZero [in DecSyn.common]
HRed.ProjCong [in DecSyn.common]
HRed.ProjPair [in DecSyn.common]
I
ids [in DecSyn.Autosubst2.unscoped]L
LogRelImpl.InterpExt_Conv [in DecSyn.logrel]LogRelImpl.InterpExt_Step [in DecSyn.logrel]
LogRelImpl.InterpExt_Univ [in DecSyn.logrel]
LogRelImpl.InterpExt_Nat [in DecSyn.logrel]
LogRelImpl.InterpExt_Bind [in DecSyn.logrel]
LogRelImpl.InterpExt_Ne [in DecSyn.logrel]
LoRed.AbsCong [in DecSyn.fp_red]
LoRed.AppAbs [in DecSyn.fp_red]
LoRed.AppCong0 [in DecSyn.fp_red]
LoRed.AppCong1 [in DecSyn.fp_red]
LoRed.BindCong0 [in DecSyn.fp_red]
LoRed.BindCong1 [in DecSyn.fp_red]
LoRed.IndCong0 [in DecSyn.fp_red]
LoRed.IndCong1 [in DecSyn.fp_red]
LoRed.IndCong2 [in DecSyn.fp_red]
LoRed.IndCong3 [in DecSyn.fp_red]
LoRed.IndSuc [in DecSyn.fp_red]
LoRed.IndZero [in DecSyn.fp_red]
LoRed.PairCong0 [in DecSyn.fp_red]
LoRed.PairCong1 [in DecSyn.fp_red]
LoRed.ProjCong [in DecSyn.fp_red]
LoRed.ProjPair [in DecSyn.fp_red]
LoRed.SucCong [in DecSyn.fp_red]
N
NeEPar.AppEta [in DecSyn.fp_red]NeEPar.NAbsCong [in DecSyn.fp_red]
NeEPar.NAppCong [in DecSyn.fp_red]
NeEPar.NBindCong [in DecSyn.fp_red]
NeEPar.NIndCong [in DecSyn.fp_red]
NeEPar.NNatCong [in DecSyn.fp_red]
NeEPar.NPairCong [in DecSyn.fp_red]
NeEPar.NProjCong [in DecSyn.fp_red]
NeEPar.NSucCong [in DecSyn.fp_red]
NeEPar.NUniv [in DecSyn.fp_red]
NeEPar.NVarTm [in DecSyn.fp_red]
NeEPar.NZeroCong [in DecSyn.fp_red]
NeEPar.PairEta [in DecSyn.fp_red]
NeEPar.R_inj [in DecSyn.fp_red]
N_IndCong [in DecSyn.fp_red]
N_IndSuc [in DecSyn.fp_red]
N_IndZero [in DecSyn.fp_red]
N_ProjCong [in DecSyn.fp_red]
N_ProjPairR [in DecSyn.fp_red]
N_ProjPairL [in DecSyn.fp_red]
N_AppL [in DecSyn.fp_red]
N_β [in DecSyn.fp_red]
N_Suc [in DecSyn.fp_red]
N_Zero [in DecSyn.fp_red]
N_Nat [in DecSyn.fp_red]
N_Univ [in DecSyn.fp_red]
N_Bind [in DecSyn.fp_red]
N_Exp [in DecSyn.fp_red]
N_SNe [in DecSyn.fp_red]
N_Abs [in DecSyn.fp_red]
N_Pair [in DecSyn.fp_red]
N_Ind [in DecSyn.fp_red]
N_Proj [in DecSyn.fp_red]
N_App [in DecSyn.fp_red]
N_Var [in DecSyn.fp_red]
R
ren1 [in DecSyn.Autosubst2.unscoped]ren2 [in DecSyn.Autosubst2.unscoped]
ren3 [in DecSyn.Autosubst2.unscoped]
ren4 [in DecSyn.Autosubst2.unscoped]
ren5 [in DecSyn.Autosubst2.unscoped]
RERed.AbsCong [in DecSyn.fp_red]
RERed.AppAbs [in DecSyn.fp_red]
RERed.AppCong0 [in DecSyn.fp_red]
RERed.AppCong1 [in DecSyn.fp_red]
RERed.AppEta [in DecSyn.fp_red]
RERed.BindCong0 [in DecSyn.fp_red]
RERed.BindCong1 [in DecSyn.fp_red]
RERed.IndCong0 [in DecSyn.fp_red]
RERed.IndCong1 [in DecSyn.fp_red]
RERed.IndCong2 [in DecSyn.fp_red]
RERed.IndCong3 [in DecSyn.fp_red]
RERed.IndSuc [in DecSyn.fp_red]
RERed.IndZero [in DecSyn.fp_red]
RERed.PairCong0 [in DecSyn.fp_red]
RERed.PairCong1 [in DecSyn.fp_red]
RERed.PairEta [in DecSyn.fp_red]
RERed.ProjCong [in DecSyn.fp_red]
RERed.ProjPair [in DecSyn.fp_red]
RERed.SucCong [in DecSyn.fp_red]
RPar.AbsCong [in DecSyn.fp_red]
RPar.AppAbs [in DecSyn.fp_red]
RPar.AppCong [in DecSyn.fp_red]
RPar.BindCong [in DecSyn.fp_red]
RPar.IndCong [in DecSyn.fp_red]
RPar.IndSuc [in DecSyn.fp_red]
RPar.IndZero [in DecSyn.fp_red]
RPar.NatCong [in DecSyn.fp_red]
RPar.PairCong [in DecSyn.fp_red]
RPar.ProjCong [in DecSyn.fp_red]
RPar.ProjPair [in DecSyn.fp_red]
RPar.SucCong [in DecSyn.fp_red]
RPar.Univ [in DecSyn.fp_red]
RPar.VarTm [in DecSyn.fp_red]
RPar.ZeroCong [in DecSyn.fp_red]
RRed.AbsCong [in DecSyn.fp_red]
RRed.AppAbs [in DecSyn.fp_red]
RRed.AppCong0 [in DecSyn.fp_red]
RRed.AppCong1 [in DecSyn.fp_red]
RRed.BindCong0 [in DecSyn.fp_red]
RRed.BindCong1 [in DecSyn.fp_red]
RRed.IndCong0 [in DecSyn.fp_red]
RRed.IndCong1 [in DecSyn.fp_red]
RRed.IndCong2 [in DecSyn.fp_red]
RRed.IndCong3 [in DecSyn.fp_red]
RRed.IndSuc [in DecSyn.fp_red]
RRed.IndZero [in DecSyn.fp_red]
RRed.PairCong0 [in DecSyn.fp_red]
RRed.PairCong1 [in DecSyn.fp_red]
RRed.ProjCong [in DecSyn.fp_red]
RRed.ProjPair [in DecSyn.fp_red]
RRed.SucCong [in DecSyn.fp_red]
S
SemWff_cons [in DecSyn.logrel]SemWff_nil [in DecSyn.logrel]
subst1 [in DecSyn.Autosubst2.unscoped]
subst2 [in DecSyn.Autosubst2.unscoped]
subst3 [in DecSyn.Autosubst2.unscoped]
subst4 [in DecSyn.Autosubst2.unscoped]
subst5 [in DecSyn.Autosubst2.unscoped]
Sub1.PiCong [in DecSyn.fp_red]
Sub1.Refl [in DecSyn.fp_red]
Sub1.SigCong [in DecSyn.fp_red]
Sub1.Univ [in DecSyn.fp_red]
Su_Sig_Proj2 [in DecSyn.typing]
Su_Pi_Proj2 [in DecSyn.typing]
Su_Sig_Proj1 [in DecSyn.typing]
Su_Pi_Proj1 [in DecSyn.typing]
Su_Eq [in DecSyn.typing]
Su_Sig [in DecSyn.typing]
Su_Pi [in DecSyn.typing]
Su_Univ [in DecSyn.typing]
Su_Transitive [in DecSyn.typing]
S_Red [in DecSyn.fp_red]
S_Suc [in DecSyn.fp_red]
S_Neu [in DecSyn.fp_red]
S_Zero [in DecSyn.fp_red]
S_HRedR [in DecSyn.common]
S_HRedL [in DecSyn.common]
S_NfNf [in DecSyn.common]
S_Conf [in DecSyn.common]
S_NeuNeu [in DecSyn.common]
S_NatCong [in DecSyn.common]
S_SigCong [in DecSyn.common]
S_PiCong [in DecSyn.common]
S_UnivCong [in DecSyn.common]
T
there [in DecSyn.common]T_Conv [in DecSyn.typing]
T_Ind [in DecSyn.typing]
T_Suc [in DecSyn.typing]
T_Zero [in DecSyn.typing]
T_Nat [in DecSyn.typing]
T_Univ [in DecSyn.typing]
T_Proj2 [in DecSyn.typing]
T_Proj1 [in DecSyn.typing]
T_Pair [in DecSyn.typing]
T_App [in DecSyn.typing]
T_Abs [in DecSyn.typing]
T_Bind [in DecSyn.typing]
T_Var [in DecSyn.typing]
T_Once [in DecSyn.fp_red]
T_Refl [in DecSyn.fp_red]
W
Wff_Cons [in DecSyn.typing]Wff_Nil [in DecSyn.typing]
Lemma Index
A
Abs_Inv [in DecSyn.admissible]Abs_Pi_Inv [in DecSyn.algorithmic]
algo_dom_neu_neu_nonconf [in DecSyn.algorithmic]
algo_dom_hf_hne [in DecSyn.algorithmic]
algo_dom_r_algo_dom [in DecSyn.common]
algo_dom_salgo_dom [in DecSyn.common]
algo_dom_sym [in DecSyn.common]
algo_dom_no_hred [in DecSyn.common]
algo_dom_r_inv [in DecSyn.common]
App_Inv [in DecSyn.admissible]
A_Conf' [in DecSyn.algorithmic]
A_HRedR' [in DecSyn.common]
A_HRedsR [in DecSyn.common]
A_HRedsL [in DecSyn.common]
B
Bind_Univ_Inv [in DecSyn.algorithmic]bind_inst [in DecSyn.structural]
Bind_Inv [in DecSyn.structural]
C
ce_neu_neu_helper [in DecSyn.algorithmic]CE_Nf [in DecSyn.algorithmic]
CE_HRedR [in DecSyn.algorithmic]
CE_HRedL [in DecSyn.algorithmic]
check_sub_hredr [in DecSyn.executable]
check_sub_hredl [in DecSyn.executable]
check_sub_irrel [in DecSyn.executable]
check_sub_conf [in DecSyn.executable]
check_sub_neuneu [in DecSyn.executable]
check_sub_nfnf [in DecSyn.executable]
check_sub_univ_univ [in DecSyn.executable]
check_sub_sig_sig [in DecSyn.executable]
check_sub_pi_pi [in DecSyn.executable]
check_equal_conf [in DecSyn.executable]
check_equal_univ [in DecSyn.executable]
check_equal_hredr [in DecSyn.executable]
check_equal_ind_ind [in DecSyn.executable]
check_equal_app_app [in DecSyn.executable]
check_equal_proj_proj [in DecSyn.executable]
check_equal_bind_bind [in DecSyn.executable]
check_equal_neu_pair [in DecSyn.executable]
check_equal_pair_neu [in DecSyn.executable]
check_equal_pair_pair [in DecSyn.executable]
check_equal_neu_abs [in DecSyn.executable]
check_equal_abs_neu [in DecSyn.executable]
check_equal_abs_abs [in DecSyn.executable]
check_equal_hredl [in DecSyn.executable]
check_equal_irrel [in DecSyn.executable]
check_equal_nfnf [in DecSyn.executable]
check_sub_complete [in DecSyn.executable_correct]
check_sub_sound [in DecSyn.executable_correct]
check_equal_complete [in DecSyn.executable_correct]
check_equal_sound [in DecSyn.executable_correct]
CLE_HRedR [in DecSyn.algorithmic]
CLE_HRedL [in DecSyn.algorithmic]
Conv_dec [in DecSyn.conv_dec]
coqeqr_no_hred [in DecSyn.executable_correct]
coqeq_complete [in DecSyn.algorithmic]
coqeq_sound [in DecSyn.algorithmic]
coqeq_complete' [in DecSyn.algorithmic]
coqeq_sound_mutual [in DecSyn.algorithmic]
coqeq_symmetric_mutual [in DecSyn.algorithmic]
coqeq_neuneu' [in DecSyn.executable_correct]
coqeq_neuneu [in DecSyn.executable_correct]
coqeq_no_hred [in DecSyn.executable_correct]
coqleq_sound [in DecSyn.algorithmic]
coqleq_complete [in DecSyn.algorithmic]
coqleq_complete_unty [in DecSyn.algorithmic]
coqleq_complete' [in DecSyn.algorithmic]
coqleq_sound_mutual [in DecSyn.algorithmic]
coqleq_no_hred [in DecSyn.executable_correct]
Core.congr_PInd [in DecSyn.Autosubst2.syntax]
Core.congr_PSuc [in DecSyn.Autosubst2.syntax]
Core.congr_PZero [in DecSyn.Autosubst2.syntax]
Core.congr_PNat [in DecSyn.Autosubst2.syntax]
Core.congr_PUniv [in DecSyn.Autosubst2.syntax]
Core.congr_PBind [in DecSyn.Autosubst2.syntax]
Core.congr_PProj [in DecSyn.Autosubst2.syntax]
Core.congr_PPair [in DecSyn.Autosubst2.syntax]
Core.congr_PApp [in DecSyn.Autosubst2.syntax]
Core.congr_PAbs [in DecSyn.Autosubst2.syntax]
Core.congr_PR [in DecSyn.Autosubst2.syntax]
Core.congr_PL [in DecSyn.Autosubst2.syntax]
Core.congr_PSig [in DecSyn.Autosubst2.syntax]
Core.congr_PPi [in DecSyn.Autosubst2.syntax]
Core.instId'_PTm_pointwise [in DecSyn.Autosubst2.syntax]
Core.instId'_PTm [in DecSyn.Autosubst2.syntax]
Core.renRen_PTm [in DecSyn.Autosubst2.syntax]
Core.renRen'_PTm_pointwise [in DecSyn.Autosubst2.syntax]
Core.renSubst_PTm_pointwise [in DecSyn.Autosubst2.syntax]
Core.renSubst_PTm [in DecSyn.Autosubst2.syntax]
Core.rinstId'_PTm_pointwise [in DecSyn.Autosubst2.syntax]
Core.rinstId'_PTm [in DecSyn.Autosubst2.syntax]
Core.rinstInst_up_PTm_PTm [in DecSyn.Autosubst2.syntax]
Core.rinstInst'_PTm_pointwise [in DecSyn.Autosubst2.syntax]
Core.rinstInst'_PTm [in DecSyn.Autosubst2.syntax]
Core.substRen_PTm_pointwise [in DecSyn.Autosubst2.syntax]
Core.substRen_PTm [in DecSyn.Autosubst2.syntax]
Core.substSubst_PTm_pointwise [in DecSyn.Autosubst2.syntax]
Core.substSubst_PTm [in DecSyn.Autosubst2.syntax]
Core.upExtRen_PTm_PTm [in DecSyn.Autosubst2.syntax]
Core.upExt_PTm_PTm [in DecSyn.Autosubst2.syntax]
Core.upId_PTm_PTm [in DecSyn.Autosubst2.syntax]
Core.upRen_PTm_PTm [in DecSyn.Autosubst2.syntax]
Core.up_subst_subst_PTm_PTm [in DecSyn.Autosubst2.syntax]
Core.up_subst_ren_PTm_PTm [in DecSyn.Autosubst2.syntax]
Core.up_ren_subst_PTm_PTm [in DecSyn.Autosubst2.syntax]
Core.up_ren_ren_PTm_PTm [in DecSyn.Autosubst2.syntax]
Core.up_PTm_PTm [in DecSyn.Autosubst2.syntax]
Core.varLRen'_PTm_pointwise [in DecSyn.Autosubst2.syntax]
Core.varLRen'_PTm [in DecSyn.Autosubst2.syntax]
Core.varL'_PTm_pointwise [in DecSyn.Autosubst2.syntax]
Core.varL'_PTm [in DecSyn.Autosubst2.syntax]
ctx_eq_subst_one [in DecSyn.structural]
Cumulativity [in DecSyn.structural]
D
DJoin.AbsCong [in DecSyn.fp_red]DJoin.abs_inj [in DecSyn.fp_red]
DJoin.AppCong [in DecSyn.fp_red]
DJoin.BindCong [in DecSyn.fp_red]
DJoin.bind_inj [in DecSyn.fp_red]
DJoin.bind_univ_noconf [in DecSyn.fp_red]
DJoin.cong [in DecSyn.fp_red]
DJoin.cong' [in DecSyn.fp_red]
DJoin.ejoin_abs_inj [in DecSyn.fp_red]
DJoin.ejoin_pair_inj [in DecSyn.fp_red]
DJoin.FromEJoin [in DecSyn.fp_red]
DJoin.FromRedSNs [in DecSyn.fp_red]
DJoin.FromRReds [in DecSyn.fp_red]
DJoin.FromRRed0 [in DecSyn.fp_red]
DJoin.FromRRed1 [in DecSyn.fp_red]
DJoin.hne_proj_inj [in DecSyn.fp_red]
DJoin.hne_app_inj [in DecSyn.fp_red]
DJoin.hne_nat_noconf [in DecSyn.fp_red]
DJoin.hne_bind_noconf [in DecSyn.fp_red]
DJoin.hne_univ_noconf [in DecSyn.fp_red]
DJoin.IndCong [in DecSyn.fp_red]
DJoin.PairCong [in DecSyn.fp_red]
DJoin.pair_inj [in DecSyn.fp_red]
DJoin.ProjCong [in DecSyn.fp_red]
DJoin.refl [in DecSyn.fp_red]
DJoin.renaming [in DecSyn.fp_red]
DJoin.sne_univ_noconf [in DecSyn.fp_red]
DJoin.sne_bind_noconf [in DecSyn.fp_red]
DJoin.sne_nat_noconf [in DecSyn.fp_red]
DJoin.standardization [in DecSyn.fp_red]
DJoin.standardization_lo [in DecSyn.fp_red]
DJoin.substing [in DecSyn.fp_red]
DJoin.SucCong [in DecSyn.fp_red]
DJoin.suc_inj [in DecSyn.fp_red]
DJoin.symmetric [in DecSyn.fp_red]
DJoin.ToEJoin [in DecSyn.fp_red]
DJoin.transitive [in DecSyn.fp_red]
DJoin.univ_inj [in DecSyn.fp_red]
DJoin.var_inj [in DecSyn.fp_red]
DJoin.weakening [in DecSyn.fp_red]
E
EJoin.bind_inj [in DecSyn.fp_red]EJoin.hne_proj_inj [in DecSyn.fp_red]
EJoin.hne_app_inj [in DecSyn.fp_red]
EJoin.ind_inj [in DecSyn.fp_red]
EJoin.suc_inj [in DecSyn.fp_red]
epar_sn_preservation [in DecSyn.fp_red]
EPar.AppEta' [in DecSyn.fp_red]
EPar.morphing [in DecSyn.fp_red]
EPar.morphing_up [in DecSyn.fp_red]
EPar.morphing_ext [in DecSyn.fp_red]
EPar.morphing_ren [in DecSyn.fp_red]
EPar.refl [in DecSyn.fp_red]
EPar.renaming [in DecSyn.fp_red]
EPar.substing [in DecSyn.fp_red]
EReds.AbsCong [in DecSyn.fp_red]
EReds.AppCong [in DecSyn.fp_red]
EReds.app_inv [in DecSyn.fp_red]
EReds.BindCong [in DecSyn.fp_red]
EReds.bind_inv [in DecSyn.fp_red]
EReds.FromEPar [in DecSyn.fp_red]
EReds.FromEPars [in DecSyn.fp_red]
EReds.IndCong [in DecSyn.fp_red]
EReds.ind_inv [in DecSyn.fp_red]
EReds.PairCong [in DecSyn.fp_red]
EReds.ProjCong [in DecSyn.fp_red]
EReds.proj_inv [in DecSyn.fp_red]
EReds.renaming [in DecSyn.fp_red]
EReds.substing [in DecSyn.fp_red]
EReds.SucCong [in DecSyn.fp_red]
EReds.suc_inv [in DecSyn.fp_red]
EReds.zero_inv [in DecSyn.fp_red]
ered_confluence [in DecSyn.fp_red]
ered_local_confluence [in DecSyn.fp_red]
ered_sn [in DecSyn.fp_red]
ered_size [in DecSyn.fp_red]
ERed.abs_back_preservation [in DecSyn.fp_red]
ERed.antirenaming [in DecSyn.fp_red]
ERed.AppEta' [in DecSyn.fp_red]
ERed.nf_preservation [in DecSyn.fp_red]
ERed.renaming [in DecSyn.fp_red]
ERed.substing [in DecSyn.fp_red]
ERed.subst_differ_one_ren_up [in DecSyn.fp_red]
ERed.tm_free_ren_any [in DecSyn.fp_red]
ERed.ToEPar [in DecSyn.fp_red]
ESub.pi_inj [in DecSyn.fp_red]
ESub.sig_inj [in DecSyn.fp_red]
ESub.suc_inj [in DecSyn.fp_red]
E_PairEta [in DecSyn.admissible]
E_ProjPair2 [in DecSyn.admissible]
E_ProjPair1 [in DecSyn.admissible]
E_AppEta [in DecSyn.admissible]
E_PairExt [in DecSyn.admissible]
E_FunExt [in DecSyn.admissible]
E_Proj2 [in DecSyn.admissible]
E_App [in DecSyn.admissible]
E_Bind [in DecSyn.admissible]
E_AppAbs [in DecSyn.admissible]
E_Pair [in DecSyn.preservation]
E_Abs [in DecSyn.preservation]
E_Conv_E [in DecSyn.algorithmic]
E_IndSuc' [in DecSyn.structural]
E_IndZero' [in DecSyn.structural]
E_ProjPair2' [in DecSyn.structural]
E_AppAbs' [in DecSyn.structural]
E_App' [in DecSyn.structural]
E_Bind' [in DecSyn.structural]
E_Proj2' [in DecSyn.structural]
E_IndCong' [in DecSyn.structural]
F
funcomp_assoc [in DecSyn.Autosubst2.core]fundamental_theorem [in DecSyn.soundness]
H
here' [in DecSyn.common]hf_not_hne [in DecSyn.algorithmic]
hf_hred_lored [in DecSyn.algorithmic]
hf_no_hred [in DecSyn.common]
hne_ind_inj [in DecSyn.algorithmic]
hne_nf_ne [in DecSyn.algorithmic]
hne_no_hred [in DecSyn.common]
hreds_nf_refl [in DecSyn.common]
HReds.preservation [in DecSyn.algorithmic]
HReds.ToEq [in DecSyn.algorithmic]
hred_none [in DecSyn.executable]
hred_hne [in DecSyn.algorithmic]
hred_deter [in DecSyn.common]
hred_sound [in DecSyn.common]
hred_complete [in DecSyn.common]
HRed.preservation [in DecSyn.algorithmic]
HRed.ToEq [in DecSyn.algorithmic]
HRed.ToRRed [in DecSyn.algorithmic]
I
Ind_Inv [in DecSyn.preservation]L
LogRelFactsImpl.adequacy [in DecSyn.logrel]LogRelFactsImpl.back_closs [in DecSyn.logrel]
LogRelFactsImpl.back_clos [in DecSyn.logrel]
LogRelFactsImpl.bindspace_impl [in DecSyn.logrel]
LogRelFactsImpl.Bind_nopf [in DecSyn.logrel]
LogRelFactsImpl.Bind_inv_nopf [in DecSyn.logrel]
LogRelFactsImpl.Bind_inv [in DecSyn.logrel]
LogRelFactsImpl.case [in DecSyn.logrel]
LogRelFactsImpl.CR_SNat [in DecSyn.logrel]
LogRelFactsImpl.CR_okay [in DecSyn.logrel]
LogRelFactsImpl.cumulative [in DecSyn.logrel]
LogRelFactsImpl.functional [in DecSyn.logrel]
LogRelFactsImpl.InterpUniv_Functional [in DecSyn.logrel]
LogRelFactsImpl.InterpUniv_Join [in DecSyn.logrel]
LogRelFactsImpl.join [in DecSyn.logrel]
LogRelFactsImpl.Nat_inv [in DecSyn.logrel]
LogRelFactsImpl.N_Exps [in DecSyn.logrel]
LogRelFactsImpl.SNe_inv [in DecSyn.logrel]
LogRelFactsImpl.sub [in DecSyn.logrel]
LogRelFactsImpl.sub' [in DecSyn.logrel]
LogRelFactsImpl.sub0 [in DecSyn.logrel]
LogRelFactsImpl.Univ_inv [in DecSyn.logrel]
LogRelImpl.InterpExt_lt_eq [in DecSyn.logrel]
LogRelImpl.InterpExt_lt_impl [in DecSyn.logrel]
LogRelImpl.InterpExt_Univ' [in DecSyn.logrel]
LogRelImpl.InterpUniv_Conv [in DecSyn.logrel]
LogRelImpl.InterpUniv_Nat [in DecSyn.logrel]
LogRelImpl.InterpUniv_Step [in DecSyn.logrel]
LogRelImpl.InterpUniv_Univ [in DecSyn.logrel]
LogRelImpl.InterpUniv_Bind [in DecSyn.logrel]
LogRelImpl.InterpUniv_Ne [in DecSyn.logrel]
LogRelImpl.InterpUniv_ind [in DecSyn.logrel]
LogRelImpl.InterpUniv_nolt [in DecSyn.logrel]
LogRelImpl.InterpUniv_rec_nolt [in DecSyn.logrel]
LogRelImpl.InterpUniv_rec_acc_irrel [in DecSyn.logrel]
lookup_deter [in DecSyn.common]
loreds_hne_preservation [in DecSyn.algorithmic]
loreds_embed [in DecSyn.algorithmic]
LoReds.AbsCong [in DecSyn.fp_red]
LoReds.AppCong [in DecSyn.fp_red]
LoReds.BindCong [in DecSyn.fp_red]
LoReds.FromSN [in DecSyn.fp_red]
LoReds.FromSN_mutual [in DecSyn.fp_red]
LoReds.hf_ne_imp [in DecSyn.fp_red]
LoReds.hf_preservation [in DecSyn.fp_red]
LoReds.IndCong [in DecSyn.fp_red]
LoReds.PairCong [in DecSyn.fp_red]
LoReds.ProjCong [in DecSyn.fp_red]
LoReds.SucCong [in DecSyn.fp_red]
LoReds.ToRReds [in DecSyn.fp_red]
lored_nsteps_pair_inv [in DecSyn.algorithmic]
lored_nsteps_proj_cong [in DecSyn.algorithmic]
lored_nsteps_app_cong [in DecSyn.algorithmic]
lored_nsteps_proj_inv [in DecSyn.algorithmic]
lored_nsteps_app_inv [in DecSyn.algorithmic]
lored_nsteps_ind_inv [in DecSyn.algorithmic]
lored_nsteps_bind_inv [in DecSyn.algorithmic]
lored_hne_preservation [in DecSyn.algorithmic]
lored_nsteps_abs_inv [in DecSyn.algorithmic]
lored_nsteps_suc_inv [in DecSyn.algorithmic]
lored_nsteps_renaming [in DecSyn.algorithmic]
lored_embed [in DecSyn.algorithmic]
LoRed.AppAbs' [in DecSyn.fp_red]
LoRed.hf_preservation [in DecSyn.fp_red]
LoRed.IndSuc' [in DecSyn.fp_red]
LoRed.renaming [in DecSyn.fp_red]
LoRed.ToRRed [in DecSyn.fp_red]
M
morphing [in DecSyn.structural]morphing_id [in DecSyn.structural]
morphing_wt' [in DecSyn.structural]
morphing_wt [in DecSyn.structural]
morphing_up [in DecSyn.structural]
morphing_ext [in DecSyn.structural]
morphing_ren [in DecSyn.structural]
morphing_SemWt_Univ [in DecSyn.logrel]
morphing_SemWt [in DecSyn.logrel]
N
Nat_Inv [in DecSyn.algorithmic]NeEPars.R_nonelim_nf [in DecSyn.fp_red]
NeEPars.ToEReds [in DecSyn.fp_red]
NeEPar.R_elim_nonelim [in DecSyn.fp_red]
NeEPar.R_nonelim_nothf [in DecSyn.fp_red]
NeEPar.R_elim_nf [in DecSyn.fp_red]
NeEPar.ToEPar [in DecSyn.fp_red]
ne_nf_embed [in DecSyn.fp_red]
ne_nf_ren [in DecSyn.fp_red]
ne_nf [in DecSyn.fp_red]
ne_hne [in DecSyn.algorithmic]
NoForbid_Fact.P_RReds [in DecSyn.fp_red]
NoForbid_Fact.P_EPars [in DecSyn.fp_red]
nostuck_antisubstitution [in DecSyn.cosn]
N_IndSuc' [in DecSyn.fp_red]
N_β' [in DecSyn.fp_red]
N_Projs [in DecSyn.logrel]
P
Pair_Inv [in DecSyn.admissible]Pair_Sig_Inv [in DecSyn.algorithmic]
PAppBind_imp [in DecSyn.fp_red]
PAppPair_imp [in DecSyn.fp_red]
PApp_imp [in DecSyn.fp_red]
PInd_imp [in DecSyn.fp_red]
pointwise_forall [in DecSyn.Autosubst2.core]
PProjAbs_imp [in DecSyn.fp_red]
PProjBind_imp [in DecSyn.fp_red]
PProj_imp [in DecSyn.fp_red]
Proj1_Inv [in DecSyn.admissible]
Proj2_Inv [in DecSyn.admissible]
R
redsns_preservation [in DecSyn.logrel]redsn_preservation_mutual [in DecSyn.logrel]
red_uniquenf [in DecSyn.fp_red]
red_confluence [in DecSyn.fp_red]
red_sn_preservation [in DecSyn.fp_red]
regularity [in DecSyn.structural]
regularity_sub0 [in DecSyn.structural]
renaming [in DecSyn.structural]
renaming_comp [in DecSyn.admissible]
renaming_su' [in DecSyn.structural]
renaming_wt' [in DecSyn.structural]
renaming_wt [in DecSyn.structural]
renaming_up [in DecSyn.structural]
renaming_shift [in DecSyn.common]
renaming_SemWt [in DecSyn.logrel]
ren_injective [in DecSyn.common]
REReds.AbsCong [in DecSyn.fp_red]
REReds.AppCong [in DecSyn.fp_red]
REReds.BindCong [in DecSyn.fp_red]
REReds.bind_inv [in DecSyn.fp_red]
REReds.bind_preservation [in DecSyn.fp_red]
REReds.cong [in DecSyn.fp_red]
REReds.cong_up2 [in DecSyn.fp_red]
REReds.cong_up [in DecSyn.fp_red]
REReds.cong' [in DecSyn.fp_red]
REReds.FromEReds [in DecSyn.fp_red]
REReds.FromRReds [in DecSyn.fp_red]
REReds.hne_ind_inv [in DecSyn.fp_red]
REReds.hne_proj_inv [in DecSyn.fp_red]
REReds.hne_app_inv [in DecSyn.fp_red]
REReds.hne_preservation [in DecSyn.fp_red]
REReds.IndCong [in DecSyn.fp_red]
REReds.nat_inv [in DecSyn.fp_red]
REReds.nat_preservation [in DecSyn.fp_red]
REReds.PairCong [in DecSyn.fp_red]
REReds.ProjCong [in DecSyn.fp_red]
REReds.sne_preservation [in DecSyn.fp_red]
REReds.sn_preservation [in DecSyn.fp_red]
REReds.substing [in DecSyn.fp_red]
REReds.SucCong [in DecSyn.fp_red]
REReds.suc_inv [in DecSyn.fp_red]
REReds.ToEReds [in DecSyn.fp_red]
REReds.univ_inv [in DecSyn.fp_red]
REReds.univ_preservation [in DecSyn.fp_red]
REReds.var_inv [in DecSyn.fp_red]
REReds.zero_inv [in DecSyn.fp_red]
rered_confluence [in DecSyn.fp_red]
rered_standardization' [in DecSyn.fp_red]
rered_standardization [in DecSyn.fp_red]
RERed.bind_preservation [in DecSyn.fp_red]
RERed.FromBeta [in DecSyn.fp_red]
RERed.FromEta [in DecSyn.fp_red]
RERed.hne_preservation [in DecSyn.fp_red]
RERed.nat_preservation [in DecSyn.fp_red]
RERed.sne_preservation [in DecSyn.fp_red]
RERed.sn_preservation [in DecSyn.fp_red]
RERed.substing [in DecSyn.fp_red]
RERed.ToBetaEta [in DecSyn.fp_red]
RERed.ToBetaEtaPar [in DecSyn.fp_red]
RERed.univ_preservation [in DecSyn.fp_red]
RPar.AppAbs' [in DecSyn.fp_red]
RPar.cong [in DecSyn.fp_red]
RPar.diamond [in DecSyn.fp_red]
RPar.FromRRed [in DecSyn.fp_red]
RPar.IndSuc' [in DecSyn.fp_red]
RPar.morphing [in DecSyn.fp_red]
RPar.morphing_up [in DecSyn.fp_red]
RPar.morphing_ext [in DecSyn.fp_red]
RPar.morphing_ren [in DecSyn.fp_red]
RPar.ProjPair' [in DecSyn.fp_red]
RPar.refl [in DecSyn.fp_red]
RPar.renaming [in DecSyn.fp_red]
RPar.substing [in DecSyn.fp_red]
RPar.triangle [in DecSyn.fp_red]
RReds.AbsCong [in DecSyn.fp_red]
RReds.abs_preservation [in DecSyn.fp_red]
RReds.AppCong [in DecSyn.fp_red]
RReds.BindCong [in DecSyn.fp_red]
RReds.FromRedSNs [in DecSyn.fp_red]
RReds.FromRPar [in DecSyn.fp_red]
RReds.IndCong [in DecSyn.fp_red]
RReds.nf_refl [in DecSyn.fp_red]
RReds.PairCong [in DecSyn.fp_red]
RReds.ProjCong [in DecSyn.fp_red]
RReds.renaming [in DecSyn.fp_red]
RReds.RParIff [in DecSyn.fp_red]
RReds.SucCong [in DecSyn.fp_red]
RRed_Eq [in DecSyn.preservation]
RRed.abs_preservation [in DecSyn.fp_red]
RRed.antirenaming [in DecSyn.fp_red]
RRed.AppAbs' [in DecSyn.fp_red]
RRed.FromRedSN [in DecSyn.fp_red]
RRed.IndSuc' [in DecSyn.fp_red]
RRed.nf_imp [in DecSyn.fp_red]
RRed.renaming [in DecSyn.fp_red]
RRed.substing [in DecSyn.fp_red]
S
Safe_NoForbid.P_IndInv [in DecSyn.cosn]Safe_NoForbid.P_renaming [in DecSyn.cosn]
Safe_NoForbid.P_AbsInv [in DecSyn.cosn]
Safe_NoForbid.P_SucInv [in DecSyn.cosn]
Safe_NoForbid.P_BindInv [in DecSyn.cosn]
Safe_NoForbid.P_ProjInv [in DecSyn.cosn]
Safe_NoForbid.P_PairInv [in DecSyn.cosn]
Safe_NoForbid.P_AppInv [in DecSyn.cosn]
Safe_NoForbid.PInd_imp [in DecSyn.cosn]
Safe_NoForbid.PProj_imp [in DecSyn.cosn]
Safe_NoForbid.PApp_imp [in DecSyn.cosn]
Safe_NoForbid.P_RRed [in DecSyn.cosn]
Safe_NoForbid.P_EPar [in DecSyn.cosn]
safe_omega [in DecSyn.cosn]
safe_rereds [in DecSyn.cosn]
safe_rered [in DecSyn.cosn]
safe_rred [in DecSyn.cosn]
safe_ind_imp [in DecSyn.cosn]
safe_proj_imp [in DecSyn.cosn]
safe_app_imp [in DecSyn.cosn]
safe_suc_inv [in DecSyn.cosn]
safe_pair_inv1 [in DecSyn.cosn]
safe_pair_inv0 [in DecSyn.cosn]
safe_bind_inv1 [in DecSyn.cosn]
safe_bind_inv0 [in DecSyn.cosn]
safe_ind_inv3 [in DecSyn.cosn]
safe_ind_inv2 [in DecSyn.cosn]
safe_ind_inv1 [in DecSyn.cosn]
safe_ind_inv0 [in DecSyn.cosn]
safe_proj_inv [in DecSyn.cosn]
safe_abs_inv [in DecSyn.cosn]
safe_app_inv1 [in DecSyn.cosn]
safe_app_inv0 [in DecSyn.cosn]
safe_antisubstitution [in DecSyn.cosn]
safe_coind [in DecSyn.cosn]
salgo_dom_no_hred [in DecSyn.common]
salgo_dom_r_inv [in DecSyn.common]
SBind_inst [in DecSyn.logrel]
SBind_inv1 [in DecSyn.logrel]
scons_comp' [in DecSyn.Autosubst2.unscoped]
scons_eta_id' [in DecSyn.Autosubst2.unscoped]
scons_eta' [in DecSyn.Autosubst2.unscoped]
SemEq_SN_Join [in DecSyn.logrel]
SemEq_SemWt [in DecSyn.logrel]
SemLEq_SN_Sub [in DecSyn.logrel]
SemLEq_SemWt [in DecSyn.logrel]
SemWff_lookup [in DecSyn.logrel]
SemWt_SN [in DecSyn.logrel]
SemWt_SemLEq [in DecSyn.logrel]
SemWt_SemEq [in DecSyn.logrel]
SemWt_Univ [in DecSyn.logrel]
SE_App [in DecSyn.logrel]
SE_Nat [in DecSyn.logrel]
SE_FunExt [in DecSyn.logrel]
SE_PairExt [in DecSyn.logrel]
SE_PairEta [in DecSyn.logrel]
SE_ProjPair2 [in DecSyn.logrel]
SE_ProjPair1 [in DecSyn.logrel]
SE_IndSuc [in DecSyn.logrel]
SE_IndZero [in DecSyn.logrel]
SE_IndCong [in DecSyn.logrel]
SE_SucCong [in DecSyn.logrel]
SE_Proj2 [in DecSyn.logrel]
SE_Proj1 [in DecSyn.logrel]
SE_Pair [in DecSyn.logrel]
SE_Conv [in DecSyn.logrel]
SE_Conv' [in DecSyn.logrel]
SE_AppAbs [in DecSyn.logrel]
SE_AppEta [in DecSyn.logrel]
SE_Abs [in DecSyn.logrel]
SE_Bind [in DecSyn.logrel]
SE_Bind' [in DecSyn.logrel]
SE_Transitive [in DecSyn.logrel]
SE_Symmetric [in DecSyn.logrel]
SE_Refl [in DecSyn.logrel]
size_PTm_ren [in DecSyn.fp_red]
smorphing_ext [in DecSyn.logrel]
smorphing_ren [in DecSyn.logrel]
smorphing_ok_refl [in DecSyn.logrel]
SNat_SN [in DecSyn.logrel]
SN_NoForbid.P_IndInv [in DecSyn.fp_red]
SN_NoForbid.P_renaming [in DecSyn.fp_red]
SN_NoForbid.P_AbsInv [in DecSyn.fp_red]
SN_NoForbid.P_SucInv [in DecSyn.fp_red]
SN_NoForbid.P_BindInv [in DecSyn.fp_red]
SN_NoForbid.P_ProjInv [in DecSyn.fp_red]
SN_NoForbid.P_PairInv [in DecSyn.fp_red]
SN_NoForbid.P_AppInv [in DecSyn.fp_red]
SN_NoForbid.PInd_imp [in DecSyn.fp_red]
SN_NoForbid.PProj_imp [in DecSyn.fp_red]
SN_NoForbid.PApp_imp [in DecSyn.fp_red]
SN_NoForbid.P_RRed [in DecSyn.fp_red]
SN_NoForbid.P_EPar [in DecSyn.fp_red]
SN_IndInv [in DecSyn.fp_red]
SN_ProjInv [in DecSyn.fp_red]
SN_AppInv [in DecSyn.fp_red]
sn_unmorphing [in DecSyn.fp_red]
sn_antirenaming [in DecSyn.fp_red]
sn_renaming [in DecSyn.fp_red]
SN_Proj [in DecSyn.fp_red]
sn_algo_dom [in DecSyn.algorithmic]
sn_term_metric [in DecSyn.algorithmic]
sn_bot_up2 [in DecSyn.logrel]
sn_bot_up [in DecSyn.logrel]
sn_unmorphing' [in DecSyn.logrel]
SSu_Sig_Proj2 [in DecSyn.logrel]
SSu_Pi_Proj2 [in DecSyn.logrel]
SSu_Sig_Proj1 [in DecSyn.logrel]
SSu_Pi_Proj1 [in DecSyn.logrel]
SSu_Sig [in DecSyn.logrel]
SSu_Pi [in DecSyn.logrel]
SSu_Univ [in DecSyn.logrel]
SSu_Transitive [in DecSyn.logrel]
SSu_Eq [in DecSyn.logrel]
stm_conf_sym [in DecSyn.common]
stm_tm_nonconf [in DecSyn.common]
ST_Univ [in DecSyn.logrel]
ST_Univ' [in DecSyn.logrel]
ST_Ind [in DecSyn.logrel]
ST_Suc [in DecSyn.logrel]
ST_Zero [in DecSyn.logrel]
ST_Nat [in DecSyn.logrel]
ST_Conv [in DecSyn.logrel]
ST_Conv_E [in DecSyn.logrel]
ST_Conv' [in DecSyn.logrel]
ST_Proj2 [in DecSyn.logrel]
ST_Proj1 [in DecSyn.logrel]
ST_Pair [in DecSyn.logrel]
ST_App' [in DecSyn.logrel]
ST_App [in DecSyn.logrel]
ST_Abs [in DecSyn.logrel]
ST_Bind [in DecSyn.logrel]
ST_Bind' [in DecSyn.logrel]
ST_Var [in DecSyn.logrel]
ST_Var' [in DecSyn.logrel]
subject_reduction [in DecSyn.preservation]
substing_wt [in DecSyn.structural]
subst_scons_id [in DecSyn.common]
subvar_inj [in DecSyn.algorithmic]
Sub_Bind_InvL [in DecSyn.algorithmic]
Sub_Univ_InvR [in DecSyn.algorithmic]
Sub_Bind_InvR [in DecSyn.algorithmic]
Sub.bind_inj [in DecSyn.fp_red]
Sub.bind_univ_noconf [in DecSyn.fp_red]
Sub.bind_nat_noconf [in DecSyn.fp_red]
Sub.bind_sne_noconf [in DecSyn.fp_red]
Sub.cong [in DecSyn.fp_red]
Sub.FromJoin [in DecSyn.fp_red]
Sub.hne_bind_noconf [in DecSyn.fp_red]
Sub.nat_bind_noconf [in DecSyn.fp_red]
Sub.nat_univ_noconf [in DecSyn.fp_red]
Sub.nat_sne_noconf [in DecSyn.fp_red]
Sub.PiCong [in DecSyn.fp_red]
Sub.refl [in DecSyn.fp_red]
Sub.SigCong [in DecSyn.fp_red]
Sub.sne_univ_noconf [in DecSyn.fp_red]
Sub.sne_bind_noconf [in DecSyn.fp_red]
Sub.sne_nat_noconf [in DecSyn.fp_red]
Sub.standardization [in DecSyn.fp_red]
Sub.standardization_lo [in DecSyn.fp_red]
Sub.substing [in DecSyn.fp_red]
Sub.suc_inj [in DecSyn.fp_red]
Sub.ToESub [in DecSyn.fp_red]
Sub.ToJoin [in DecSyn.fp_red]
Sub.transitive [in DecSyn.fp_red]
Sub.UnivCong [in DecSyn.fp_red]
Sub.univ_inj [in DecSyn.fp_red]
Sub.univ_bind_noconf [in DecSyn.fp_red]
Sub.univ_nat_noconf [in DecSyn.fp_red]
Sub.univ_sne_noconf [in DecSyn.fp_red]
Sub1.bind_preservation [in DecSyn.fp_red]
Sub1.commutativity_Rs [in DecSyn.fp_red]
Sub1.commutativity_Ls [in DecSyn.fp_red]
Sub1.commutativity0 [in DecSyn.fp_red]
Sub1.hne_refl [in DecSyn.fp_red]
Sub1.refl [in DecSyn.fp_red]
Sub1.renaming [in DecSyn.fp_red]
Sub1.sne_preservation [in DecSyn.fp_red]
Sub1.sn_preservation [in DecSyn.fp_red]
Sub1.substing [in DecSyn.fp_red]
Sub1.transitive [in DecSyn.fp_red]
Sub1.transitive0 [in DecSyn.fp_red]
Sub1.univ_preservation [in DecSyn.fp_red]
Suc_Inv [in DecSyn.preservation]
Su_Sig_Proj2_Var [in DecSyn.structural]
Su_Pi_Proj2_Var [in DecSyn.structural]
Su_Sig_Proj2' [in DecSyn.structural]
Su_Pi_Proj2' [in DecSyn.structural]
Su_Wt [in DecSyn.structural]
synsub_to_usub [in DecSyn.soundness]
S_HRedR' [in DecSyn.common]
S_HRedsR [in DecSyn.common]
S_HRedsL [in DecSyn.common]
T
term_metric_algo_dom [in DecSyn.algorithmic]term_metric_ind [in DecSyn.algorithmic]
term_metric_proj [in DecSyn.algorithmic]
term_metric_app [in DecSyn.algorithmic]
term_metric_pair_neu [in DecSyn.algorithmic]
term_metric_abs_neu [in DecSyn.algorithmic]
term_metric_suc [in DecSyn.algorithmic]
term_metric_bind [in DecSyn.algorithmic]
term_metric_pair [in DecSyn.algorithmic]
term_metric_abs [in DecSyn.algorithmic]
term_metric_case [in DecSyn.algorithmic]
term_metric_sym [in DecSyn.algorithmic]
there' [in DecSyn.common]
tm_conf_sym [in DecSyn.common]
tm_stm_conf [in DecSyn.common]
T_Eta [in DecSyn.admissible]
T_Abs [in DecSyn.admissible]
T_AbsBind_Imp [in DecSyn.algorithmic]
T_PairUniv_Imp' [in DecSyn.algorithmic]
T_SucUniv_Imp' [in DecSyn.algorithmic]
T_ZeroUniv_Imp' [in DecSyn.algorithmic]
T_AbsUniv_Imp' [in DecSyn.algorithmic]
T_AbsUniv_Imp [in DecSyn.algorithmic]
T_PairUniv_Imp [in DecSyn.algorithmic]
T_PairSuc_Imp [in DecSyn.algorithmic]
T_PairZero_Imp [in DecSyn.algorithmic]
T_PairNat_Imp [in DecSyn.algorithmic]
T_PairBind_Imp [in DecSyn.algorithmic]
T_AbsNat_Imp [in DecSyn.algorithmic]
T_AbsSuc_Imp [in DecSyn.algorithmic]
T_AbsZero_Imp [in DecSyn.algorithmic]
T_AbsPair_Imp [in DecSyn.algorithmic]
T_Univ_Raise [in DecSyn.algorithmic]
T_Abs_Neu_Inv [in DecSyn.algorithmic]
T_Abs_Inv [in DecSyn.algorithmic]
T_Conv_E [in DecSyn.algorithmic]
T_Bind' [in DecSyn.structural]
T_Proj2' [in DecSyn.structural]
T_Ind' [in DecSyn.structural]
T_Pair' [in DecSyn.structural]
T_App' [in DecSyn.structural]
T_Nat' [in DecSyn.structural]
U
UniqueNF.η_postponement_star [in DecSyn.fp_red]UniqueNF.η_postponement_strengthened [in DecSyn.fp_red]
UniqueNF.η_postponement [in DecSyn.fp_red]
UniqueNF.η_split [in DecSyn.fp_red]
Univ_Inv [in DecSyn.algorithmic]
up_ren_ren [in DecSyn.Autosubst2.unscoped]
up_injective [in DecSyn.common]
V
Var_Inv [in DecSyn.structural]W
weakening_su [in DecSyn.structural]weakening_wt' [in DecSyn.structural]
weakening_wt [in DecSyn.structural]
weakening_Sem_Univ [in DecSyn.logrel]
weakening_Sem [in DecSyn.logrel]
Wff_Cons' [in DecSyn.structural]
wff_mutual [in DecSyn.structural]
Wt_Univ [in DecSyn.structural]
Z
Zero_Inv [in DecSyn.algorithmic]other
Γ_eq'_refl [in DecSyn.logrel]Γ_eq'_cons [in DecSyn.logrel]
Γ_eq_sub [in DecSyn.logrel]
Γ_sub'_SemWt [in DecSyn.logrel]
Γ_sub'_cons [in DecSyn.logrel]
Γ_sub'_refl [in DecSyn.logrel]
ρ_ok_ext [in DecSyn.logrel]
ρ_ok_renaming [in DecSyn.logrel]
ρ_ok_cons' [in DecSyn.logrel]
ρ_ok_cons [in DecSyn.logrel]
ρ_ok_id [in DecSyn.logrel]
Axiom Index
L
LogRelFacts.adequacy [in DecSyn.logrel]LogRelFacts.back_closs [in DecSyn.logrel]
LogRelFacts.back_clos [in DecSyn.logrel]
LogRelFacts.Bind_nopf [in DecSyn.logrel]
LogRelFacts.Bind_inv_nopf [in DecSyn.logrel]
LogRelFacts.Bind_inv [in DecSyn.logrel]
LogRelFacts.case [in DecSyn.logrel]
LogRelFacts.cumulative [in DecSyn.logrel]
LogRelFacts.functional [in DecSyn.logrel]
LogRelFacts.join [in DecSyn.logrel]
LogRelFacts.Nat_inv [in DecSyn.logrel]
LogRelFacts.SNe_inv [in DecSyn.logrel]
LogRelFacts.sub [in DecSyn.logrel]
LogRelFacts.Univ_inv [in DecSyn.logrel]
LogRel.InterpUniv [in DecSyn.logrel]
LogRel.InterpUniv_ind [in DecSyn.logrel]
LogRel.InterpUniv_Conv [in DecSyn.logrel]
LogRel.InterpUniv_Nat [in DecSyn.logrel]
LogRel.InterpUniv_Step [in DecSyn.logrel]
LogRel.InterpUniv_Univ [in DecSyn.logrel]
LogRel.InterpUniv_Bind [in DecSyn.logrel]
LogRel.InterpUniv_Ne [in DecSyn.logrel]
N
NoForbid_FactSig.P_RReds [in DecSyn.fp_red]NoForbid_FactSig.P_EPars [in DecSyn.fp_red]
NoForbid.P [in DecSyn.fp_red]
NoForbid.PApp_imp [in DecSyn.fp_red]
NoForbid.PInd_imp [in DecSyn.fp_red]
NoForbid.PProj_imp [in DecSyn.fp_red]
NoForbid.P_renaming [in DecSyn.fp_red]
NoForbid.P_ProjInv [in DecSyn.fp_red]
NoForbid.P_PairInv [in DecSyn.fp_red]
NoForbid.P_IndInv [in DecSyn.fp_red]
NoForbid.P_BindInv [in DecSyn.fp_red]
NoForbid.P_SucInv [in DecSyn.fp_red]
NoForbid.P_AbsInv [in DecSyn.fp_red]
NoForbid.P_AppInv [in DecSyn.fp_red]
NoForbid.P_RRed [in DecSyn.fp_red]
NoForbid.P_EPar [in DecSyn.fp_red]
Inductive Index
A
algo_dom_r [in DecSyn.common]algo_dom [in DecSyn.common]
C
CoqEq [in DecSyn.algorithmic]CoqEq_R [in DecSyn.algorithmic]
CoqEq_Neu [in DecSyn.algorithmic]
CoqLEq [in DecSyn.algorithmic]
CoqLEq_R [in DecSyn.algorithmic]
Core.BTag [in DecSyn.Autosubst2.syntax]
Core.PTag [in DecSyn.Autosubst2.syntax]
Core.PTm [in DecSyn.Autosubst2.syntax]
Core.Up_PTm [in DecSyn.Autosubst2.syntax]
E
EPar.R [in DecSyn.fp_red]Eq [in DecSyn.typing]
ERed.R [in DecSyn.fp_red]
H
HRed.R [in DecSyn.common]L
LEq [in DecSyn.typing]LogRelImpl.InterpExt [in DecSyn.logrel]
lookup [in DecSyn.common]
LoRed.R [in DecSyn.fp_red]
N
NeEPar.R_elim [in DecSyn.fp_red]NeEPar.R_nonelim [in DecSyn.fp_red]
R
Ren1 [in DecSyn.Autosubst2.unscoped]Ren2 [in DecSyn.Autosubst2.unscoped]
Ren3 [in DecSyn.Autosubst2.unscoped]
Ren4 [in DecSyn.Autosubst2.unscoped]
Ren5 [in DecSyn.Autosubst2.unscoped]
RERed.R [in DecSyn.fp_red]
RPar.R [in DecSyn.fp_red]
RRed.R [in DecSyn.fp_red]
S
salgo_dom_r [in DecSyn.common]salgo_dom [in DecSyn.common]
SemWff [in DecSyn.logrel]
SN [in DecSyn.fp_red]
SNat [in DecSyn.fp_red]
SNe [in DecSyn.fp_red]
Subst1 [in DecSyn.Autosubst2.unscoped]
Subst2 [in DecSyn.Autosubst2.unscoped]
Subst3 [in DecSyn.Autosubst2.unscoped]
Subst4 [in DecSyn.Autosubst2.unscoped]
Subst5 [in DecSyn.Autosubst2.unscoped]
Sub1.R [in DecSyn.fp_red]
T
TRedSN [in DecSyn.fp_red]TRedSN' [in DecSyn.fp_red]
V
Var [in DecSyn.Autosubst2.unscoped]W
Wff [in DecSyn.typing]Wt [in DecSyn.typing]
Projection Index
C
Core.up_PTm [in DecSyn.Autosubst2.syntax]I
ids [in DecSyn.Autosubst2.unscoped]R
ren1 [in DecSyn.Autosubst2.unscoped]ren2 [in DecSyn.Autosubst2.unscoped]
ren3 [in DecSyn.Autosubst2.unscoped]
ren4 [in DecSyn.Autosubst2.unscoped]
ren5 [in DecSyn.Autosubst2.unscoped]
S
safe_red [in DecSyn.cosn]safe_nostuck [in DecSyn.cosn]
subst1 [in DecSyn.Autosubst2.unscoped]
subst2 [in DecSyn.Autosubst2.unscoped]
subst3 [in DecSyn.Autosubst2.unscoped]
subst4 [in DecSyn.Autosubst2.unscoped]
subst5 [in DecSyn.Autosubst2.unscoped]
Instance Index
C
Core.ren_PTm_morphism2 [in DecSyn.Autosubst2.syntax]Core.ren_PTm_morphism [in DecSyn.Autosubst2.syntax]
Core.Ren_PTm [in DecSyn.Autosubst2.syntax]
Core.subst_PTm_morphism2 [in DecSyn.Autosubst2.syntax]
Core.subst_PTm_morphism [in DecSyn.Autosubst2.syntax]
Core.Subst_PTm [in DecSyn.Autosubst2.syntax]
Core.Up_PTm_PTm [in DecSyn.Autosubst2.syntax]
Core.VarInstance_PTm [in DecSyn.Autosubst2.syntax]
F
funcomp_morphism2 [in DecSyn.Autosubst2.core]funcomp_morphism [in DecSyn.Autosubst2.core]
I
idsRen [in DecSyn.Autosubst2.unscoped]S
scons_morphism2 [in DecSyn.Autosubst2.unscoped]scons_morphism [in DecSyn.Autosubst2.unscoped]
Definition Index
A
algor_ind [in DecSyn.common]algo_ind [in DecSyn.common]
algo_dom_r_sind [in DecSyn.common]
algo_dom_r_ind [in DecSyn.common]
algo_dom_sind [in DecSyn.common]
algo_dom_ind [in DecSyn.common]
ap [in DecSyn.Autosubst2.unscoped]
apc [in DecSyn.Autosubst2.unscoped]
B
BindSpace [in DecSyn.logrel]BTag_eq_dec [in DecSyn.executable]
C
check_sub_r [in DecSyn.executable]check_sub [in DecSyn.executable]
check_equal_r [in DecSyn.executable]
check_equal [in DecSyn.executable]
check_sub_r_wt [in DecSyn.conv_dec]
coqeq_r_ind [in DecSyn.algorithmic]
coqeq_ind [in DecSyn.algorithmic]
coqeq_neu_ind [in DecSyn.algorithmic]
CoqEq_R_sind [in DecSyn.algorithmic]
CoqEq_R_ind [in DecSyn.algorithmic]
CoqEq_Neu_sind [in DecSyn.algorithmic]
CoqEq_Neu_ind [in DecSyn.algorithmic]
CoqEq_sind [in DecSyn.algorithmic]
CoqEq_ind [in DecSyn.algorithmic]
coqleq_r_ind [in DecSyn.algorithmic]
coqleq_ind [in DecSyn.algorithmic]
CoqLEq_R_sind [in DecSyn.algorithmic]
CoqLEq_R_ind [in DecSyn.algorithmic]
CoqLEq_sind [in DecSyn.algorithmic]
CoqLEq_ind [in DecSyn.algorithmic]
Core.BTag_sind [in DecSyn.Autosubst2.syntax]
Core.BTag_rec [in DecSyn.Autosubst2.syntax]
Core.BTag_ind [in DecSyn.Autosubst2.syntax]
Core.BTag_rect [in DecSyn.Autosubst2.syntax]
Core.compRenRen_PTm [in DecSyn.Autosubst2.syntax]
Core.compRenSubst_PTm [in DecSyn.Autosubst2.syntax]
Core.compSubstRen_PTm [in DecSyn.Autosubst2.syntax]
Core.compSubstSubst_PTm [in DecSyn.Autosubst2.syntax]
Core.extRen_PTm [in DecSyn.Autosubst2.syntax]
Core.ext_PTm [in DecSyn.Autosubst2.syntax]
Core.idSubst_PTm [in DecSyn.Autosubst2.syntax]
Core.PTag_sind [in DecSyn.Autosubst2.syntax]
Core.PTag_rec [in DecSyn.Autosubst2.syntax]
Core.PTag_ind [in DecSyn.Autosubst2.syntax]
Core.PTag_rect [in DecSyn.Autosubst2.syntax]
Core.PTm_sind [in DecSyn.Autosubst2.syntax]
Core.PTm_rec [in DecSyn.Autosubst2.syntax]
Core.PTm_ind [in DecSyn.Autosubst2.syntax]
Core.PTm_rect [in DecSyn.Autosubst2.syntax]
Core.ren_PTm [in DecSyn.Autosubst2.syntax]
Core.rinst_inst_PTm [in DecSyn.Autosubst2.syntax]
Core.subst_PTm [in DecSyn.Autosubst2.syntax]
CR [in DecSyn.logrel]
D
DJoin.R [in DecSyn.fp_red]E
EJoin.R [in DecSyn.fp_red]EPar.R_sind [in DecSyn.fp_red]
EPar.R_ind [in DecSyn.fp_red]
eq_ind [in DecSyn.typing]
Eq_sind [in DecSyn.typing]
Eq_ind [in DecSyn.typing]
ERed.R_sind [in DecSyn.fp_red]
ERed.R_ind [in DecSyn.fp_red]
ERed.tm_i_free [in DecSyn.fp_red]
ESub.R [in DecSyn.fp_red]
F
fancy_hred [in DecSyn.common]funcomp [in DecSyn.Autosubst2.core]
H
hred [in DecSyn.common]HRed.nf [in DecSyn.common]
HRed.R_sind [in DecSyn.common]
HRed.R_ind [in DecSyn.common]
I
id [in DecSyn.Autosubst2.unscoped]ind_motive_okay [in DecSyn.logrel]
isabs [in DecSyn.common]
isabs_ren [in DecSyn.common]
isbind [in DecSyn.common]
ishf [in DecSyn.common]
ishf_ren [in DecSyn.common]
ishne [in DecSyn.common]
ishne_ren [in DecSyn.common]
isnat [in DecSyn.common]
ispair [in DecSyn.common]
ispair_ren [in DecSyn.common]
issuc [in DecSyn.common]
isuniv [in DecSyn.common]
iszero [in DecSyn.common]
L
LEq_sind [in DecSyn.typing]LEq_ind [in DecSyn.typing]
le_ind [in DecSyn.typing]
list_comp [in DecSyn.Autosubst2.core]
list_id [in DecSyn.Autosubst2.core]
list_ext [in DecSyn.Autosubst2.core]
LogRelImpl.InterpExt_sind [in DecSyn.logrel]
LogRelImpl.InterpExt_ind [in DecSyn.logrel]
LogRelImpl.InterpUniv [in DecSyn.logrel]
LogRelImpl.InterpUniv_rec [in DecSyn.logrel]
lookup_sind [in DecSyn.common]
lookup_ind [in DecSyn.common]
LoRed.R_sind [in DecSyn.fp_red]
LoRed.R_ind [in DecSyn.fp_red]
M
morphing_ok [in DecSyn.structural]N
ne [in DecSyn.fp_red]NeEPar.epar_nonelim_ind [in DecSyn.fp_red]
NeEPar.epar_elim_ind [in DecSyn.fp_red]
NeEPar.R_elim_sind [in DecSyn.fp_red]
NeEPar.R_elim_ind [in DecSyn.fp_red]
NeEPar.R_nonelim_sind [in DecSyn.fp_red]
NeEPar.R_nonelim_ind [in DecSyn.fp_red]
neuneu_nonconf [in DecSyn.common]
nf [in DecSyn.fp_red]
nostuck [in DecSyn.cosn]
O
option_comp [in DecSyn.Autosubst2.core]option_ext [in DecSyn.Autosubst2.core]
option_id [in DecSyn.Autosubst2.core]
option_map [in DecSyn.Autosubst2.core]
P
ProdSpace [in DecSyn.logrel]prod_comp [in DecSyn.Autosubst2.core]
prod_ext [in DecSyn.Autosubst2.core]
prod_id [in DecSyn.Autosubst2.core]
prod_map [in DecSyn.Autosubst2.core]
PTag_eq_dec [in DecSyn.executable]
R
renaming_ok [in DecSyn.common]ren_inj [in DecSyn.common]
RERed.R_sind [in DecSyn.fp_red]
RERed.R_ind [in DecSyn.fp_red]
RPar.R_sind [in DecSyn.fp_red]
RPar.R_ind [in DecSyn.fp_red]
RRed.R_sind [in DecSyn.fp_red]
RRed.R_ind [in DecSyn.fp_red]
S
Safe_NoForbid.P [in DecSyn.cosn]salgor_ind [in DecSyn.common]
salgo_ind [in DecSyn.common]
salgo_dom_r_sind [in DecSyn.common]
salgo_dom_r_ind [in DecSyn.common]
salgo_dom_sind [in DecSyn.common]
salgo_dom_ind [in DecSyn.common]
scons [in DecSyn.Autosubst2.unscoped]
SemEq [in DecSyn.logrel]
SemLEq [in DecSyn.logrel]
SemWff_sind [in DecSyn.logrel]
SemWff_ind [in DecSyn.logrel]
SemWt [in DecSyn.logrel]
shift [in DecSyn.Autosubst2.unscoped]
size_PTm [in DecSyn.fp_red]
smorphing_ok [in DecSyn.logrel]
SNat_sind [in DecSyn.fp_red]
SNat_ind [in DecSyn.fp_red]
sne_ind [in DecSyn.fp_red]
SNe_sind [in DecSyn.fp_red]
SNe_ind [in DecSyn.fp_red]
SN_NoForbid.P [in DecSyn.fp_red]
sn_ind [in DecSyn.fp_red]
SN_sind [in DecSyn.fp_red]
SN_ind [in DecSyn.fp_red]
sred_ind [in DecSyn.fp_red]
stm_conf [in DecSyn.common]
stm_nonconf [in DecSyn.common]
Sub.R [in DecSyn.fp_red]
Sub1.R_sind [in DecSyn.fp_red]
Sub1.R_ind [in DecSyn.fp_red]
SumSpace [in DecSyn.logrel]
T
term_metric [in DecSyn.algorithmic]tm_omega [in DecSyn.cosn]
tm_conf [in DecSyn.common]
tm_nonconf [in DecSyn.common]
TRedSN_sind [in DecSyn.fp_red]
TRedSN_ind [in DecSyn.fp_red]
TRedSN'_sind [in DecSyn.fp_red]
TRedSN'_ind [in DecSyn.fp_red]
U
up_allfv [in DecSyn.Autosubst2.unscoped]up_ren [in DecSyn.Autosubst2.unscoped]
V
var_zero [in DecSyn.Autosubst2.unscoped]W
Wff_sind [in DecSyn.typing]Wff_ind [in DecSyn.typing]
wf_ind [in DecSyn.typing]
wt_ind [in DecSyn.typing]
Wt_sind [in DecSyn.typing]
Wt_ind [in DecSyn.typing]
other
Γ_eq' [in DecSyn.logrel]Γ_sub' [in DecSyn.logrel]
ρ_ok [in DecSyn.logrel]
Record Index
C
Core.Up_PTm [in DecSyn.Autosubst2.syntax]R
Ren1 [in DecSyn.Autosubst2.unscoped]Ren2 [in DecSyn.Autosubst2.unscoped]
Ren3 [in DecSyn.Autosubst2.unscoped]
Ren4 [in DecSyn.Autosubst2.unscoped]
Ren5 [in DecSyn.Autosubst2.unscoped]
S
safe [in DecSyn.cosn]Subst1 [in DecSyn.Autosubst2.unscoped]
Subst2 [in DecSyn.Autosubst2.unscoped]
Subst3 [in DecSyn.Autosubst2.unscoped]
Subst4 [in DecSyn.Autosubst2.unscoped]
Subst5 [in DecSyn.Autosubst2.unscoped]
V
Var [in DecSyn.Autosubst2.unscoped]| 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 | (1383 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 | (41 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 | (40 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 | (16 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 | (277 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 | (705 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 | (38 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 | (46 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 | (14 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 | (13 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 | (180 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 | (13 entries) |