proposition: Lemma G_up Gamma A gamma: G Gamma gamma -> G (A :: Gamma) (up gamma).
proof: Proof. eauto using G_cons, ren_closed_G, E_var. Qed.
imports: Morphisms Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics confluence typing order)