proposition: Theorem strong_ind_seq_with_prop {A : Type} {P : nat -> (nat -> A) -> Prop} (HypP : dep_only_on_start P) (a0 : A) (H0 : P 0 (const_seq a0)) (Hstep : forall (k : nat) (prev : nat -> A), (forall l : nat, l <= k -> P l prev) -> {a : A | forall l : nat, l <= (S k) -> P l (const_seq_from a (S k) prev)}) : {seq : nat -> A | forall k : nat, P k seq}.
proof: Proof. enough {seq : nat -> A | forall k : nat, forall l : nat, l <= k -> P l seq} as [seq Hseq]. { exists seq. apply reformulate_final_prop_strong; exact Hseq. } apply (ind_seq_with_prop (quant_over_start_dep_only_on_start HypP) a0). - apply reformulate_base_prop_strong; exact H0. - exact Hstep. Defined.
imports: Lia Arith Arith.Compare ClassicalChoice ChoiceFacts Libs.Analysis.SubsequencesMetric