proposition: Lemma compat_var Gamma i A gamma: nth Gamma i = Some A -> G Gamma gamma -> E A (gamma i).
proof: Proof. intuition. Qed.
imports: Morphisms Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics confluence typing order)