## StringBase

## BaseLists

## Size

## internalize_demo

## Lists

## LProd

## LProp

## LBool

## Subst

## internalize_tac

## Base

- Base Library for ICL
- Iteration
- Decidability
- Lists
- Filter
- Element removal
- Duplicate-free lists
- Cardinality
- Power lists
- Finite closure iteration

## Encoding

## ARS

## LTactics

## Reflection

## crush_no_refl_ideas

## Tactics_old

## SumBool

## intermediate

## internalize_def

## LOptions

## LvwClos_Eval

## Lvw

- Syntax of the weak call-by-value lambda calculus
- Notation using binders
- Important terms
- Substitution
- Important definitions
- Size of terms
- Reduction
- Properties of the reduction relation
- Equivalence
- Definition of convergence
- Eta expansion
- Useful lemmas