simp
case isFalse.e_xs.h.e_6
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
lhs rhs : aig.RefStream len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
idx : Nat
hidx : idx < curr
res : RefStreamEntry α len
h✝ : ¬curr < len
hgo : { aig := aig, stream := ⋯ ▸ s } = res
⊢ HEq (⋯ ▸ s) s
no goals