Henning Basold, Peter Bruin, Dominique Lawson: The Directed Van Kampen Theorem in Lean. ITP 2024: 8:1-8:18