exact ⟨n, hn2, seq, rfl⟩
case pos
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : n < 2 ^ card α
⊢ ∃ m _hm seq2, propagate init_carry next_bit seq2 m = propagate init_carry next_bit seq n
no goals