fact: Fixpoint subst_exp (sigmaexp : fin -> exp ) (s : exp ) : _ := match s with | var_exp s => sigmaexp s | const s0 => const s0 | lam s0 => lam (subst_exp (up_exp_exp sigmaexp) s0) | app s0 s1 => app (subst_exp sigmaexp s0) (subst_exp sigmaexp s1) end.
imports: Undecidability.HOU(std.std)