It is not uncommon to find a theorem statement in the literature that draws
C2 (which we would represent in Proofscape as
Thm.C2), and having a proof that first deduces
C1 and then goes on to use
C1 together with further
argumentation in order to deduce conclusion
In Proofscape, due to the unidirectional flow convention for diagrams, such a proof must be broken into two separate deductions.
The problem, as illustrated on the left of Fig. 18, is that
when the first conclusion node
Thm.C1 is used in combination with further
argumentation in the proof, the diagram has to have an arrow that goes
backwards, terminating higher in the diagram than it originates.
Backward arrows like the arrow from
Fig. 18 are not allowed in Proofscape. One reason for this is
that this breaks the desired visual convention, in which the argument always
flows in one direction. Another reason is that such backward edges can be hard
for layout algorithms to handle.
The solution is simply to break the proof into two deductions, as illustrated on the right in Fig. 18.