no goals
α : Type u_1
t : Ordnode α
hl : Sized t
C : Ordnode α → Prop
H0 : C nil
H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (Ordnode.node' l x r)
⊢ C t
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)
no goals
case nil
α : Type u_1
C : Ordnode α → Prop
H0 : C nil
H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (Ordnode.node' l x r)
hl : Sized nil
⊢ C nil
exact H0
case node
α : Type u_1
C : Ordnode α → Prop
H0 : C nil
H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (Ordnode.node' l x r)
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
t_ih_l : Sized l✝ → C l✝
t_ih_r : Sized r✝ → C r✝
hl : Sized (node size✝ l✝ x✝ r✝)
⊢ C (Ordnode.node' l✝ x✝ r✝)
case node
α : Type u_1
C : Ordnode α → Prop
H0 : C nil
H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (Ordnode.node' l x r)
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
t_ih_l : Sized l✝ → C l✝
t_ih_r : Sized r✝ → C r✝
hl : Sized (node size✝ l✝ x✝ r✝)
⊢ C (node size✝ l✝ x✝ r✝)
rw [hl.eq_node']
no goals
case node
α : Type u_1
C : Ordnode α → Prop
H0 : C nil
H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (Ordnode.node' l x r)
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
t_ih_l : Sized l✝ → C l✝
t_ih_r : Sized r✝ → C r✝
hl : Sized (node size✝ l✝ x✝ r✝)
⊢ C (Ordnode.node' l✝ x✝ r✝)
exact H1 _ _ _ (t_ih_l hl.2.1) (t_ih_r hl.2.2)