proposition: Lemma instId_exp : subst_exp (var_exp ) = id .
proof: Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x => idSubst_exp (var_exp ) (fun n => eq_refl) (id x))). Qed.
imports: Undecidability.HOU(std.std)