Ordnode.node.injEq

theorem Ordnode.node.injEq : ∀ {α : Type u} (size : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α) (size_1 : ℕ) (l_1 : Ordnode α) (x_1 : α) (r_1 : Ordnode α), (Ordnode.node size l x r = Ordnode.node size_1 l_1 x_1 r_1) = (size = size_1 ∧ l = l_1 ∧ x = x_1 ∧ r = r_1)

This theorem, `Ordnode.node.injEq`, states that for any type `α`, two ordered nodes of type `α` are equal if and only if their sizes, left and right child nodes, and values are all respectively equal. Here, an ordered node is represented by `Ordnode.node` with size of type ℕ, left and right child nodes of type `Ordnode α`, and value of type `α`. The theorem asserts equality between two such nodes by comparing all their constituent elements.

More concisely: For any type α and ordered nodes x and y of type Ordnode.node α, x = y if and only if their sizes, left child nodes, and values are equal.