βη-Confluence for the λ-calculus #
Reference #
- [T. Nipkow, More Church-Rosser Proofs (in Isabelle/HOL)][Nipkow2001]
theorem
Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.stronglyCommute_eta_beta
{Var : Type u}
[HasFresh Var]
[DecidableEq Var]
:
η-reduction and β-reduction strongly commute.
theorem
Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.confluent_beta_eta
{Var : Type u}
[HasFresh Var]
[DecidableEq Var]
:
βη-reduction is confluent.