proposition: Lemma mlarge_unicity a k l l' : mlarge a (index_iota k.+1 l.+1) -> mlarge a (index_iota k.+1 l'.+1) -> l = l'.
proof: Proof. rewrite /mlarge -!interval_def => Hl Hl'; by rewrite (mlarge_unicity _ _ _ _ Hl Hl'). Qed.
imports: mathcomp(all_ssreflect zify) hydras(T1) hydras(Canon Paths Large_Sets) gaia_hydras(T1Bridge GCanon GPaths) gaia(ssete9)