proposition: Theorem inj_right_pair : forall (P:A -> Type) (y y':P x), existT P x y = existT P x y' -> y = y'.
proof: Proof. intros. cut (proj (existT P x y) y = proj (existT P x y') y). simpl in |- *. case (eq_dec x x). intro e. elim e using K_dec; trivial. intros. case n; trivial. case H0. reflexivity. Defined.
imports: Equations.Init Equations.Prop.Classes