1 2 3 4 5 6 7
Require Setoid. Goal forall {T}(a b : T), b=a -> {c | c=b}. Proof. intros T a b H. try setoid_rewrite H. Abort.