lemma gral: ∀A.∀x,y:A.
mk_Sigma A x = mk_Sigma A y → x=y.
#A #x #y #E lapply (tech1 ?? E)
- generalize {⊢ (??(???%?)? → ?)} #E1
- normalize {E1}; >(K ?? E1) normalize
+ generalize in ⊢ (??(???%?)? → ?); #E1
+ normalize in E1; >(K ?? E1) normalize
#H @H
qed.
lemma jm_to_eq_sigma:
∀A,x,y. jmeq A x A y → mk_Sigma A x = mk_Sigma A y.
- #A #x #y #E cases E {⊢ (???%)} %
+ #A #x #y #E cases E in ⊢ (???%); %
qed.
definition curry:
lemma G : ∀A.∀x:A.∀P:∀y:A.mk_Sigma A x = mk_Sigma A y →Type[0].
P x (refl ? (mk_Sigma A x)) → ∀y.∀h:mk_Sigma A x = mk_Sigma A y.
P y h.
- #A #x #P #H #y #E lapply (gral ??? E) #G generalize {match E}
+ #A #x #P #H #y #E lapply (gral ??? E) #G generalize in match E;
@(match G
return λy.λ_. ∀e:mk_Sigma A x = mk_Sigma A y. P y e
with
#A #a #P #H #b #E letin F ≝ (jm_to_eq_sigma ??? E)
lapply (G ?? (curry ?? P) ?? F)
[ normalize //
- | #H whd {H} @(H : PP ? (P b) ?) ]
+ | #H whd in H; @(H : PP ? (P b) ?) ]
qed.
lemma jmeq_elim : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0].