last one

coq-community · Jul 17, 2024 · e06e7c1 · e06e7c1
1 parent 4c14009
commit e06e7c1
Showing 1 changed file with 3 additions and 6 deletions.
diff --git a/theories/Param_vector.v b/theories/Param_vector.v
@@ -207,12 +207,9 @@ Definition tR_sym_fK {A A' : Type} (AR : A -> A' -> Type) {n n' : nat} (nR : nat
   (v : t A n) (v' : t A' n') (vR : tR A A' AR n n' nR v v') :
      g (f (f vR)) = vR.
 Proof.
-elim: vR => // {}n {}n' {}nR a a' aR {}v {}v' vR {2}<-/=.
-case: _ / Param_nat_symK (tR_sym_f _ _ _).
-
-Fail by case: _ / Param_nat_symK (f _).
-admit.
-Admitted.
+elim: vR => // {}n {}n' {}nR a a' aR {}v {}v' vR {2}<-/=; rewrite /g /=.
+by case: _ / Param_nat_symK (tR_sym_f _ _ _).
+Qed.
 
 Definition tR_sym_fE {A A' : Type} (AR : A -> A' -> Type) {n n' : nat} (nR : natR n n')
   (v : t A n) (v' : t A' n') (vR : tR A A' AR n n' nR v v') :