exact ih1 i i_lt_idx p_entails_c_arr_i
case h.inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
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 : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
p_entails_c_arr_i : p ⊨ c_arr[↑i]
i_lt_idx : ↑i < ↑idx
⊢ False
no goals