If you want something like first-order predicate calculus but need several ‘types’ each using its own sort of variable here is how to re-do your propositions so as to appear as ordinary PC (predicate calc) and also convert your proofs.

To transform multi-type to unitype

It takes only a little work to transform the proofs from multi type logic to unitype logic.