[tel]

> it is as impossible to determine whether two lawful sequences are equal as it is to determine whether two lawless sequences are

I also think that's enough.

I think when you mention that it's easier to build a mechanistic theorem prover on an intuitionistic foundation that it's a bit more "foundational" a problem than it seems. Theorem provers need (some kind of partial) equality on propositions and on proofs in order to function, but propositions are too rich to support finite equality. This backs you into a more intuitionistic approach.

[pron]

> but propositions are too rich to support finite equality

Why do you say that? The finitary deduction rules of all logic systems provide both equivalence (<=>) and partial order (=> or |-) relations. Classical logic gives rise to a boolean algebra, while intuirionistic logic forms a Heyting algebra, of which boolean algebra is a special case. The latter is more general, but both are bounded lattices, and both are perfectly fine.

[tel]

Sorry, on the propositions themselves, yes, but it's hard to internalize equality: the big sticking point between ITT, OTT, HTT, etc.

[pron]

It's only hard if you're constructive (and so all relations have to be computable, including equality).