The forward direction is: if $s \equiv_\alpha s' \land t \equiv_\alpha t'$, then $st \equiv_\alpha s't'$. I'm wondering if this holds:
if $st \equiv_\alpha s' t'$ then $s \equiv_\alpha s' \land t \equiv_\alpha t'$.
I was trying to come up with a counterargument, where if for any term $s t$, there exists a way to rewrite it as: $s'' t''$, where $s'' \not \equiv s' \lor t'' \not\equiv t'$, then this property clearly fails. But I haven't found any way to do this, as expanding the terms seem to keep the terms encapsulated inside $s$ or $t$. Maybe I'm missing something.
Thanks!
In an inductive definition of α-equivalence, there is a rule $$\dfrac{s =_α s' \quad t =_α t'}{st =_α s't'}$$ and this is the only way to deduce that two applications are α-equivalent. Hence what you try to (dis)prove is true by definition.
Alternatively, you could have these two rules: $$\dfrac{s =_α s'}{st =_α s't} \qquad \dfrac{t =_α t'}{st =_α st'}$$ then similarly the statement holds.