proposition: Theorem fst_split_map_eq : forall (A B : Type)(ls : list (A * B)), fst (split ls) = map fst ls.
proof: Proof. induction ls; intuition idtac; simpl in *. remember (split ls) as z. destruct z. simpl in *. congruence. Qed.
imports: FCF.FCF FCF.CompFold FCF.Array FCF.Hybrid