interpretation "new I" 'I a = (nI ? a).
ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
interpretation "new I" 'I a = (nI ? a).
ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
nlemma elim_eq_TYPE : ∀A,B:setoid.∀P:CProp[1]. A=B → ((B ⇒ A) → P) → P.
#A; #B; #P; *; #f; *; #g; #_; #IH; napply IH; napply g;
nqed.
nlemma elim_eq_TYPE : ∀A,B:setoid.∀P:CProp[1]. A=B → ((B ⇒ A) → P) → P.
#A; #B; #P; *; #f; *; #g; #_; #IH; napply IH; napply g;
nqed.
ndefinition image_is_ext : ∀A:nAx.∀a:A.∀i:𝐈 a.𝛀^A.
#A; #a; #i; @ (image … i); #x; #y; #H; @;
##[ *; #d; #Ex; @ d; napply (.= H^-1); nassumption;
ndefinition image_is_ext : ∀A:nAx.∀a:A.∀i:𝐈 a.𝛀^A.
#A; #a; #i; @ (image … i); #x; #y; #H; @;
##[ *; #d; #Ex; @ d; napply (.= H^-1); nassumption;