proposition: Lemma varL_term (sigmapoly_type : ( nat ) -> poly_type ) (sigmaterm : ( nat ) -> term ) : funcomp (subst_term sigmapoly_type sigmaterm) (var ) === sigmaterm .
proof: Proof. exact ((fun x => eq_refl)). Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms