proposition: Lemma up_ren_ren (xi: nat -> nat) (zeta : nat -> nat) (rho: nat -> nat) (E: forall x, (xi >> zeta) x = rho x) : forall x, (up_ren xi >> up_ren zeta) x = up_ren rho x.
proof: Proof. intros [|x]. - reflexivity. - unfold up_ren. simpl. unfold funcomp. rewrite <- E. reflexivity. Qed.
imports: Undecidability.SystemF.SysF Morphisms