induction c
c : ConsExp
⊢ decode (encode c) = c
case nat
a✝ : ℕ
⊢ decode (encode (nat a✝)) = nat a✝

case cons
a✝¹ a✝ : ConsExp
a_ih✝¹ : decode (encode a✝¹) = a✝¹
a_ih✝ : decode (encode a✝) = a✝
⊢ decode (encode (cons a✝¹ a✝)) = cons a✝¹ a✝