proposition: Theorem Theorem_4_5 (a: T1)(Ha : T1nf a) (A B : seq nat) (HA : Sorted.Sorted Peano.lt A) (HB : Sorted.Sorted Peano.lt B) (HAB : List.incl A B) : largeS a A -> largeS a B.
proof: Proof. rewrite /largeS; apply Theorem_4_5 => //; by rewrite hnf_g2h. Qed.
imports: mathcomp(all_ssreflect zify) hydras(T1) hydras(Canon Paths Large_Sets) gaia_hydras(T1Bridge GCanon GPaths) gaia(ssete9)