constructor
i : Nat
⊢ getBit 1 i = true ↔ getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false
case mp
i : Nat
⊢ getBit 1 i = true → getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false

case mpr
i : Nat
⊢ (getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false) → getBit 1 i = true