Congruence for the λ-calculus

inductive Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Xi {Var : Type u} (R : Term Var → Term Var → Prop) : 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.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Xi.step_lc_r {Var : Type u} {R : Term Var → Term Var → Prop} {M N : Term Var} (hR : ∀ {M' N' : Term Var}, R M' N' → N'.LC) (step : Xi R M N) : N.LC

The right side of a congruence step is locally closed.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Xi.step_lc_l {Var : Type u} {R : Term Var → Term Var → Prop} {M N : Term Var} (hR : ∀ {M' N' : Term Var}, R M' N' → M'.LC) (step : Xi R M N) : M.LC

The left side of a congruence step is locally closed.