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.
😞 The reason is that there are two clauses here
⊢ p(x)andp(y) ⊢and we combine the instances for these two clauses in an unfortunate way.