## Stream: Coq users

### Topic: Help with exist destruct in hypothesis

#### Mycroft92 (May 09 2024 at 15:55):

Hi,
I have a hypothesis as follows:

``````ctxt: Env.t ident
ck: clock
i: ident
b: bool
IHck: forall st : ST, assign_clk_type ck = Some st -> wst_clock ck st
st: ST
H: assign_clk_type (Con ck i b) = Some st
H': exists (st' : ST) (ty : ident),
st = st' ⊔ [ty] /\ assign_clk_type ck = Some st' /\ Env.find i ctxt = Some ty
1/1
wst_clock (Con ck i b) st
``````

I want to open up H' to 3 different hypotheses. Is there a cleaner way to do it other than repeated destruct on it?

Originally I applied (using `apply`) a result on the hypothesis to get H'. However I could not find a proper intro pattern to achieve the 3 destruct case I specified.

#### Quentin VERMANDE (May 09 2024 at 16:02):

You can do `destruct H' as [x [y [z [t u]]]]`.

#### Mycroft92 (May 09 2024 at 16:06):

Quentin VERMANDE said:

You can do `destruct H' as [x [y [z [t u]]]]`.

Thank you that was exactly what I was looking for! I guess I can use this directly in the apply as well. I couldn't figure out the intro pattern correctly so far.

#### Kenji Maillard (May 10 2024 at 08:02):

For nested "pairs" like this you can also use `destruct H' as (x & y & z & t & u)`.

#### Mycroft92 (May 10 2024 at 09:34):

Kenji Maillard said:

For nested "pairs" like this you can also use `destruct H' as (x & y & z & t & u)`.

Cool. This is even cleaner. Thanks for all the help.

Last updated: Jun 23 2024 at 03:02 UTC