proposition: Lemma insub_eqE : insub_eq =1 insub.
proof: Proof. rewrite /insub_eq => x; set b := P x; rewrite [in LHS]/b in (Db := erefl b) *. by case: b in Db *; [rewrite insubT | rewrite insubF]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool)