GitHub repository: objectionary/proof
Primary language: Lean
Description: Proof of 𝜑-calculus confluence