The logic of multiple generality in antiquity

In an older preprint of ours (Ancient Natural Deduction) we tried to argue from Aristotle, Euclid and Galen that the ancients were in possession of the basic natural deduction rules for quantifiers. In Sextus' Outlines II, v, 23 (discussing a view of Democritus) we find the following theorem involving quantifiers: From the premises \[ Human(x) \leftrightarrow \forall y. (Human(y) \rightarrow Know(y,x))\tag{1}\]\[\neg \exists x. (Human(x) \& \forall y. (Human(y) \rightarrow Know(y,x)))\tag{2}\]is concluded \[ \neg \exists x. Human(x)\]

It would be interesting to find in detail how the ancients might have carried out the proof of this conclusion. Could Stoic logic have handled this ?

There also an interesting argument in II, xii, 141 (If some god has told you that this man will be rich...) which we interpret as:  \[ (\exists x. God(x)\& ToldRich(x,y)) \rightarrow BeRich(y)\tag{1}\] \[ God(a)\& ToldRich(a,b)\tag{2}\] therefore \[BeRich(b)\]

In modern natural deduction we would use $\exists$-introduction on (2) for $a$, $\forall$-introduction on (1) for variable $y$ and then $\forall$-elimination for substitution $[b/y]$ and finish with modus ponens. How would the Stoics have done this ?

 We plan to write a survey article discussing Bobzien and Shogry's paper Stoic Logic and Multiple Generality. These authors argue that the Stoics 'had all the elements' to develop a variable-free version of quantifier logic, even if there is no direct evidence that the Stoics actually carried out such an enterprise. One of the reason this interests us is because of our own project which involves combinatory (variable-free) intensional logics.