Sigma.mk and length-n-tuples

Stream: lean4

[Dean Young]

I've got something like this:

def A := Sigma fun (p : Prop)=>  Sigma fun (q : Prop)=> Prop

And I wanted to know how I might use a length n-tuple as notation to introduce an element of A, instead of nested length 2 tuples. Is that ever done?

[Reid Barton]

It should just work

[Dean Young]

Reid Barton said:

It should just work

ok great. I should have tried it anyways.