Nearby theorems
|
|
brismu bridi |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > Home > Th. List > df-sub | |||
| Description: Definition of proper substitution following definition df-sb in [ILE] p. 0. This clever gadget breaks scoping to require that substitution is correct in both the case where {da} is free and the case where {da} is bound by mixing both cases, skipping grammatical analysis and scope-tracking entirely. |
| Ref | Expression |
|---|---|
| df-sub | ⊢ go [ ko'a / da ] broda gi ge ganai da du ko'a gi broda gi su'o da zo'u ge da du ko'a gi broda |
| Copyright terms: Public domain | W3C validator |