1 include "basics/jmeq.ma".
2 include "basics/types.ma".
3 include "basics/list.ma".
5 definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.
\ 5a title="Sigma" href="cic:/fakeuri.def(1)"
\ 6Σ
\ 5/a
\ 6x:A.P x ≝ λA,P,a,p.
\ 5a href="cic:/matita/basics/types/Sig.con(0,1,2)"
\ 6dp
\ 5/a
\ 6 … a p.
6 definition eject : ∀A.∀P: A → Prop.(
\ 5a title="Sigma" href="cic:/fakeuri.def(1)"
\ 6Σ
\ 5/a
\ 6x:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w].
8 (* coercion inject nocomposites: ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?.
9 coercion eject nocomposites: ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?. *)
11 (*axiom VOID: Type[0].
12 axiom assert_false: VOID.
13 definition bigbang: ∀A:Type[0].False → VOID → A.
17 coercion bigbang nocomposites: ∀A:Type[0].False → ∀v:VOID.A ≝ bigbang on _v:VOID to ?.*)
19 lemma sig2: ∀A.∀P:A → Prop. ∀p:
\ 5a title="Sigma" href="cic:/fakeuri.def(1)"
\ 6Σ
\ 5/a
\ 6x:A.P x. P (
\ 5a href="cic:/matita/Cerco/ASM/JMCoercions/eject.def(1)"
\ 6eject
\ 5/a
\ 6 … p).
20 #A #P #p cases p #w #q @q