proposition: Lemma sub_Forall_add : forall T A (B : T -> formula), (forall t, A ⊆ B t) -> A ⊆ ∀t, B t.
proof: Proof. intros T A B HAB π [t Hπ]. now apply (HAB t). Qed.
imports: RelationClasses Morphisms ClassicalRealizability.ShallowEmbedding ClassicalRealizability.Tactics ClassicalRealizability.BasicResults