Working on a polymorphic version of MirrorCore I have been working a lot with heterogeneous lists and proof-relevant membership. The later is the source of this challenge problem.

A shell of the code is available as a gist, and my solution is available as well.

## The Function

Suppose that I want to implement the following version of hetergeneous decideable equality on them:

```
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.
Definition member_heq
: forall (T : Type) (l r : T) (ls : list T) (m : member l ls),
member r ls -> member r (del_member m) + (l = r)
```

Essntially `del_member`

computes the list that is the result of removing the position marked by `m`

.
You can see how this might be useful in the context of manipulating syntax because when you replace a unification variable (notated by `m`

) with an expression, you will get an expression that has all the same unification variables but without any occurances of `m`

.

Given that, what `member_heq`

is doing is comparing two `member`

s and returning the translation of the second into the `del_member`

ed list in the case that they are not the same, or proving that the two types are the same.
Parametricity will guarantee that if we return an `inr pf`

for any `pf`

, that the two memberes must be equal; however, we’ll prove that as the second (more challenging) part of the challenge.

First part of the challenge is to implement `member_heq`

**without using any axioms or additional assumptions**.
If you are going to try to do it with tactics, note that tactics such as `dependent induction`

and `dependent destruct`

can silently introduce axioms, so you should check the proof at the end with `Print Assumptions member_heq.`

.
Don’t forget to finish your definition with `Defined`

or you won’t be able to prove anything about the function!

## The verification

The second step, which is significantly more challenging, is to prove that if `member_heq a b`

returns `inr pf`

then `a = b`

.
Of course, you won’t simply be able to simply write `a = b`

since the two terms have different types, but the `pf`

proof shows that these two types are *provably* equal.

Here’s the statement of the second part of the challenge.

```
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.
```

As before, no axioms. The proof needs to reduce completely, i.e.

```
member_heq_eq MZ MZ eq_refl eq_refl = eq_refl
```

and

```
member_heq_eq (MN MZ) (MN MZ) eq_refl eq_refl = eq_refl
```

## Finished?

If you’ve found a solution that you’d like to share, leave a link in the comments.