Set up API for proof transfer with the completeness theorem

[jesse-michael-han]

Given a 𝔹-valued model M of a theory T, a proposition of the form ⊤ ≤ (b : 𝔹), if there exists a first-order sentence ψ such that ⟦ψ⟧[M] = b then by the completeness theorem and 𝔹-valued soundness theorem, to prove the proposition it suffices to show that ψ is true in every ordinary model of T.

We could set up a typeclass of models of T (and maybe have special support for ZFC) to make working in an arbitrary model easier.

Once this is done we could try transferring proofs from Metamath mm0-style by generalizing Mario's setup for pSet.