Theory cv_rep

⊢ ∀pre_cond cv_tm from_fun hol_tm.
    cv_rep pre_cond cv_tm from_fun hol_tm ⇔
    pre_cond ⇒ from_fun hol_tm = cv_tm

⊢ ∀x y. implies x y ⇔ x ⇒ y

⊢ b ⇒ b ⇒ c ⇔ b ⇒ c

⊢ b1 ⇒ b2 ⇒ c ⇔ b2 ⇒ b1 ⇒ c

⊢ ∀f. UNCURRY f = (λx'. case x' of (x,y) => f x y)

⊢ c2n (Num n) = n ∧ c2n (Pair x y) = 0 ∧ (c2b (Num n) ⇔ n ≠ 0) ∧
  (c2b (Pair x y) ⇔ F)

⊢ cv_if c x x = x

⊢ (∀v. cv_proj [] v = v) ∧
  (∀xs v. cv_proj (T::xs) v = cv_fst (cv_proj xs v)) ∧
  ∀xs v. cv_proj (F::xs) v = cv_snd (cv_proj xs v)

⊢ ∀P. (∀v. P [] v) ∧ (∀xs v. P xs v ⇒ P (T::xs) v) ∧
      (∀xs v. P xs v ⇒ P (F::xs) v) ⇒
      ∀v v1. P v v1

⊢ ∀v xs. cv_size (cv_proj xs v) ≤ cv_size v

⊢ cv_rep p (cv (g a)) f x ⇒
  ∀cv_a p_a. cv_rep p_a cv_a g a ⇒ cv_rep (p_a ∧ p) (cv cv_a) f x

⊢ cv_rep p y f x ⇒ from_to f t ⇒ p ⇒ x = t y

⊢ b ⇒ cv_rep p x y z ⇔ cv_rep (b ∧ p) x y z

⊢ ∀f n. cv_rep T (f n) f n

⊢ (c2b (cv_ispair cv_v) ⇔ ∃x1 x2. cv_v = Pair x1 x2) ∧
  (c2b (cv_lt (Num 0) cv_v) ⇔ ∃k. cv_v = Num (SUC k)) ∧
  (c2b (cv_lt (Num (NUMERAL (BIT1 n))) (cv_fst cv_v)) ⇔
   ∃k z. cv_v = Pair (Num k) z ∧ NUMERAL (BIT1 n) < k) ∧
  (c2b (cv_lt (Num (NUMERAL (BIT2 n))) (cv_fst cv_v)) ⇔
   ∃k z. cv_v = Pair (Num k) z ∧ NUMERAL (BIT2 n) < k) ∧
  (cv_fst cv_v = Pair x y ⇔ ∃z. cv_v = Pair (Pair x y) z) ∧
  (cv_snd cv_v = Pair x y ⇔ ∃z. cv_v = Pair z (Pair x y)) ∧
  (cv_fst cv_v = Num (SUC k) ⇔ ∃z. cv_v = Pair (Num (SUC k)) z) ∧
  (cv_snd cv_v = Num (SUC k) ⇔ ∃z. cv_v = Pair z (Num (SUC k)))

⊢ (if n = 0 then x else y) = if 0 < n then y else x

⊢ 0 < n ⇔ n ≠ 0

⊢ cv_fst = cv_proj [T] ∧ cv_snd = cv_proj [F] ∧
  cv_proj xs (cv_proj ys b) = cv_proj (xs ⧺ ys) b