proposition: Lemma ForAll_True (s : ∞A) : ForAll (λ _, True) s.
proof: Proof. revert s. cofix F. intros. constructor; trivial. Qed.
imports: MathClasses.theory.CoqStreams MathClasses.implementations.peano_naturals MathClasses.interfaces.abstract_algebra