proposition: Lemma eq_sigT_rw : forall T U F (a b : T) (pf : a = b) s, match pf in _ = x return @sigT U (F x) with | eq_refl => s end = @existT U (F b) (projT1 s) match pf in _ = x return F x (projT1 s) with | eq_refl => (projT2 s) end.
proof: Proof. destruct pf. destruct s; reflexivity. Qed.
imports: ExtLib.Structures.EqDep ExtLib.Tactics.Injection ExtLib.Tactics.EqDep