proposition: Lemma maxset_eq P1 P2 E : P1 =1 P2 -> maxset P1 E = maxset P2 E.
proof: Proof. move=> P1P2. rewrite /maxset. rewrite P1P2. congr (_ && _). apply/forallP/forallP => /= H x. by rewrite -P1P2 H. by rewrite P1P2 H. Qed.
imports: mathcomp(all_ssreflect)