proposition: Lemma prl_subsets_prop2 S M (H:prl_subfam_hyp S M): projective_limit(projective_system_subsets H) = projective_limit S \cap (productb M).
proof: Proof. move:(prl_subsets_prop H) => [pa pb pc pd]. rewrite {1}/projective_limit pa pc pd. have dM: domain M = psI S by case: (H). move:(prl_subfam_prop1 H) => [_ h2 _ _ _]. set_extens t. move=> /Zo_P [ha hb]; apply/setI2_P; split; last by exact. move:ha => /setXb_P[ua ub uc]. rewrite dM in uc. have ha:inc t (productb (psE S)). apply/setXb_P; split => //. by rewrite ub dM ps_domain_E. rewrite ps_domain_E => i ii. by move: (H) => [_ _ hh _]; apply: (hh _ ii); apply: uc. apply/Zo_P; split => // i j lij. have xM: inc (Vg t j) (Vg M j). by apply: uc; rewrite - ps_substrate_r; order_tac. by rewrite - (h2 _ _ _ lij xM) - (hb _ _ lij). move =>/setI2_P [/Zo_P [ha hb] tp]; apply/Zo_P; split; first exact. move:tp => /setXb_P[ua ub uc]. move => i j lij. have wp: inc (Vg t j) (Vg M j). by apply: uc; rewrite dM -(ps_substrate_r); order_tac. by rewrite (h2 _ _ _ lij wp) - (hb _ _ lij). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)