Progress Theorem for the Simply Typed Lambda Calculus logic Heine-Borel Compactness from Dyadic Bar Compactness logic Curry–Howard Soundness of Type Checking for a Fixed Dependent Type Theory logic Ultrafilter Extension Lemma logic Diagonal Elementary Embedding into an Ultrapower logic Robinson Diagram Lemma logic Numerical Existence Property for Heyting Arithmetic logic Extensional Predicates Define Subobjects logic