start

Rejestracja warunkowa

registration
  let x1 be Θ1;
   .....
  let xn be Θn;
  cluster η1 ... ηk -> ξ1 ... ξm for Θ(x1,...,xn);
  coherence
  proof      :: thesis: for x being Θ(x1,...,xn) st x is η1 ... ηk
           ::       holds x is ξ1 ... ξm
    let x be Θ(x1,...,xn) ;
    assume x is η1 ... ηk;
    thus x is ξ1;
      ....
    thus x is ξm;
  end;
end;

gdzie η₁, ..., η_k, ξ₁, ..., ξ_m są przymiotnikami, do których typów definiowalności rozszerza się typ Θ(x₁,...,x_n). Przymiotnik η_i lub ξ_i może mieć argumenty jawne (τ_i,1,...,τ_i,ni) zależne od x₁,...,x_n.

Rejestracja powoduje automatyczne dołączanie przymiotników ξ₁(τ₁,...,τ_n), ..., ξ_m(τ₁,...,τ_n) do typu η₁(τ₁,...,τ_n) ... η_k(τ₁,...,τ_n) Θ(τ₁,...,τ_n).