proposition: Lemma coercible_sym (T T' : X) (s : f T) (s' : f T') : coercible T' s = coercible T s'.
proof: Proof. rewrite /coercible /coerce; case: eqPc; case: eqPc => //. - by move=> ? ?; subst T'; rewrite -!eq_rect_eq. - by move=> ? ?; exfalso; auto. Qed.
imports: mathcomp(all_ssreflect)