如何使用 LaTeX 编写结构归纳证明？

Question

只是想知道我可以在 LaTeX 中使用哪些包或方法来为 LaTeX 中的列表写出结构归纳证明；我正在 overleaf 中写出证明。

作为示例，我尝试写出这个引理来证明：

$$(\dagger) \forall xs \forall ys. length(xs ++ ys) = length (ys ++ xs)$$

但这在视觉上不太清楚，我想要一些类似于下图所示的方程式

。

任何帮助都将不胜感激，谢谢。