proposition: Lemma ForAll_tl (P : ∞A → Prop) s : ForAll P s → ForAll P (tl s).
proof: Proof. apply (ForAll_Str_nth_tl 1). Qed.
imports: MathClasses.theory.CoqStreams MathClasses.implementations.peano_naturals MathClasses.interfaces.abstract_algebra