Function prove_int_eq 

pub fn prove_int_eq(ctx: &Context, lhs: &Term, rhs: &Term) -> Option<Term>

Prove an Int equality Eq Int lhs rhs, or return None.

The returned term, when it exists, has type Eq Int lhs rhs (the kernel will confirm). None means “this oracle found no proof” — never “it is false.”