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

State before:
α : Type u_1
inst✝ : Encoding α Memory
N₁ : ℕ
x✝¹ : (Fin 0 → Bool) → α
x✝ : (Fin N₁ → Bool) → α
⊢ encode x✝¹ = encode x✝ → 0 = N₁
Tactic:
cases N₁ <;> simp [encodeOp_zeroDef, encodeOp_succDef]
State after:
no goals

State before:
α : Type u_1
inst✝ : Encoding α Memory
N₀ : ℕ
x✝¹ : (Fin (N₀ + 1) → Bool) → α
x✝ : (Fin 0 → Bool) → α
⊢ encode x✝¹ = encode x✝ → N₀ + 1 = 0
Tactic:
simp [encodeOp_zeroDef, encodeOp_succDef]
State after:
no goals

State before:
α : Type u_1
inst✝ : Encoding α Memory
N₀ N₁ : ℕ
f₀ : (Fin (N₀ + 1) → Bool) → α
f₁ : (Fin (N₁ + 1) → Bool) → α
⊢ encode f₀ = encode f₁ → N₀ + 1 = N₁ + 1
Tactic:
simpa [encodeOp_succDef] using λ _ ↦ encodeOp_injN
State after:
no goals