C.2.2.1 vs. C.3

Stream: lean4

[Dean Young]

I've got this example here, namely bob:

def Bob :=
Sigma fun (forall X : Prop, Unit)=>
Sigma fun (forall X : Prop, Unit)=>
Sigma fun (forall X : Prop,Unit) =>
Unit

Now I want to define something like this:

def justone (C : Bob) :=
  match C with
  | C => C.2.1

Now is there some alternative where instead of C.2.1 I could have done C.2?

I also was interested in the general situation with C.3, C.4, and so on. It's not a big deal I guess.

[Sebastian Ullrich]

This is what structures are for