proposition: Lemma varL_pure_term (sigmapure_term : ( nat ) -> pure_term ) : funcomp (subst_pure_term sigmapure_term) (pure_var ) === sigmapure_term .
proof: Proof. exact ((fun x => eq_refl)). Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms