proposition: Lemma injective_upRen_exp_exp delta: Injective delta -> Injective (upRen_exp_exp delta).
proof: Proof. intros H [| x] [| y]; eauto. all: cbn; discriminate. Qed.
imports: Undecidability.HOU(calculus.prelim calculus.terms calculus.syntax std.std) Morphisms Lia FinFun