proposition: Lemma AS6 (T U: Set) (R: property): T = U -> R T <-> R U.
proof: Proof. move => h. have rr: R U <-> R U by done. exact: (eq_ind_r (fun t => R t <-> R U) rr h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)