proposition: Lemma varLRen_pure_term (xipure_term : ( nat ) -> nat ) : funcomp (ren_pure_term xipure_term) (pure_var ) === funcomp (pure_var ) xipure_term .
proof: Proof. exact ((fun x => eq_refl)). Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms