Set Implicit Arguments.
Set Strict Implicit.

Section ClassReify.
  Variable P Q : Type.
  Variable D : P -> Q.

  Class ClassReify (v : Q) : Type :=
  { reify : P
  ; reify_sound : D reify = v
  }.
End ClassReify.

Require Import Lists.List.

Section ListReify.
  Variables (T U : Type) (f : T -> U).

  Global Instance  Reflect_nil : ClassReify (map f) nil :=
  { reify := nil 
  ; reify_sound := refl_equal
  }.

  Global Instance  Reflect_cons a b (Ra : ClassReify f a) (Rb : ClassReify (map f) b) 
  : ClassReify (map f) (a :: b).
(* Goal: @ClassReify (list T) (list U) (@map T U f) (@cons U a b) *)
  refine {| reify := cons (@reify _ _ _ _ Ra) (@reify _ _ _ _ Rb) |}.
(* Goal: @eq (list U) (@map T U f (@cons T (@reify T U f a Ra) (@reify (list T) (list U) (@map T U f) b Rb))) (@cons U a b) *)
  simpl; f_equal; eapply reify_sound.
  Defined.
End ListReify.
