lemma ZipConsCons' [simp]:
  "zip'(X_Cons x xs, X_Cons y ys) = X_Cons (x, y) (zip'(xs, ys))"
  by (rule ZipConsCons) rule
  
lemma [elim]:
  "length' (X_Cons x xs) = 0' \<Longrightarrow> P"
  sorry

lemma [elim]:
  "k +' length'(xs) = 0' \<Longrightarrow> P"
  sorry

lemma [elim]:
  "0' = 1' \<Longrightarrow> P"
  sorry

lemma plus_inject_l:
  "(a::X_Int) +' b = a +' c \<Longrightarrow> b = c"
  sorry

theorem ZipSpec:
  assumes "length'(xs) = length'(ys)"
  shows "unzip (zip' (xs, ys)) = (xs, ys)"
using assms proof (induct xs arbitrary: ys)
  case X_Nil then show ?case apply (simp_all add: UnzipNil LengthCons)
    apply (cases ys) apply simp_all apply (drule sym) apply auto done
next
  case (X_Cons x xs) then show ?case apply (cases ys)
    apply (auto simp add: ZipConsNil UnzipNil LengthCons UnzipCons Let_def split_def)
    apply (drule plus_inject_l, auto)
    apply (drule plus_inject_l, auto)
    done
qed