Add perf test: proof irrelevance refutes proofs of different propositions

[nomeata]

This adds perf/irrelevance-refutes, which checks

f 100000 (slowRefl 100000) = f 100001 (slowRefl 100001)

where f ignores its arguments and slowRefl m : m = m is a Nat.rec over m. A checker that compares the arguments may meet the two proofs. Their types, 100000 = 100000 and 100001 = 100001, are not defeq, so the proofs are not defeq either. Official's is_def_eq_core stops on is_def_eq_proof_irrel's l_false. A checker that uses only proof irrelevance's positive answer instead unfolds both proofs, at a cost of Θ(m).

Official compares the arguments left to right and refutes at the literals before it reaches the proofs. No test of this shape can catch a left-to-right checker: proofs whose types differ always come after an earlier argument that already differs.

The test is distilled from decide +kernel on Rat arithmetic, which made nanoda run out of memory on the Lean v4.35.0-rc3 export of Mathlib. There the proofs are Nat.gcd_dvd terms by well-founded recursion, reached through Int.divExact's arguments, which nanoda compares right to left.

Local results, instructions:u, one run each, nanoda with the arena's config:

checker	instructions	result
nanoda 3a24072	1.9 G	accepted
nanoda 3a24072 + three-valued proof irrelevance	2.9 M	accepted
official	170 M (startup)	accepted
con-ron	139 M (startup)	accepted

🤖 Generated with Claude Code