explicitly naming components of dependent pair

Stream: Is there code for X?

[Arnav Sabharwal]

inductive HeadT where
| first
| second

def dep (a : HeadT) :=
  match a with
  | .first => Nat
  | .second => Bool

def dep_pair := @Sigma.mk HeadT dep HeadT.second true

-- dummy example
example : dep_pair = @Sigma.mk HeadT dep HeadT.second true := by {
  unfold dep_pair
  -- how to access fst and snd from here
  trivial
}

In the above example, is there a way to assign names to fst and snd when unfolding the dependent pair? Thanks!

[Arnav Sabharwal]

(deleted)

[Notification Bot]

Arnav Sabharwal has marked this topic as resolved.

[Notification Bot]

Arnav Sabharwal has marked this topic as unresolved.

[Matt Diamond]

cases' dep_pair with a b?