fact: Definition up_ren_subst_exp_exp (xi : fin -> fin ) (tau : fin -> exp ) (theta : fin -> exp ) (Eq : forall x, (funcomp tau xi) x = theta x) : forall x, (funcomp (up_exp_exp tau) (upRen_exp_exp xi)) x = (up_exp_exp theta) x := fun n => match n with | S n => ap (ren_exp shift) (Eq n) | 0 => eq_refl end.
imports: Undecidability.HOU(std.std)