proposition: Theorem eq_dep_eq_positive : forall (P:positive->Type) (p:positive) (x y:P p), eq_dep positive P p x p y -> x = y.
proof: Proof. apply eq_dep_eq_dec. decide equality. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef