proposition: Lemma forall_distribute : ∀ a {X} P, (∀ x, a → P x) → (a → ∀ (x : X), P x).
proof: Proof. intros. apply X0. assumption. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Structure.Terminal Category.Structure.Cartesian Category.Structure.Cartesian.Closed Category.Functor.Structure.Cartesian Category.Instance.Coq Category.Instance.AST Category.Tools.Represented