From 88c241032a5ed3f16a030d3a12fc9c9db4506741 Mon Sep 17 00:00:00 2001 From: Yosuke Tsuji Date: Thu, 1 Aug 2024 15:50:43 +0900 Subject: [PATCH] rewrite part of the proof of nindmatch_leq_nminmatch --- graph.v | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/graph.v b/graph.v index f488317..46c392d 100644 --- a/graph.v +++ b/graph.v @@ -1091,9 +1091,7 @@ rewrite 2!cardfE. set f : N -> M := fun n => [` (psi_M Mmax (val n)) ]. apply: (leq_card f). move=> e0 e1. -move/eqP => fe01. -apply/eqP. -move: fe01. +move/eqP => fe01; apply/eqP; move: fe01. move/(psi_inj Nind). rewrite /f. by rewrite 2!fsvalP => /(_ erefl erefl).