Hey! So I started to learn some Coq today (I’ve done some Agda). I’m doing stuff with session types, and I have the following:

```
Require Import Unicode.Utf8.
Inductive type (A : Type) : Set :=
| End : type A
| Send : type A → type A
| Receive : type A → type A
| Branch : list (type A) → type A
| Select : nat → type A.
Fixpoint dual {A} (t₁ : type A) (t₂ : type A) : Prop :=
match (t₁, t₂) with
| (End _, End _) => True
| (Send _ t₁', Receive _ t₂') => dual t₁' t₂'
| (Receive _ t₁', Send _ t₂') => dual t₁' t₂'
| (Branch _ ts, Select _ n) => True
| (Select _ n, Branch _ ts) => True
| _ => False
end.
Module Type Basis.
Parameter A : Type.
Parameter var : type A → Type.
End Basis.
Module Process (B : Basis).
Import B.
Inductive Process : type A → Set :=
| P0 : Process (End A)
| PNew : ∀ {t}, Process t → Process t
| PInput : ∀ {t : type A}, Process t → Process (Send A t)
| POutput : ∀ {t}, Process t → Process (Receive A t)
(* branch needs an heterogenous list of types *)
| PComp : ∀ {t₁ t₂}, Process t₁ → Process t₂ → dual t₁ t₂ → Process (End _)
.
Theorem meh : dual (Send A (End A)) (Receive A (End A)).
simpl. trivial. Qed.
Check PComp (PInput P0) (POutput P0) True.
End Process.
```

While the theorem holds, the Check command is unable to see that `PInput P0`

and `POutput P0`

have types that are `dual`

. How should I get the computation to “advance” so that Coq sees this?