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.
<p>To transform multi-type to unitype<ul>
<li>Invent a new predicate T for each type which will be deemed true for that type and false for all others.
<li>Recursively replace each instance of (<font size=+2>∧</font>x Φ) by
(<font size=+2>∧</font>x (Tx → Φ)) where the selected predicate T matches the type of the variable x.
We assume that existential quantifiers are defined in terms of universal quantifiers and they will be transformed thereby as well.</ul>
It takes only a little work to transform the proofs from multi type logic to unitype logic.