Elimination rule for the equality type aka J axiom

Question

I'm implementing a interpreter for lambda calculus, and now I want to add the equality type. The introduction rule for it is easy, but the elimination rule is rather obscure for me. I found this stackoverflow thread, but it explains the J axiom only in one sentence. How can it be understood intuitively?