Shell of the proof of member_heq_eq.

member_heq_eq.v

Require Import Coq.Lists.List.
Require Import ExtLib.Data.HList.
Require Import ExtLib.Data.Member.

Set Implicit Arguments.
Set Strict Implicit.

Arguments MZ {_ _ _}.
Arguments MN {_ _ _ _} _.

Section del_val.
  Context {T : Type}.
  Variable ku : T.

  Fixpoint del_member (ls : list T) (m : member ku ls) : list T :=
    match m with
    | @MZ _ _ l => l
    | @MN _ _ ku' _ m => ku' :: del_member m
    end.
End del_val.

Section member_heq.
  Context {T : Type}.

  Definition member_heq (l r : T) (ls : list T) (m : member l ls)
  : member r ls -> member r (del_member m) + (l = r).
  Admitted.

  Lemma member_heq_eq
  : forall {l l' ls} (m1 : member l ls) (m2 : member l' ls) pf,
      member_heq m1 m2 = inr pf ->
      match pf in _ = X return member X ls with
      | eq_refl => m1
      end = m2.
  Proof.
  Admitted.

End member_heq.

Arguments member_heq_eq [_ _ _ _] _ _ _ _ : clear implicits.

Eval compute in member_heq_eq (@MZ _ 1 nil) MZ eq_refl eq_refl.

Eval compute in member_heq_eq (@MN _ 2 1 (2 :: 3 :: nil) MZ) (MN MZ) eq_refl eq_refl.