fact: Definition up_subst_subst_pure_term_pure_term (sigma : ( nat ) -> pure_term ) (taupure_term : ( nat ) -> pure_term ) (theta : ( nat ) -> pure_term ) (Eq : forall x, (funcomp (subst_pure_term taupure_term) sigma) x = theta x) : forall x, (funcomp (subst_pure_term (up_pure_term_pure_term taupure_term)) (up_pure_term_pure_term sigma)) x = (up_pure_term_pure_term theta) x := fun n => match n with | S n => eq_trans (compRenSubst_pure_term shift (up_pure_term_pure_term taupure_term) (funcomp (up_pure_term_pure_term taupure_term) shift) (fun x => eq_refl) (sigma n)) (eq_trans (eq_sym (compSubstRen_pure_term taupure_term shift (funcomp (ren_pure_term shift) taupure_term) (fun x => eq_refl) (sigma n))) (ap (ren_pure_term shift) (Eq n))) | 0 => eq_refl end.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms