  We report on yet another formalization of the Church-Rosser property in
lambda-calculi, carried out with the proof environment Beluga. After the
well-known proofs of confluence for beta-reduction in the untyped settings,
with and without Takahashi's complete developments method, we concentrate on
eta-reduction and obtain the result for beta-eta modularly. We further extend
the analysis to typed-calculi, in particular System F. Finally, we investigate
the idea of pursuing the encoding directly in Beluga's meta-logic, as well as
the use of Beluga's logic programming engine to search for counterexamples.
