proposition: Lemma coerce_sym (T T' : X) (s : f T) (s' : f T') : coerce T' s = Some s' -> coerce T s' = Some s.
proof: Proof. rewrite /coerce; case: eqPc => //= h; case: eqPc => //. by move=> h'/= [<-]; subst T'; rewrite -!eq_rect_eq. by rewrite {1}h; auto. Qed.
imports: mathcomp(all_ssreflect)