proposition: Lemma nat_bounded_forall_true (f : nat -> bool) (n : nat) : nat_bounded_forall f n = true -> f n = true.
proof: Proof. intros. induction n. - simpl in *. assumption. - simpl in *. apply andb_prop in H. destruct H. assumption. Qed.
imports: Coq(FunctionalExtensionality Lia PeanoNat ProofIrrelevance ProofIrrelevanceFacts) ZornsLemma(FiniteTypes FunctionProperties) Coq(RelationClasses)