Gallery of programs Intro: introduction to Equations, demonstrating its features (source). Polynomials: a reflexive tactic for solving boolean tautologies (source). HoTT_light: basics of the HoTT library implemented using a logic in Type (source). STLC: strong normalization of simply-typed lambda-calculus with products using hereditary substitutions (source). MoreDep: part of chapter 8 of Adam Chlipala’s CPDT (source). String Matching: beginning of example by Nicky Vazou on string matching, uses well-founded recursion (source). Rose Trees: nested well-founded recursion (source). Nested mutual recursion: structural mutual and nested recursion (source). General recursion: working with general recursive functions, without worrying about termination proofs (source).