simp only [ofArray, Array.foldl_eq_foldl_data] at h
case right.intro
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
hl :
  ∀ (acc : Array Assignment),
    modified_assignments_invariant acc →
      ∀ (cOpt : Option (DefaultClause n)), cOpt ∈ arr.data → modified_assignments_invariant (ofArray_fold_fn acc cOpt)
_h_size : (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data).size = n
h' :
  ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data)[i.val] = true →
      unit (i, b) ∈ (ofArray arr).toList
i : PosFin n
b : Bool
h : hasAssignment b (ofArray arr).assignments[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList
case right.intro
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
hl :
  ∀ (acc : Array Assignment),
    modified_assignments_invariant acc →
      ∀ (cOpt : Option (DefaultClause n)), cOpt ∈ arr.data → modified_assignments_invariant (ofArray_fold_fn acc cOpt)
_h_size : (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data).size = n
h' :
  ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data)[i.val] = true →
      unit (i, b) ∈ (ofArray arr).toList
i : PosFin n
b : Bool
h : hasAssignment b (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data)[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList