constructor
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit✝ : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
⊢ (∀ (seq : β → ℕ → Bool), propagate init_carry next_bit seq = zeroSeq) ↔
    ∀ (seq : β → ℕ → Bool) (i : ℕ), i < 2 ^ card α → propagate init_carry next_bit seq i = false
case mp
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit✝ : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
⊢ (∀ (seq : β → ℕ → Bool), propagate init_carry next_bit seq = zeroSeq) →
    ∀ (seq : β → ℕ → Bool) (i : ℕ), i < 2 ^ card α → propagate init_carry next_bit seq i = false

case mpr
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit✝ : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
⊢ (∀ (seq : β → ℕ → Bool) (i : ℕ), i < 2 ^ card α → propagate init_carry next_bit seq i = false) →
    ∀ (seq : β → ℕ → Bool), propagate init_carry next_bit seq = zeroSeq