Credit Werner [LMCS 2008] in confluence proof

[andreasabel]

A confluence proof using a reduction relation (kappa) and a relation comparing syntax up to proof-irrelevance (==p) was presented first by Benjamin Werner in his LMCS 2008 paper On the Strength of Proof-Irrelevant Type Theories. He uses beta-reduction and epsilon-equality (equality up to erasure of proof parts). His proof also employs the parallel reduction method.

Note that his definition of the reduction rule for elimination of propositional equality has a typo (as confirmed with him via email). The eliminator should be reducible whenever the two sides of the equality are beta-epsilon-equal, not just epsilon-equal as written in the paper.

I think it would be good to reference his work when you explain the idea of your confluence proof.