fact: Definition pfamily_mem y mD (mF : aT -> mem_pred rT) := family (fun i : aT => if in_mem i mD then pred_of_simpl (mF i) else pred1 y).
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple)