declSig to Expr

Stream: lean4

[Jon Eugster]

I'm very new to metacoding and I have a (hopefully simple) question. How do I turn an element (call it sig) of type TSyntax `Lean.Parser.Command.declSig into an Expr?

For context, I am adding a new theorem to context using let thmStatement ← `(theorem $(mkIdent name) $sig $val) and I would
like to check if it is the same statement as another (specified) theorem that's already in context.

I get the existing theorem's type with ((← getEnv).constants.map₁.find! thmName.getId).type, which is an Expr:

forall {α : Type.{u}} (x : α), Membership.mem.{u, u} α (Set.{u} α) (Set.instMembershipSet.{u} α) x (Set.univ.{u} α)

and dbg_trace sig gives the following:

(Command.declSig
 [(Term.implicitBinder "{" [`A] [":" (Term.type "Type" [])] "}") (Term.explicitBinder "(" [`x] [":" `A] [] ")")]
 (Term.typeSpec ":" («term_∈_» `x "∈" (Term.typeAscription "(" `univ ":" [(Term.app `Set [`A])] ")"))))

which is a TSyntax `Lean.Parser.Command.declSig. I'd guess that's some sort of elaboration of sig but I don't understand elaboration enough yet, so I'm also struggling constructing a compact mwe.