Pattern match error

Using Coq
11

So now I have this:

Fixpoint amalg {ctx} {a} {b}
   (x : conv ctx (a -> b)) (y : conv ctx a) : conv ctx b.
Proof.
inversion x as [c1 ctx1 d1 | c1 ctx1 ? e1];
inversion y as [c2 ctx2 d2 | c2 ctx2 ? e2].
- exact (cc (sapp d1 d2)).
- exact (cn (amalg _ _ _ (cc (sapp sb d1)) e2)).
- exact (cn (amalg _ _ _ (cc (sapp (sapp sc sc) d2)) e1)). 
- exact (cn (amalg _ _ _ (amalg _ _ _ (cc ss) e1) e2)). (* the error is here *)
Defined.

But this gives the following error:

In environment
amalg : forall ctx a b : Type, conv ctx (a -> b) -> conv ctx a -> conv ctx b
ctx : Type
a : Type
b : Type
x : conv ctx (a -> b)
y : conv ctx a
c1 : Type
ctx1 : Type
a0 : Type
e1 : conv ctx1 (c1 -> a -> b)
H : (ctx1 * c1)%type = ctx
H0 : a0 = (a -> b)
c2 : Type
ctx2 : Type
a1 : Type
e2 : conv ctx2 (c2 -> a)
H1 : (ctx2 * c2)%type = ctx
H2 : a1 = a
The term "e2" has type "conv ctx2 (c2 -> a)" while it is expected to have type "conv ctx1 (c1 -> a)".

So I see that H and H1 can be used to prove (ctx1 * c1)%type = (ctx2 * c2)%type, but I don’t know how to prove that this implies that ctx1 = ctx2 and c1 = c2. It looks a lot like pair_equal_spec, but then on the type level. Unfortunately, there seems to be no prod_equal_spec.