η-confluence for the λ-calculus

Reference

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

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.stronglyConfluent_eta {Var : Type u} [HasFresh Var] [DecidableEq Var] : Relation.StronglyConfluent FullEta