proposition: Lemma isum_q5 I: sub I E -> substrate (ipartial_order I) = disjointU (restr f I).
proof: Proof. move => En; rewrite (orsum_sr (isum_q4 En)). congr disjointU; rewrite /fam_of_substrates Lgd; apply: Lg_exten => i iE. by rewrite LgV// ordinal_o_sr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)