no goals
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
H : (∃ l', Raised l' (size l) ∧ BalancedSz l' (size r)) ∨ ∃ r', Raised (size r) r' ∧ BalancedSz (size l) r'
⊢ All P (balanceL l x r) ↔ All P l ∧ P x ∧ All P r
rw [balanceL_eq_balance' hl hr sl sr H, all_balance']