Theorem: Cpdt.Chapter3.EvenList.eCons_eappend (Cpdt/Chapter3/Mutual.lean)

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