def Lean.Meta.mkStringLitNeProof (s₁ s₂ : String) : MetaM Expr

Builds a proof of String.ofList l₁ ≠ String.ofList l₂ for two distinct string literals.

The proof avoids both String.decEq (expensive UTF-8 byte array comparison) and full List Char comparison. It reduces to List Char via String.ofList_injective, then proves the lists differ using one of two strategies depending on whether the strings share a common prefix of the shorter string's full length:

• Different characters at position i: Uses congrArg (fun l => (List.get!Internal l i).toNat) to project down to Nat, then Nat.ne_of_beq_eq_false rfl for a single Nat.beq comparison. This avoids Decidable instances entirely — the kernel only evaluates Nat.beq on two concrete natural numbers.

• One string is a prefix of the other: Uses congrArg (List.drop n ·) where n is the shorter string's length, then List.cons_ne_nil to prove the non-empty tail differs from []. This avoids decide entirely since cons_ne_nil is a definitional proof.

Equations

• One or more equations did not get rendered due to their size.