# Untyped λ-calculus ```agda {-# OPTIONS --rewriting --confluence-check #-} module LC.index where import LC.Definitions import LC.Tests ```