 Existence hypotheses and premises get added to the other quantifier rules: \(\forall\)-E and \(\exists\)-I become two-premiss rules, with \(E!(t)\) as the second premiss, and the subproof for \(\exists\)-E ends up with two hypotheses, \(A(a)\) and \(E!(a)\). Formulations of many-sorted quantificational logics (Hailperin 1957, 1960 for a classic statement; Freund 2019 for a philosophical application) can follow the same pattern, with the extra hypotheses and premisses saying that the relevant term or parameter stands for something in the range of a particular sort of variable.