Rejestracja redukcji

registration
  let x1 be Θ1;
  .....
  let xn be Θn;
  reduce τ -> τ';
  reducibility
  proof
     thus τ = τ';
  end;
end;

Rejestracja redukcji powoduje automatyczne dołączanie równości τ(τ₁,...,τ_n) = τ'(τ₁,...,τ_n) gdy występuje term τ(τ₁,...,τ_n).