proposition: Lemma insubT x Px : insub x = Some (Sub x Px).
proof: Proof. do [case: insubP => [/SubP[y Py] _ <- | /negP// ]; rewrite SubK] in Px *. by rewrite (bool_irrelevance Px Py). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool)