proposition: Lemma Forall_comm : forall T₁ T₂ (A : T₁ -> T₂ -> formula), (∀t, ∀u, A t u) ≈ ∀u, ∀t, A t u.
proof: Proof. intros ? ? ? π; split; intro; dec π; find. Qed.
imports: RelationClasses Morphisms ClassicalRealizability.ShallowEmbedding ClassicalRealizability.Tactics ClassicalRealizability.BasicResults