proposition: Lemma ex6_prop5a i (H:inc i L): inl_same_data (ex6_systemi i) (inl_restr (ex6_prop4 H)).
proof: Proof. by rewrite /ex6_systemi; case: (ixm (inc i L)) => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)