Ugly expansion proofs

[gebner]

val Some(ugly) = Escargot.getExpansionProof(hof"∃x ∃y (p(x) → p(y))")
// :- ∃x ∃y (p(x) → p(y))
//      +^{x, y} (wk-{p(x)} → p(y)+)
//      +^{y, y} (p(y)- → wk+{p(y)})

😞 The reason is that there are two clauses here ⊢ p(x) and p(y) ⊢ and we combine the instances for these two clauses in an unfortunate way.