proposition: Lemma L_fin_ok i : L_spec (\F i) (L_fin i).
proof: Proof. rewrite /L_spec (Finite_ref i) g2h_h2gK; apply L_fin_ok. Qed.
imports: mathcomp(all_ssreflect zify) hydras(T1) hydras(Canon Paths Large_Sets) gaia_hydras(T1Bridge GCanon GPaths) gaia(ssete9)