Definition pred (T : Type) := T -> bool.

CoInductive mem_pred (T : Type) : Type :=  Mem : pred T -> mem_pred T.

Definition isMem (T : Type) pT topred mem :=
  mem = (fun p : pT => Mem T (fun x => topred p x)).

Record predType (T : Type) := PredType {
  pred_sort :> Type;
  topred : pred_sort -> pred T;
  _ : {mem | isMem _ _ topred mem}
}.

Definition mem (T : Type) (pT : predType T) : pT -> mem_pred T :=
  match pT return pT -> _ with
  | PredType _ _ _ (exist _ mem _) => mem
  end.

Definition predPredType (T : Type) :=
  PredType T (pred T) (fun x => x)
    (exist (isMem T (pred T) (fun x => x))
       (fun p => @Mem T (fun x : T => p x)) (eq_refl _)).

Module Type PredSig.
Parameter mkPred : forall T, (T -> bool) -> predPredType T.
End PredSig.

Module Pred : PredSig.
Definition mkPred T (p : T -> bool) := p.
End Pred.

Definition x :=
  mem unit (predPredType unit) (Pred.mkPred _ (fun _ => true)).

Extraction "hoge.ml" x.