fact: Definition typingRen Delta delta Gamma := forall x A, nth Gamma x = Some A -> nth Delta (delta x) = Some A.
imports: List Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics)