Considering these definitions (where Formula is an usual modal logic formula):

```
Definition LabelledHyp : Type := (nat * Formula)%type.
Definition LCtx : Type := slist LabelledHyp.
```

I'm able to define an Inductive like this:

```
Inductive DC_Proof : LCtx -> LCtx -> Formula -> Prop :=
| dc_thyp : forall (D: LCtx) (G G': LCtx) (n : nat) (A: Formula),
DC_Proof D ((G,(pair n A));G') A
```

but is it possible to define it with LabelledHyp and is there a way to destruct the pair? Something like:

```
Inductive DC_Proof : LCtx -> LCtx -> Formula -> Prop :=
| dc_thyp : forall (D: LCtx) (G G': LCtx) ((n, A) : LabelledHyp),
DC_Proof D ((G,(pair n A));G') A
```

And slist is my definition for snoc lists but it's replaceable for lists with no problem

What you are looking for looks like the so-called Irrefutable patterns. In a definition you could write something like

```
Definition dc_thyp (D G G' : LCtx) (l : LabelledHyp) := let 'pair n A := l in …
```

but because of the restriction on what a constructor type can be, you cannot literally do this here. The closest I got was

```
Inductive DC_Proof : LCtx -> LCtx -> Formula -> Prop :=
| dc_thyp : forall (D: LCtx) (G G': LCtx) (l : LabelledHyp),
DC_Proof D ((G,(pair n A));G') (let 'pair _ A := l in A).
```

Thanks, and as you said I'm not able to find a way to use the let inside as in a `Definition`

, I'll keep looking for a way

Last updated: Sep 26 2023 at 12:02 UTC