Function lex_le 

pub fn lex_le(x: &[ProofExpr], y: &[ProofExpr], aux: &str) -> ProofExpr

“X ≤ₗₑₓ Y” over equal-length boolean vectors (false < true), MSB-first: at the first index where they differ, X has false and Y has true. Encoded with a chain of “equal-so-far” auxiliaries {aux}_eq_{k} (distinct constraints must use distinct aux). Returns a tautology for empty/ length-1-or-shorter vectors handled position-by-position.

Correctness is pinned exhaustively against a brute-force oracle (every assignment, small m).