Public statement.

theorem AVenhance.IsStreamSeq.adm_pred {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (h : IsStreamSeq I Φ) (m : ℕ) : IsAdmissibleStream (Φ (m - 1))

Admissibility of φ_{m-1} for every m (so the flow X_{m-1} of b_{m-1} exists), read off IsStreamSeq: for m ≥ 1 it is the ∃ h of the definition, for m = 0 (Φ (0-1) = Φ 0 = 0) it is trivial. No closure theorem is used and no premise ∀ m, IsAdmissibleStream (Φ m).