ssreflect inversion, I need two equations instead of one

Question

I have next definitions (code can be compiled):

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Set Asymmetric Patterns.

Unset Strict Implicit.
Unset Printing Implicit Defensive.

Inductive val : Set := VConst of nat | VPair of val & val.
Inductive type : Set := TNat | TPair of type & type.

Inductive tjudgments_val : val -> type -> Prop :=
| TJV_nat n :
    tjudgments_val (VConst n) TNat
| TJV_pair v1 t1 v2 t2 : 
    tjudgments_val v1 t1 ->
    tjudgments_val v2 t2 ->
    tjudgments_val (VPair v1 v2) (TPair t1 t2).

And I would like to prove the following lemma:

Lemma tjexp_pair v1 t1 v2 t2 (H : tjudgments_val (VPair v1 v2) (TPair t1 t2)) :
  tjudgments_val v1 t1 /\ tjudgments_val v2 t2.
Proof.
  case E: _ _ / H => // [v1' t1' v2' t2' jv1 jv2].
  (* case E: _ / H => // [v1' t1' v2' t2' jv1 jv2]. *)

• The case E: _ _ / H => // [v1' t1' v2' t2' jv1 jv2]. leaves me with E : VPair v1 v2 = VPair v1' v2'.
• The case E: _ / H => // [v1' t1' v2' t2TPair t1 t2 = TPair t1' t2'' jv1 jv2]. leaves me with E : TPair t1 t2 = TPair t1' t2'.

But it looks to me like I need both of them together. How to?

Answer 1

There is a way of using inversion's power with ssreflect tactics.

Derive Inversion tjudgments_val_inv with (forall v t, tjudgments_val v t).

You can use it with elim/tjudgments_val_inv: H.

The proof is straightforward after this.

Answer 2

In such a case, you can use the very handy inversion tactic an enhancement of the case tactic, which automatically does the kind of work of indices you are manually trying to do. Here inversion H is almost enough to finish the proof.