INFINITE: Prove Theorem 3.11 (laws with at most two variables have nontrivial finite models)

[teorth]

A result of Austin. Proven by considering linear models x ◇ y = a * x + b * y. Some field theory may be required to formalize the proof properly.

InfModel.lean is the most logical place to place this theorem.

When done, mark the statement and proof of the theorem in the blueprint with \leanoks, and the statement with a \lean{} tag.

[jscanvic]

claim

[jscanvic]

propose #442