From d83b0b63880e4efd5b1f54cf23a8e0bed52a8e12 Mon Sep 17 00:00:00 2001 From: smolka Date: Wed, 19 Jun 2024 19:21:16 +0200 Subject: [PATCH] green --- coq/more.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/coq/more.v b/coq/more.v index 845171c..911dfa6 100644 --- a/coq/more.v +++ b/coq/more.v @@ -258,7 +258,7 @@ Qed. Fact R {X Y f g} : @inv (option X) (option Y) g f -> - forall x, Sigma y, match f (Some x) with Some y' => y = y' | None => f None = Some y end. + forall x, Sigma z, match f (Some x) with Some y => z = y | None => Some z = f None end. Proof. intros H x. destruct (f (Some x)) as [y|] eqn:E1. @@ -279,7 +279,7 @@ Proof. revert H3 H4. destruct (f (Some x)) as [y1|] eqn:E. - intros <-. rewrite <-E, H1. easy. - - intros <-. rewrite H1. rewrite <-E, H1. congruence. + - intros ->. rewrite H1. rewrite <-E, H1. congruence. Qed. Theorem bijection_option X Y : @@ -297,7 +297,7 @@ Proof. - hnf. intros [x|]; congruence. - hnf. intros [y|]; congruence. Qed. - + (*** Numeral Types *) Fixpoint num n : Type :=