cases h
a✝¹ a✝ : ConsExp
hf : decode (encode a✝¹) = a✝¹
hg : decode (encode a✝) = a✝
m✝ : ℕ
h✝ : Nat.boddDiv2 (2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1) = (true, m✝)
h : Nat.mkpair (encode a✝¹) (encode a✝) = 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 refl
a✝¹ a✝ : ConsExp
hf : decode (encode a✝¹) = a✝¹
hg : decode (encode a✝) = a✝
h : Nat.boddDiv2 (2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1) = (true, Nat.mkpair (encode a✝¹) (encode a✝))
⊢ (match hm : Nat.unpair (Nat.mkpair (encode a✝¹) (encode a✝)) with
    | (f, g) =>
      let_fun hn' := (_ : 1 ≤ 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this := (_ : Nat.mkpair (encode a✝¹) (encode a✝) < 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✝