[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Sequents and entailment rather than implication and universal quantification. coherent mathematics The problem is with infinite sets: one could prove function extensionality for functions with domain a finite set. Same goes with choice. category: redirected to nlab