βη-Confluence for the λ-calculus

Reference

• T. Nipkow, More Church-Rosser Proofs (in Isabelle/HOL)

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.stronglyCommute_eta_beta {Var : Type u} [HasFresh Var] [DecidableEq Var] : Relation.StronglyCommute FullEta FullBeta

η-reduction and β-reduction strongly commute.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.confluent_beta_eta {Var : Type u} [HasFresh Var] [DecidableEq Var] : Relation.Confluent FullBetaEta

βη-reduction is confluent.