rw [encode, decode]
a✝¹ a✝ : ConsExp
hf : decode (encode a✝¹) = a✝¹
hg : decode (encode a✝) = a✝
⊢ decode (encode (cons a✝¹ a✝)) = cons a✝¹ a✝
a✝¹ a✝ : ConsExp
hf : decode (encode a✝¹) = a✝¹
hg : decode (encode a✝) = a✝
⊢ (match hn : Nat.boddDiv2 (2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1) with
    | (false, m) => nat m
    | (true, m) =>
      match hm : Nat.unpair m with
      | (f, g) =>
        let_fun hn' := (_ : 1 ≤ 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
        let_fun this := (_ : m < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
        let_fun this_1 := (_ : f < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
        let_fun this := (_ : g < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
        cons (decode f) (decode g)) =
    cons a✝¹ a✝