proposition: Lemma renRen_term (xipoly_type : ( nat ) -> nat ) (xiterm : ( nat ) -> nat ) (zetapoly_type : ( nat ) -> nat ) (zetaterm : ( nat ) -> nat ) (s : term ) : ren_term zetapoly_type zetaterm (ren_term xipoly_type xiterm s) = ren_term (funcomp zetapoly_type xipoly_type) (funcomp zetaterm xiterm) s .
proof: Proof. exact (compRenRen_term xipoly_type xiterm zetapoly_type zetaterm (_) (_) (fun n => eq_refl) (fun n => eq_refl) s). Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms