simp only [h] at p_c_arr_idx_eq_false
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = false
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) neg = false
p_c_arr_idx_eq_false : ¬p c_arr[↑idx].fst = true
⊢ p ⊨ (i, b)
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = false
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) neg = false
p_c_arr_idx_eq_false : ¬p i = true
⊢ p ⊨ (i, b)