proposition: Lemma set_to_T1_pr x (Hx: inc x T1) : set_to_T1 x = Bo Hx.
proof: Proof. rewrite /set_to_T1;case: (ixm (inc x T1)) => // Hy; apply: R_inj. by rewrite (B_eq Hx) (B_eq Hy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)