| Name | Category | Theorems |
|---|
Binding 📖 | CompData | 6 mathmath: Env.Wf.to_ok, Binding.subst_sub, Typing.tabs_inv, Typing.abs_inv, Binding.subst_fresh, Binding.subst_ty
|
Env 📖 | CompOp | 1 mathmath: Env.Wf.to_ok
|
Term 📖 | CompData | 24 mathmath: Term.open_ty_subst_ty_intro, Term.open_tm_subst_ty, Term.openRec_tm_subst_tm, Term.open_ty_subst_tm, Term.openRec_ty_subst_tm, Term.open_ty_subst_ty, Term.subst_tm_lc, Term.subst_ty_def, Term.subst_tm_fresh, Term.openRec_ty_subst_ty, Term.open_tm_subst_tm, Typing.subst_tm, Term.subst_ty_lc, Term.openRec_ty_subst_ty_intro, Term.openRec_tm_subst_tm_intro, Term.open_tm_subst_tm_intro, Term.open_ty_subst_tm_var, Term.open_ty_subst_ty_var, Term.subst_ty_fresh, Term.open_tm_subst_ty_var, Term.open_tm_subst_tm_var, Term.subst_tm_def, Typing.subst_ty, Term.openRec_tm_subst_ty
|
Ty 📖 | CompData | 26 mathmath: Ty.open_subst, Term.open_ty_subst_ty_intro, Term.open_tm_subst_ty, Ty.subst_def, Ty.open_subst_intro, Term.open_ty_subst_ty, Binding.subst_sub, Term.subst_ty_def, Ty.openRec_subst_intro, Env.Wf.map_subst_nmem, Env.Wf.map_subst, Term.openRec_ty_subst_ty, Term.subst_ty_lc, Term.openRec_ty_subst_ty_intro, Sub.map_subst, Binding.subst_fresh, Ty.subst_fresh, Ty.openRec_subst, Ty.subst_lc, Term.open_ty_subst_ty_var, Term.subst_ty_fresh, Term.open_tm_subst_ty_var, Typing.subst_ty, Binding.subst_ty, Term.openRec_tm_subst_ty, Ty.open_subst_var
|
instInhabitedBinding 📖 | CompOp | — |
instInhabitedTy 📖 | CompOp | — |