English
Let hl be a Sized witness for t. If a predicate C on Ordnode α is true for nil and closed under node-building from l and r when C l and C r hold, then C t holds.
Русский
Пусть hl — признак того, что t является Sized. Если для предиката C на Ordnode α верно C(nil) и C(l) → C(r) → C(l.node' x r), то C t выполняется.
LaTeX
$$$\\forall t\\ (hl : Sized t)\\ {C : Ordnode\\, α \\to Prop},\\ C nil\\ \\to\\ (\\forall l x r, C l \\to C r \\to C (l.\\mathrm{node'} x r))\\to C t$$$
Lean4
@[elab_as_elim]
theorem induction {t} (hl : @Sized α t) {C : Ordnode α → Prop} (H0 : C nil)
(H1 : ∀ l x r, C l → C r → C (.node' l x r)) : C t := by
induction t with
| nil => exact H0
| node _ _ _ _ t_ih_l t_ih_r =>
rw [hl.eq_node']
exact H1 _ _ _ (t_ih_l hl.2.1) (t_ih_r hl.2.2)
