In dependently typed type theory there's a equality type. Usually when this type is defined, a number of utilities, namely cong and subst are introduced. How expressive they are? Is it possible to express everything we can with eliminator for equality with them?
No, you can't prove uniqueness of identity proofs only with cong, subst and eliminator.
uip : {α : Level} {A : Set α} {x y : A} -> (p q : x ≡ y) -> p ≡ q
Here is the explanation: http://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/