Library TreeAl

Require Import
  Coqlib
  Maps
  DLib.

Set Implicit Arguments.

Module Type TYPE_EQ.
  Variable s: Type.
  Variable t: Type.
  Variable t_of_s : st.
  Variable s_of_t : ts.
  Hypothesis inj : x : s, s_of_t (t_of_s x) = x.
  Hypothesis surj: x : t, t_of_s (s_of_t x) = x.
  Variable eq: (x y: s), {x = y} + {x y}.
End TYPE_EQ.

Module TYPE_EQ_PROP (X:TYPE_EQ).
  Lemma injective (a b: X.s) :
    a bX.t_of_s a X.t_of_s b.
  Corollary injective' (a b: X.s) :
    X.t_of_s a = X.t_of_s ba = b.
  Lemma tinjective (a b: X.t) :
    a bX.s_of_t a X.s_of_t b.
  Lemma tinjective' (a b: X.t) :
    X.s_of_t a = X.s_of_t ba = b.
End TYPE_EQ_PROP.

Module Z_EQ_POS : TYPE_EQ
    with Definition s := Z
    with Definition t := positive.
  Definition s := Z.
  Definition t := positive.
  Definition t_of_s (z: s) : t :=
    match z with
      | Z0xH
      | Zpos pxO p
      | Zneg pxI p
    end.
  Definition s_of_t (p: t) : s :=
    match p with
      | xHZ0
      | xO xZpos x
      | xI xZneg x
    end.
  Lemma inj : x : s, s_of_t (t_of_s x) = x.
  Lemma surj: x : t, t_of_s (s_of_t x) = x.
  Definition eq: (x y: s), {x = y} + {x y} :=
    Z_eq_dec.
End Z_EQ_POS.

Lemma fold_left_map:
   {A B C} (f: AB) (g: CBC) xs a,
    fold_left g (