Congruence for the λ-calculus #
inductive
Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Xi
{Var : Type u}
(R : Term Var → Term Var → Prop)
:
Congruence closure of a relation.
- base
{Var : Type u}
{R : Term Var → Term Var → Prop}
{M N : Term Var}
: R M N → Xi R M N
The base relation.
- appL
{Var : Type u}
{R : Term Var → Term Var → Prop}
{Z M N : Term Var}
: Z.LC → Xi R M N → Xi R (Z.app M) (Z.app N)
Left congruence rule for application.
- appR
{Var : Type u}
{R : Term Var → Term Var → Prop}
{Z M N : Term Var}
: Z.LC → Xi R M N → Xi R (M.app Z) (N.app Z)
Right congruence rule for application.
- abs
{Var : Type u}
{R : Term Var → Term Var → Prop}
{M N : Term Var}
(xs : Finset Var)
: (∀ x ∉ xs, Xi R (M.open' (fvar x)) (N.open' (fvar x))) → Xi R M.abs N.abs
The ξ (xi) rule for lambda terms.