우리는 도메인 이론(domain theory)에 기반한 새로운 증명 기법을 제시하여 종속형 타입 시스템(dependent type systems)의 핵심 메타-이론적 속성, 즉 정의적 역전 속성(definitional inversion properties), 다시 말해 타입 생성자(type constructors)의 단사성(injectivity)과 비혼동성(no-confusion)을 증명합니다. 이 증명 기법은 정규화(normalisation)와 독립적이며, 마틴-뢰프(Martin-Löf)의 원래 타입 이론(original type theory)의 '타입 내 타입(type-in-type)' 규칙에도 적용될 수 있습니다. 우리의 증명은 $\eta$ 법칙($\eta$ laws)이 존재하는 시스템에서 타입 생성자의 단사성을 확립한 최초의 사례입니다. 더 일반적으로, 이 기법은 Idris, Lean 또는 종속형 Haskell과 같은 시스템의 메타 이론에 의해 동기 부여되었으며 의도되었습니다. 이러한 시스템들의 근본적인 타입 이론은 비정규화(non-normalising)임이 알려져 있으며, 또한 Gödel의 제2 불완전성 정리(Gödel's second incompleteness theorem)로 인해 객체 논리 자체에서 정규화를 증명할 수 없는 MetaRocq나 Lean4Lean과 같은 프로젝트에도 적용될 수 있습니다. 우리는 작은 타입 이론에 이 방법을 소개한 다음, 이것이 어떻게 더 야심 찬 확장으로 일반화되는지 설명합니다.