proof_irrel source