simp [FoldTarget.mkAnd, hidx]
case mpr.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
idx : Nat
hidx : idx < len
h : ⟦{ aig := aig, ref := s.getRef idx hidx }, assign⟧ = true
⊢ idx < len
no goals