From Undecidability.Shared.Libs.PSL Require Import Base FinTypes.
From Coq Require Import EqdepFacts List.

#[global]
Instance eqType_depPair (F : eqType) (a : F eqType) : eq_dec {f : F & a f}.
Proof.
  intros [x fx] [y fy]. eapply dec_transfer. now rewrite eq_sigT_iff_eq_dep.
  decide (x=y).
  subst y. decide (fx = fy).
  +subst fy. left. reflexivity.
  +right. intros eq. apply n. apply Eqdep_dec.eq_dep_eq_dec in eq. auto. intros. decide (=y);econstructor;eassumption;eauto.
  +right. intros eq. now inv eq.
Qed.


#[global]
Instance finType_depPair (F : finType) (a : F finType) : finTypeC (EqType( {f : F & a f} )).
Proof.
  exists (undup (concat (map ( f map ( x existT a _ x) (elem (a f))) (elem F)))).
  intros H. hnf in H. apply dupfreeCount. now apply dupfree_undup.
  rewrite undup_id_equi. apply in_concat_iff.
  exists (( f : F map ( x : a f existT ( x0 : F a ) f x) (elem (a f))) ( H)).
  split.
  -rewrite in_map_iff. destruct H. cbn. exists e. split.
   +reflexivity.
   +apply countIn. setoid_rewrite enum_ok. .
  -rewrite in_map_iff. eexists. split. reflexivity.
   apply countIn. setoid_rewrite enum_ok. .
Qed.


#[export] Hint Extern 4 (finTypeC (EqType ({_ : _ & _}))) eapply finType_depPair : typeclass_instances.