exact p_entails_c_arr_j
case right.h_2.h_4.inr
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
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_eq_idx : ↑j = ↑idx
p_entails_c_arr_j : p ⊨ c_arr[↑idx]
⊢ p ⊨ c_arr[↑idx]
no goals