Safety

📁 Source: Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean

Statistics

Metric	Count
Definitions	0
Theorems preservation, progress	2
Total	2

Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservation 📖	—	Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.Red	—	—	abs_inv tabs_inv Cslib.HasFresh.fresh_exists Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.open_ty_subst_ty_intro Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.open_subst_intro inl_inv inr_inv
progress 📖	mathematical	Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding	Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.Value Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.Red	—	canonical_form_abs canonical_form_tabs canonical_form_sum

---

← Back to Index