proposition: Lemma inj_pair2 : forall (P:A -> Type) (p:A) (x y:P p), existT P p x = existT P p y -> x = y.
proof: Proof. intros. eapply Coq.Logic.Eqdep_dec.inj_pair2_eq_dec; auto. Qed.
imports: ExtLib.Core.RelDec ExtLib.Tactics.Consider