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