Ignore *.agdai files.
Added typed lambda calculus and an arithmetic language and proved/disproved subject expansion for those languages.
Fixed substitution.