Bug in forgetting with letin

[tlringer]

This fails:

Definition append_vect (A : Type) (pv1 : sigT (vector A)) (pv2 : sigT (vector A)) :=
  let pv := append_vect_inner A pv1 pv2 in
  existT _ (projT1 pv) (projT2 pv).

Lift list vector in append as append_vect_lifted.

While this succeeds:

Definition append_vect (A : Type) (pv1 : sigT (vector A)) (pv2 : sigT (vector A)) :=
  existT _ (projT1 (append_vect_inner A pv1 pv2 )) (projT2 (append_vect_inner A pv1 pv2 )).

Lift list vector in append as append_vect_lifted.

Since we get an intermediate (vector A) in an unexpected place even though it eventually goes away. We should support this somehow. Forgetting in general is not very useful when going along the equivalence we have, honestly; would be better to use the other equivalence for this.