fact: Definition up_subst_subst_exp_exp (sigma : fin -> exp ) (tauexp : fin -> exp ) (theta : fin -> exp ) (Eq : forall x, (funcomp (subst_exp tauexp) sigma) x = theta x) : forall x, (funcomp (subst_exp (up_exp_exp tauexp)) (up_exp_exp sigma)) x = (up_exp_exp theta) x := fun n => match n with | S n => eq_trans (compRenSubst_exp shift (up_exp_exp tauexp) (funcomp (up_exp_exp tauexp) shift) (fun x => eq_refl) (sigma n)) (eq_trans (eq_sym (compSubstRen__exp tauexp shift (funcomp (ren_exp shift) tauexp) (fun x => eq_refl) (sigma n))) (ap (ren_exp shift) (Eq n))) | 0 => eq_refl end.
imports: Undecidability.HOU(std.std)