split
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✝
case h_1
a✝¹ a✝ : ConsExp
hf : decode (encode a✝¹) = a✝¹
hg : decode (encode a✝) = a✝
m✝ : ℕ
heq✝ : Nat.boddDiv2 (2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1) = (false, m✝)
⊢ nat m✝ = cons a✝¹ a✝

case h_2
a✝¹ a✝ : ConsExp
hf : decode (encode a✝¹) = a✝¹
hg : decode (encode a✝) = a✝
m✝ : ℕ
heq✝ : Nat.boddDiv2 (2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1) = (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✝