proposition: Lemma rel_True: singleton (Ro I) = True.
proof: Proof. apply: extensionality. move => t /set1_P ->; apply: R_inc. move => t [a <-]; apply /set1_P. have -> //: a = I by case:a. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)