proposition: Lemma eq_in_pmap (aT : eqType) rT (f1 f2 : aT -> option rT) s : {in s, f1 =1 f2} -> pmap f1 s = pmap f2 s.
proof: Proof. by elim: s => //= a s IHs /forall_cons [-> /IHs ->]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)