Theorem: Cpdt.Chapter3.OddList.oCons_oappend (Cpdt/Chapter3/Mutual.lean)

State before:
x : Nat
xs ys : EvenList
⊢ oappend (oCons x xs) ys = oCons x (eappend xs ys)
Tactic:
rw[oappend]
State after:
no goals