proposition: Lemma varLRen_term (xipoly_type : ( nat ) -> nat ) (xiterm : ( nat ) -> nat ) : funcomp (ren_term xipoly_type xiterm) (var ) === funcomp (var ) xiterm .
proof: Proof. exact ((fun x => eq_refl)). Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms