From 179aad29c98fcb78c8859e8a044e342b9259dd02 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 14 Dec 2011 15:41:12 +0000 Subject: [PATCH] More stuff from CerCo to the standard library. --- matita/matita/lib/basics/types.ma | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma index 46cc5dd4b..1dcd79b7a 100644 --- a/matita/matita/lib/basics/types.ma +++ b/matita/matita/lib/basics/types.ma @@ -214,3 +214,10 @@ lemma pair_destruct_2: ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c. #A #B #a #b *; /2/ qed. + +lemma coerc_pair_sigma: + ∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x). +#A #B #P * #a #b #p % [@a | /2/] +qed. +coercion coerc_pair_sigma:∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x) +≝ coerc_pair_sigma on p: (? × ?) to (? × (Sig ??)). -- 2.39.2