What I wrote with words on the last slide is best expressed, I think, by the following rule, where I omit the Gamma in front of each line:

T type
A:T
B:T
X:T |- P top
P[A/X] type
P[B/X] type
R:P[B/X]
e:Id0 T A B
————————
trb0(R,*e,*X.P,*A,*B,*T):P[A/X]

where

"P top” signifies that P is a syntactically correct type expression but need not be well-formed (well typed, derivable) in Gamma,

the “*” in front of an argument as in “ *e “ signifies a non-essential argument, such arguments are ignored when two expressions are compared for alpha-equivalence.

This is semantically acceptable if Id0 is interpreted as exact equality.

Syntactically we have the case when the well-formed sentences form something like an ideal in a ring because one operation has as one of its arguments an element of the ambient structure (raw typing judgements).

This came out stranger than I expected.

Vladimir.