proposition: Lemma varL_poly_type (sigmapoly_type : ( nat ) -> poly_type ) : funcomp (subst_poly_type sigmapoly_type) (poly_var ) === sigmapoly_type .
proof: Proof. exact ((fun x => eq_refl)). Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms