我有下一个定义(可以编译代码):
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).
我想证明以下引理:
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]. *)
case E: _ _ / H => // [v1' t1' v2' t2' jv1 jv2].
离开E : VPair v1 v2 = VPair v1' v2'
我。case E: _ / H => // [v1' t1' v2' t2TPair t1 t2 = TPair t1' t2'' jv1 jv2].
离开E : TPair t1 t2 = TPair t1' t2'
我。
但在我看来,我需要他们两个在一起。如何?