intro i b h p hp j j_lt_idx_add_one p_entails_c_arr_j
case right
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
res : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) res
⊢ ∀ (a : PosFin n) (b : Bool),
    reduce_fold_fn assignment res c_arr[↑idx] = reducedToUnit (a, b) →
      ∀ (p : PosFin n → Bool), p ⊨ assignment → ∀ (x : Fin c_arr.size), ↑x < ↑idx + 1 → p ⊨ c_arr[↑x] → p ⊨ (a, b)
case right
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
res : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) res
i : PosFin n
b : Bool
h : reduce_fold_fn assignment res c_arr[↑idx] = reducedToUnit (i, b)
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
⊢ p ⊨ (i, b)