# On the diamond property for $F_{\omega}$ in TAPL

In page 455, of Pierce´s TAPL and page 560, the single-step diamond property of reduction:

$$S \Rrightarrow S' \land T \Rrightarrow T' \implies \exists V. T \Rrightarrow V \land U \Rrightarrow V$$

is proved. The argument goes by induction on the total sizes of the given derivations, with a case analysis on the final rules of both. I think this is a bit of an overkill since I think I have a proof by induction on $$S$$.

If $$S = X$$ then $$T=U=X$$ and we can take $$V = X$$.

If $$S = S_1 \to S_2$$ then $$T = T_1 \to T_2$$ and $$U = U_1 \to U_2$$ where $$S_1 \Rrightarrow T_1, S_2 \Rrightarrow T_2, S_1 \Rrightarrow U_1, S_2 \Rrightarrow U_2$$. By induction hypothesis, $$\exists V_1,V_2. T_1, U_1 \Rrightarrow V_1, T_2,U_2 \Rrightarrow V_2$$ and by the rule QR-Arrow $$T \Rrightarrow V_1 \to V_2, U \Rrightarrow V_1 \to V_2$$.

The rest of the cases are similar with the help of lemma 30.3.7:

$$S \Rrightarrow S', T \Rrightarrow T' \implies [Y \mapsto S]T \Rrightarrow [Y \mapsto S']T'$$

for the case QR-AppAbs.

Could you help me understand what's wrong with my proofs?