fact: Definition upId_pure_term_pure_term (sigma : ( nat ) -> pure_term ) (Eq : forall x, sigma x = (pure_var ) x) : forall x, (up_pure_term_pure_term sigma) x = (pure_var ) x := fun n => match n with | S n => ap (ren_pure_term shift) (Eq n) | 0 => eq_refl end.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms