simp only [eq_iff_iff, iff_self_and]
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : ¬curr < len
hgo : { aig := aig, ref := acc } = res
⊢ (⟦{ aig := { aig := aig, ref := acc }.aig, ref := { aig := aig, ref := acc }.ref }, assign⟧ = true) =
    (⟦{ aig := aig, ref := acc }, assign⟧ = true ∧
      ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true)
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : ¬curr < len
hgo : { aig := aig, ref := acc } = res
⊢ ⟦{ aig := aig, ref := acc }, assign⟧ = true →
    ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true