English
If l is alternating and its length is even, then for every boolean b, 2 × count b l equals the length of l (i.e., the two booleans occur equally often).
Русский
Если l — чередующийся список и его длина чётна, то для любого булевого значения b число его вхождений в l умноженное на 2 равно длине l (то есть true и false встречаются одинаковое число раз).
LaTeX
$$$$\forall l : \text{List Bool},\ \text{IsChain}(\\neq) l \rightarrow \text{Even}(\text{length}(l)) \rightarrow \forall b \in \{\text{true},\text{false}\}, 2 \cdot \#\{ i \mid l_i = b \} = \text{length}(l).$$$$
Lean4
theorem two_mul_count_bool_of_even (hl : IsChain (· ≠ ·) l) (h2 : Even (length l)) (b : Bool) :
2 * count b l = length l := by rw [← count_not_add_count l b, hl.count_not_eq_count h2, two_mul]
