simp only [Array.size_toArray, List.length_nil] at h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
i lhs rhs : Nat
linv rinv : Bool
h : i < #[].size
⊢ #[][i] = Decl.gate lhs rhs linv rinv → lhs < i ∧ rhs < i
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
i lhs rhs : Nat
linv rinv : Bool
h✝ : i < #[].size
h : i < 0
⊢ #[][i] = Decl.gate lhs rhs linv rinv → lhs < i ∧ rhs < i