Theory cv_type

⊢ ∀c. from_char c = Num (ORD c)

⊢ ∀i. from_int i =
      if i < 0 then Pair (Num (Num i)) (Num 0) else Num (Num i)

⊢ (∀f. from_list f [] = Num 0) ∧
  ∀f x xs. from_list f (x::xs) = Pair (f x) (from_list f xs)

⊢ (∀f. from_option f NONE = Num 0) ∧
  ∀f x. from_option f (SOME x) = Pair (Num 1) (f x)

⊢ ∀f1 f2 x y. from_pair f1 f2 (x,y) = Pair (f1 x) (f2 y)

⊢ ∀r. from_rat r = Pair (from_int (RATN r)) (Num (RATD r))

⊢ (∀f1 f2 x. from_sum f1 f2 (INL x) = Pair (Num 0) (f1 x)) ∧
  ∀f1 f2 y. from_sum f1 f2 (INR y) = Pair (Num 1) (f2 y)

⊢ ∀f t. from_to f t ⇔ ∀x. t (f x) = x

⊢ from_unit () = Num 0

⊢ ∀w. from_word w = Num (w2n w)

⊢ ∀x. to_char x = CHR (c2n x)

⊢ (∀n. to_int (Num n) = &n) ∧ ∀x y. to_int (Pair x y) = -&c2n x

⊢ (∀f n. to_list f (Num n) = []) ∧
  ∀f x y. to_list f (Pair x y) = f x::to_list f y

⊢ (∀f n acc. to_list_tr f (Num n) acc = REVERSE acc) ∧
  ∀f x y acc. to_list_tr f (Pair x y) acc = to_list_tr f y (f x::acc)

⊢ (∀t n. to_option t (Num n) = NONE) ∧
  ∀t x y. to_option t (Pair x y) = SOME (t y)

⊢ (∀n. to_rat (Num n) = 0) ∧
  ∀x y. to_rat (Pair x y) = rat_of_int (to_int x) / &c2n y

⊢ (∀t1 t2 n. to_sum t1 t2 (Num n) = ARB) ∧
  ∀t1 t2 x y.
    to_sum t1 t2 (Pair x y) = if x = Num 0 then INL (t1 y) else INR (t2 y)

⊢ ∀x. to_unit x = ()

⊢ ∀n. to_word n = n2w (c2n n)

⊢ f1 (THE x) = y1 ∧ IS_SOME x ⇒ from_option f1 x = Pair (Num 1) y1

⊢ f1 (FST x) = y1 ∧ f2 (SND x) = y2 ⇒ from_pair f1 f2 x = Pair y1 y2

⊢ THE x = y1 ∧ IS_SOME x ⇒ x = SOME y1

⊢ FST x = y1 ∧ SND x = y2 ⇒ x = (y1,y2)

⊢ (∀y xs x n.
     cv_has_shape (SOME n::xs) (Pair x y) ⇔ x = Num n ∧ cv_has_shape xs y) ∧
  (∀y xs x. cv_has_shape (NONE::xs) (Pair x y) ⇔ cv_has_shape xs y) ∧
  (∀xs v1 v0. cv_has_shape (v0::xs) (Num v1) ⇔ F) ∧
  ∀c. cv_has_shape [] c ⇔ T

⊢ (cv_has_shape [] cv ⇔ T) ∧
  (cv_has_shape (NONE::xs) cv ⇔ ∃x y. cv = Pair x y ∧ cv_has_shape xs y) ∧
  (cv_has_shape (SOME n::xs) cv ⇔
   ∃y. cv = Pair (Num n) y ∧ cv_has_shape xs y)

⊢ ∀P. (∀n xs x y. P xs y ⇒ P (SOME n::xs) (Pair x y)) ∧
      (∀xs x y. P xs y ⇒ P (NONE::xs) (Pair x y)) ∧
      (∀v0 xs v1. P (v0::xs) (Num v1)) ∧ (∀c. P [] c) ⇒
      ∀v v1. P v v1

⊢ from_option f1 x = Pair (Num 1) y1 ⇒ f1 (THE x) = y1 ∧ IS_SOME x

⊢ from_pair f1 f2 x = Pair y1 y2 ⇒ f1 (FST x) = y1 ∧ f2 (SND x) = y2

⊢ from_to b2c c2b

⊢ from_to from_char to_char

⊢ from_to from_int to_int

⊢ from_to f t ⇒ from_to (from_list f) (to_list t)

⊢ from_to Num c2n

⊢ from_to f t ⇒ from_to (from_option f) (to_option t)

⊢ from_to f1 t1 ∧ from_to f2 t2 ⇒ from_to (from_pair f1 f2) (to_pair t1 t2)

⊢ from_to from_rat to_rat

⊢ from_to f1 t1 ∧ from_to f2 t2 ⇒ from_to (from_sum f1 f2) (to_sum t1 t2)

⊢ from_to from_unit to_unit

⊢ from_to from_word to_word

⊢ (case v of NONE => Num 0 | SOME x => Pair (Num 1) (f x)) =
  from_option f v

⊢ (case v of (v0,v1) => Pair (f0 v0) (f1 v1)) = from_pair f0 f1 v

⊢ (case v of INL x => Pair (Num 0) (f0 x) | INR y => Pair (Num 1) (f1 y)) =
  from_sum f0 f1 v

⊢ (if cv_has_shape [NONE] v then SOME (t (cv_snd v)) else NONE) =
  to_option t v

⊢ (if cv_has_shape [NONE] v then (t1 (cv_fst v),t2 (cv_snd v)) else ARB) =
  to_pair t1 t2 v

⊢ (if cv_has_shape [SOME 0] v then INL (t1 (cv_snd v))
   else if cv_has_shape [NONE] v then INR (t2 (cv_snd v))
   else ARB) =
  to_sum t1 t2 v

⊢ to_list f v = to_list_tr f v []

⊢ x = to_option t1 (Pair x1 x2) ⇒ THE x = t1 x2 ∧ IS_SOME x

⊢ x = to_pair t1 t2 (Pair x1 x2) ⇒ FST x = t1 x1 ∧ SND x = t2 x2

⊢ to_pair t1 t2 (Pair x y) = (t1 x,t2 y) ∧ to_pair t1 t2 (Num v4) = ARB

⊢ ∀P. (∀t1 t2 x y. P t1 t2 (Pair x y)) ∧ (∀t1 t2 v4. P t1 t2 (Num v4)) ⇒
      ∀v v1 v2. P v v1 v2