proposition: Lemma sub_Forall_cross : forall T A (B : T -> formula), (∀t, A → B t) ≈ A → ∀t, B t.
proof: Proof. intros; split; Ksolve. Qed.
imports: RelationClasses Morphisms ClassicalRealizability.ShallowEmbedding ClassicalRealizability.Tactics ClassicalRealizability.BasicResults