proposition: Lemma eq_sigT_sig_eq X P (x1 x2:X) H1 H2 : existT P x1 H1 = existT P x2 H2 <-> {H:x1=x2 | rew H in H1 = H2}.
proof: Proof. split; intro H. - change x2 with (projT1 (existT P x2 H2)). change H2 with (projT2 (existT P x2 H2)) at 5. destruct H. simpl. exists eq_refl. reflexivity. - destruct H as (->,<-). reflexivity. Defined.