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

State before:
α : Type u_1
β : Type u_2
inst✝¹ : Encoding α Memory
inst✝ : Encoding β Memory
v : α ⊕ β
⊢ Memory.getm (encode v) true = 0
Tactic:
cases v <;> simp
State after:
no goals