Theorem: HMem.Encoding.tupleInj_eq (HMem/Encoding/Basic.lean)

State before:
α : Type u_1
inst✝ : Encoding α Memory
N₀ N₁ : ℕ
f₀ : Fin N₀ → α
f₁ : Fin N₁ → α
⊢ (encode f₀ = encode f₁) = (N₀ = N₁ ∧ HEq f₀ f₁)
Tactic:
simp [encodeFinTuple_def, List.ofFn_inj']
State after:
no goals