English
For any L1,L2,L3,L4, if Red.Step L1 L3 and Red.Step L2 L4 and L1 = L2, then either L3 = L4 or there exists L5 such that Red.Step L3 L5 and Red.Step L4 L5.
Русский
Для любых L1,L2,L3,L4, если Red.Step L1 L3 и Red.Step L2 L4 и L1 = L2, то либо L3 = L4, либо существует L5 such that Red.Step L3 L5 и Red.Step L4 L5.
LaTeX
$$$\forall L_1,L_2,L_3,L_4,\; Red.Step L_1 L_3 \land Red.Step L_2 L_4 \land L_1 = L_2 \Rightarrow (L_3 = L_4 \lor \exists L_5\; Red.Step L_3 L_5 \land Red.Step L_4 L_5)$$$
Lean4
@[to_additive]
theorem diamond :
∀ {L₁ L₂ L₃ L₄ : List (α × Bool)},
Red.Step L₁ L₃ → Red.Step L₂ L₄ → L₁ = L₂ → L₃ = L₄ ∨ ∃ L₅, Red.Step L₃ L₅ ∧ Red.Step L₄ L₅
| _, _, _, _, Red.Step.not, Red.Step.not, H => Step.diamond_aux H
