##article.return## A Modular Lean 4 Framework for Confluence and Strong Normalization of Lambda Calculi with Products and Sums Download Download PDF