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