Consider the following to prove: $(A \implies B) \implies (C \implies D)$
Could this be proved by assuming A then proving B, then using A and B to prove C, then using A, B and C to prove D? or would it be enough to use just B if B was always true, ie use B to prove $(C \implies D)$?
Or should it be proved using the below structure by assuming $A \implies B$ and then assuming C to get A, which gives us B, then using C, A and B, to show D?
Are both these approaches the same, is one preferable to the other in certain cases, is more information needed, or is one of them completely wrong? I'm looking to understand how to deal with these kinds of proof goals in general.
I think its likely to do with the underlyling structure of the data being reasoned over e.g. if there are compositionality, as with inductions, the square like approach seems better, as structure information could be used to simplify the proofs?
