Double-negation translation

Intuitionistic logic

%sort iprop %.
%name iprop %.
%term itop iprop %.
%term iand %pi iprop %-> iprop %-> iprop %.
%term ibot iprop %.
%term ior %pi iprop %-> iprop %-> iprop %.
%term iimp %pi iprop %-> iprop %-> iprop %.
%block ipb {X iprop}%.
%worlds (ipb) (iprop) %.
%sort itrue {_ iprop} %.
%term imt itrue itop %.
%term ipair %pi (itrue A) %-> (itrue B) %-> (itrue (iand A B)) %.
%term ifst %pi (itrue (iand A B)) %-> (itrue A) %.
%term isnd %pi (itrue (iand A B)) %-> (itrue B) %.
%term iabort %pi (itrue ibot) %-> (itrue C) %.
%term iinl %pi (itrue A) %-> (itrue (ior A B)) %.
%term iinr %pi (itrue B) %-> (itrue (ior A B)) %.
%term icase
  %pi (itrue (ior A B))
  %-> (%pi (itrue A) %-> (itrue C))
  %-> (%pi (itrue B) %-> (itrue C))
  %-> (itrue C) %.
%term ilam %pi (%pi (itrue A) %-> (itrue B)) %-> (itrue (iimp A B)) %.
%term iapp %pi (itrue (iimp A B)) %-> (itrue A) %-> (itrue B) %.
%define inot (%pi iprop %-> iprop) [A] iimp A ibot %.
%define idn (%pi iprop %-> iprop) [A] inot (inot A) %.
%define dni (%pi (itrue A) %-> (itrue (idn A))) [x itrue A] ilam ([y itrue (inot A)] iapp y x) %.
%define tne (%pi (itrue (idn (inot A))) %-> (itrue (inot A))) [x3 itrue (inot (inot (inot A)))] ilam ([x itrue A] iapp x3 (ilam ([y itrue (inot A)] iapp y x))) %.
%define distdnand (%pi (itrue (idn (iand A B))) %-> (itrue (iand (idn A) (idn B)))) [f] ipair (ilam ([x itrue (inot A)] iapp f (ilam ([p] iapp x (ifst p))))) (ilam ([x itrue (inot B)] iapp f (ilam ([p] iapp x (isnd p))))) %.
%define dnebot (%pi (itrue (idn ibot)) %-> (itrue ibot)) [x] iapp x (ilam ([x] x)) %.
%inline dnetop (%pi (itrue (idn itop)) %-> (itrue itop)) [x] imt %.
%define distdnimp (%pi (itrue (idn (iimp A B))) %-> (itrue (iimp (idn A) (idn B)))) [f] ilam ([x itrue (idn A)] ilam ([y itrue (inot B)] iapp f (ilam ([g itrue (iimp A B)] iapp x (ilam ([z itrue A] iapp y (iapp g z))))))) %.
%block itb [A iprop] {D itrue A}%.
%worlds (ipb itb) (itrue _) %.

Classical logic

%sort prop %.
%name prop %.
%term top prop %.
%term and %pi prop %-> prop %-> prop %.
%term bot prop %.
%term or %pi prop %-> prop %-> prop %.
%term imp %pi prop %-> prop %-> prop %.
%term nbot prop %.
%term not %pi prop %-> prop %.
%block pb {X prop}%.
%worlds (pb) (prop) %.
%sort conc %.
%term true %pi prop %-> conc %.
%prec %prefix 2 true %.
%term false %pi prop %-> conc %.
%prec %prefix 2 false %.
%term contra conc %.
%sort >> {_ conc} %.
%prec %prefix 3 >> %.
%term mt >> true top %.
%term pair %pi (>> true A) %-> (>> true B) %-> (>> true (and A B)) %.
%term fst %pi (>> true (and A B)) %-> (>> true A) %.
%term snd %pi (>> true (and A B)) %-> (>> true B) %.
%term abort %pi (>> true bot) %-> (>> J) %.
%term inl %pi (>> true A) %-> (>> true (or A B)) %.
%term inr %pi (>> true B) %-> (>> true (or A B)) %.
%term case
  %pi (>> true (or A B))
  %-> (%pi (>> true A) %-> (>> J))
  %-> (%pi (>> true B) %-> (>> J))
  %-> (>> J) %.
%term lam %pi (%pi (>> true A) %-> (>> true B)) %-> (>> true (imp A B)) %.
%term app %pi (>> true (imp A B)) %-> (>> true A) %-> (>> true B) %.
%% anything follows from contradiction
%term cabort %pi (>> contra) %-> (>> J) %.
%% negative bottom
%term nboti %pi (>> contra) %-> (>> true nbot) %.
%term nbote %pi (>> true nbot) %-> (>> contra) %.
%% falsehood
%term cont %pi (%pi (>> true A) %-> (>> contra)) %-> (>> false A) %.
%term throw %pi (>> false A) %-> (>> true A) %-> (>> contra) %.
%% negation
%term noti %pi (>> false A) %-> (>> true (not A)) %.
%term notcase %pi (>> true (not A)) %-> (%pi (>> false A) %-> (>> J)) %-> (>> J) %.
%% because not should be positive
%% letcc
%term letcc %pi (%pi (>> false A) %-> (>> contra)) %-> (>> true A) %.
%block tb [A prop] {D >> true A}%.
%block fb [A prop] {D >> false A}%.
%worlds (pb tb fb) (>> _) %.
%define iff (%pi prop %-> prop %-> prop) [A] [B] and (imp A B) (imp B A) %.
%define iffi (
  %pi (%pi (>> true A) %-> (>> true B))
  %-> (%pi (>> true B) %-> (>> true A))
  %-> (>> true (iff A B))) [E1] [E2] pair (lam E1) (lam E2) %.
%define iffel (%pi (>> true (iff A B)) %-> (>> true A) %-> (>> true B)) [E1] [E2] app (fst E1) E2 %.
%define iffer (%pi (>> true (iff A B)) %-> (>> true B) %-> (>> true A)) [E1] [E2] app (snd E1) E2 %.
%define cdni (%pi (>> true A) %-> (>> true (not (not A)))) [x] noti (cont ([nx] notcase nx ([f] throw f x))) %.
%define cdne (%pi (>> true (not (not A))) %-> (>> true A)) [x] notcase x ([f] letcc ([u] throw f (noti u))) %.
%define notimpbot (%pi (>> true (iff A B)) %-> (>> true (iff (not A) (imp B bot)))) [c] iffi ([x] notcase x ([f] lam ([y] cabort (throw f (iffer c y))))) ([x] noti (cont ([y] abort (app x (iffel c y))))) %.
%define notimpbot2 (>> true (iff (not (not A)) (imp (imp A bot) bot))) notimpbot (notimpbot (iffi ([x] x) ([x] x))) %.

Double-negation translation

This is essentially the Godel-Gentzen Negtive Translation. It differs only by De Morgan laws that are provable intuitionistically.

%sort * {_ prop} {_ iprop} %.
%mode * %in %out %.
%term */top * top itop %.
%term */and %pi (* (and A B) (iand A' B')) %<- (* A A') %<- (* B B') %.
%term */bot * bot ibot %.
%term */or %pi (* (or A B) (inot (inot (ior A' B')))) %<- (* A A') %<- (* B B') %.
%term */imp %pi (* (imp A B) (iimp A' B')) %<- (* A A') %<- (* B B') %.
%term */nbot * nbot ibot %.
%term */not %pi (* (not A) (inot A')) %<- (* A A') %.
%block *b {X prop} {X' iprop} {_ * X (inot (inot X'))}%.
%worlds (*b) (* _ _) %.
%total A (* A _) %.
%unique * %in %out %.
%sort *tot {A} {_ * A A'} %.
%mode *tot %in %out %.
%block *totb {X prop} {X' iprop} {D* * X (idn X')} {_ *tot X D*}%.
%worlds (*totb) (*tot _ _) %.
%total {} (*tot _ _) %.
%% verified by %total above
%sort id-iprop {_ iprop} {_ iprop} %.
%term id-iprop/refl id-iprop A A %.
%sort id-iprop-not-cong {_ id-iprop A' B'} {_ id-iprop (inot A') (inot B')} %.
%mode id-iprop-not-cong %in %out %.
%term _ id-iprop-not-cong _ id-iprop/refl %.
%worlds (ipb) (id-iprop-not-cong _ _) %.
%total {} (id-iprop-not-cong _ _) %.
%sort *unique {_ * A A'} {_ * A B'} {_ id-iprop A' B'} %.
%mode *unique %in %in %out %.
%worlds (*b) (*unique _ _ _) %.
%total {} (*unique _ _ _) %.
%% verified by %unique above
%sort itrue-respects-id {_ itrue A} {_ id-iprop A' A} {_ itrue A'} %.
%mode itrue-respects-id %in %in %out %.
%term _ itrue-respects-id D _ D %.
%worlds (itb ipb) (itrue-respects-id _ _ _) %.
%total {} (itrue-respects-id _ _ _) %.

Double-negation elimination for the target of the translation

%sort dne {_ * A A'} {_ %pi (itrue (inot (inot A'))) %-> (itrue A')} %.
%mode dne %in %out %.
%term _
  %pi (dne (*/and D*2 D*1) ([x] ipair (E1 (ifst (distdnand x))) (E2 (isnd (distdnand x)))))
  %<- (dne D*1 E1)
  %<- (dne D*2 E2) %.
%term _ dne */top ([x] imt) %.
%term _ dne (*/or _ _) ([x] tne x) %.
%term _ dne */bot ([x] dnebot x) %.
%term _ dne */nbot ([x] dnebot x) %.
%term _
  %pi (dne (*/imp D*2 D*1) ([x] ilam ([y] E2 (iapp (distdnimp x) (dni y)))))
  %<- (dne D*2 E2) %.
%term _ %pi (dne (*/not D*) tne) %<- (dne D* E) %.
%block dneb {X prop} {X' iprop} {dx * X (idn X')} {_ dne dx tne}%.
%worlds (dneb itb) (dne _ _) %.
%total D (dne D _) %.

Soundness

%sort sound/true {_ >> true A} {_ * A A'} {_ itrue A'} %.
%mode sound/true %in %in %out %.
%sort sound/false {_ >> false A} {_ * A A'} {_ itrue (iimp A' ibot)} %.
%mode sound/false %in %in %out %.
%sort sound/contra {_ >> contra} {_ itrue ibot} %.
%mode sound/contra %in %out %.
%% true
%term _ sound/true mt */top imt %.
%term _
  %pi (sound/true (pair E1 E2) (*/and D*2 D*1) (ipair E1' E2'))
  %<- (sound/true E1 D*1 E1')
  %<- (sound/true E2 D*2 E2') %.
%term _
  %pi (sound/true (fst (%the (>> true (and A1 A2)) E)) D*1 (ifst E'))
  %<- (*tot A2 D*2)
  %<- (sound/true E (*/and D*2 D*1) E') %.
%term _
  %pi (sound/true (snd (%the (>> true (and A1 A2)) E)) D*2 (isnd E'))
  %<- (*tot A1 D*1)
  %<- (sound/true E (*/and D*2 D*1) E') %.
%term _
  %pi (sound/true (%the (>> true C) (abort E)) D* (iabort E'))
  %<- (sound/true E */bot E') %.
%term _
  %pi (sound/true (%the (>> true (or A1 A2)) (inl E)) (*/or D*2 D*1) (dni (iinl E')))
  %<- (sound/true E D*1 E') %.
%term _
  %pi (sound/true (%the (>> true (or A1 A2)) (inr E)) (*/or D*2 D*1) (dni (iinr E')))
  %<- (sound/true E D*2 E') %.
%term _
  %pi (sound/true (case (%the (>> true (or A B)) E) E1 E2) D* (Edne (ilam ([f itrue (inot C')] iapp E' (ilam ([x itrue (ior A' B')] icase x ([x1] iapp f (E1' x1)) ([x2] iapp f (E2' x2))))))))
  %<- (*tot A D*A)
  %<- (*tot B D*B)
  %<- (sound/true E (*/or D*B D*A) E')
  %<- ({x >> true A} {x' itrue A'} {_ {A''} {D* * A A''} {Did} {E''}
  %pi (sound/true x D* E'')
  %<- (*unique D* D*A Did)
  %<- (itrue-respects-id x' Did E'')} sound/true (E1 x) D* (E1' x'))
  %<- ({x >> true B} {x' itrue B'} {_ {A''} {D* * B A''} {Did} {E''}
  %pi (sound/true x D* E'')
  %<- (*unique D* D*B Did)
  %<- (itrue-respects-id x' Did E'')} sound/true (E2 x) D* (E2' x'))
  %<- (dne D* Edne) %.
%term _
  %pi (sound/true (%the (>> true (imp A B)) (lam E)) (*/imp D* D*A) (ilam E'))
  %<- ({x >> true A} {x' itrue A'} {_ {A''} {D* * A A''} {Did} {E''}
  %pi (sound/true x D* E'')
  %<- (*unique D* D*A Did)
  %<- (itrue-respects-id x' Did E'')} sound/true (E x) D* (E' x')) %.
%term _
  %pi (sound/true (app E1 E2) D*B (iapp E1' E2'))
  %<- (*tot A D*A)
  %<- (sound/true E1 (*/imp D*B D*A) E1')
  %<- (sound/true E2 D*A E2') %.
%term _
  %pi (sound/true (%the (>> true C) (cabort E)) D* (iabort E'))
  %<- (sound/contra E E') %.
%term _
  %pi (sound/true (%the (>> true nbot) (nboti E)) */nbot (iabort E'))
  %<- (sound/contra E E') %.
%term _
  %pi (sound/true (%the (>> true (not A)) (noti E)) (*/not D*) E')
  %<- (sound/false E D* E') %.
%term _
  %pi (sound/true (notcase E1 E2) D*C (E2' E1'))
  %<- (*tot A D*A)
  %<- (sound/true E1 (*/not (%the (* A A') D*A)) E1')
  %<- ({x >> false A} {x' itrue (inot A')} {_ {A'' iprop} {D* * A A''} {Did id-iprop A'' A'} {Did' id-iprop (inot A'') (inot A')} {E'' itrue (inot A'')}
  %pi (sound/false x D* E'')
  %<- (*unique D* D*A Did)
  %<- (id-iprop-not-cong Did Did')
  %<- (itrue-respects-id x' Did' E'')} sound/true (E2 x) D*C (E2' x')) %.
%term _
  %pi (sound/true (%the (>> true A) (letcc E)) D*A (Edne (ilam E')))
  %<- ({x >> false A} {x' itrue (inot A')} {_ {A'' iprop} {D* * A A''} {Did id-iprop A'' A'} {Did' id-iprop (inot A'') (inot A')} {E'' itrue (inot A'')}
  %pi (sound/false x D* E'')
  %<- (*unique D* D*A Did)
  %<- (id-iprop-not-cong Did Did')
  %<- (itrue-respects-id x' Did' E'')} sound/contra (E x) (E' x'))
  %<- (dne D*A Edne) %.
%% false
%term _
  %pi (sound/false (%the (>> false A) (cont E)) D*A (ilam E'))
  %<- ({x >> true A} {x' itrue A'} {_ {A''} {D* * A A''} {Did} {E''}
  %pi (sound/true x D* E'')
  %<- (*unique D* D*A Did)
  %<- (itrue-respects-id x' Did E'')} sound/contra (E x) (E' x')) %.
%term _ %pi (sound/false (cabort E) D* (iabort E')) %<- (sound/contra E E') %.
%term _
  %pi (sound/false (case (%the (>> true (or A B)) E) E1 E2) D* (ilam ([c itrue C] iapp E' (ilam ([x] icase x ([x1] iapp (E1' x1) c) ([x2] iapp (E2' x2) c))))))
  %<- (*tot _ D*A)
  %<- (*tot _ D*B)
  %<- (sound/true E (*/or D*B D*A) E')
  %<- ({x >> true A} {x' itrue A'} {_ {A''} {D* * A A''} {Did} {E''}
  %pi (sound/true x D* E'')
  %<- (*unique D* D*A Did)
  %<- (itrue-respects-id x' Did E'')} sound/false (E1 x) D* (E1' x'))
  %<- ({x >> true B} {x' itrue B'} {_ {A''} {D* * B A''} {Did} {E''}
  %pi (sound/true x D* E'')
  %<- (*unique D* D*B Did)
  %<- (itrue-respects-id x' Did E'')} sound/false (E2 x) D* (E2' x')) %.
%term _
  %pi (sound/false (%the (>> false C) (abort E)) D* (iabort E'))
  %<- (sound/true E */bot E') %.
%term _
  %pi (sound/false (notcase E1 E2) D*C (E2' E1'))
  %<- (*tot _ D*A)
  %<- (sound/true E1 (*/not (%the (* A A') D*A)) E1')
  %<- ({x >> false A} {x' itrue (inot A')} {_ {A'' iprop} {D* * A A''} {Did id-iprop A'' A'} {Did' id-iprop (inot A'') (inot A')} {E'' itrue (inot A'')}
  %pi (sound/false x D* E'')
  %<- (*unique D* D*A Did)
  %<- (id-iprop-not-cong Did Did')
  %<- (itrue-respects-id x' Did' E'')} sound/false (E2 x) D*C (E2' x')) %.
%% contra
%term _
  %pi (sound/contra (throw E1 E2) (iapp E1' E2'))
  %<- (*tot _ D*)
  %<- (sound/true E2 D* E2')
  %<- (sound/false E1 D* E1') %.
%term _ %pi (sound/contra (nbote E) E') %<- (sound/true E */nbot E') %.
%term _
  %pi (sound/contra (case E E1 E2) (iapp E' (ilam ([x] icase x E1' E2'))))
  %<- (*tot _ D*A)
  %<- (*tot _ D*B)
  %<- (sound/true E (*/or D*B D*A) E')
  %<- ({x >> true A} {x' itrue A'} {_ {A''} {D* * A A''} {Did} {E''}
  %pi (sound/true x D* E'')
  %<- (*unique D* D*A Did)
  %<- (itrue-respects-id x' Did E'')} sound/contra (E1 x) (E1' x'))
  %<- ({x >> true B} {x' itrue B'} {_ {A''} {D* * B A''} {Did} {E''}
  %pi (sound/true x D* E'')
  %<- (*unique D* D*B Did)
  %<- (itrue-respects-id x' Did E'')} sound/contra (E2 x) (E2' x')) %.
%term _ %pi (sound/contra (abort E) (iabort E')) %<- (sound/true E */bot E') %.
%term _ %pi (sound/contra (cabort E) E') %<- (sound/contra E E') %.
%term _
  %pi (sound/contra (notcase E1 E2) (E2' E1'))
  %<- (*tot _ D*A)
  %<- (sound/true E1 (*/not (%the (* A A') D*A)) E1')
  %<- ({x >> false A} {x' itrue (inot A')} {_ {A'' iprop} {D* * A A''} {Did id-iprop A'' A'} {Did' id-iprop (inot A'') (inot A')} {E'' itrue (inot A'')}
  %pi (sound/false x D* E'')
  %<- (*unique D* D*A Did)
  %<- (id-iprop-not-cong Did Did')
  %<- (itrue-respects-id x' Did' E'')} sound/contra (E2 x) (E2' x')) %.
%% uses a fancy variable case:
%block soundtb [A prop] [A' iprop] [Dx * A A'] {x >> true A} {x' itrue A'} {_ {A''} {D* * A A''} {Did} {E''}
  %pi (sound/true x D* E'')
  %<- (*unique D* Dx Did)
  %<- (itrue-respects-id x' Did E'')}%.
%block soundfb [A prop] [A' iprop] [Dx * A A'] {x >> false A} {x' itrue (inot A')} {_ {A'' iprop} {D* * A A''} {Did id-iprop A'' A'} {Did' id-iprop (inot A'') (inot A')} {E'' itrue (inot A'')}
  %pi (sound/false x D* E'')
  %<- (*unique D* Dx Did)
  %<- (id-iprop-not-cong Did Did')
  %<- (itrue-respects-id x' Did' E'')}%.
%block soundpb {X prop} {X' iprop} {dx * X (idn X')} {_ dne dx tne} {_ *tot X dx}%.
%worlds (soundpb soundtb soundfb) (sound/true _ _ _) (sound/true _ _ _) (sound/false _ _ _) (sound/false _ _ _) (sound/contra _ _) %.
%total (D1 D4 D2 D5 D3) (sound/true D4 _ _) (sound/true D1 _ _) (sound/false D5 _ _) (sound/false D2 _ _) (sound/contra D3 _) %.

Completeness

Inclusion

Include intuitionistic props into classical. We need to define another translation because * is not total with the reverse mode (it doesn’t translate atoms).

%sort *i {_ prop} {_ iprop} %.
%mode *i %out %in %.
%term *i/top *i top itop %.
%term *i/and %pi (*i (and A B) (iand A' B')) %<- (*i A A') %<- (*i B B') %.
%term *i/bot *i bot ibot %.
%term *i/or %pi (*i (or A B) (ior A' B')) %<- (*i A A') %<- (*i B B') %.
%term *i/imp %pi (*i (imp A B) (iimp A' B')) %<- (*i A A') %<- (*i B B') %.
%block *ib {X prop} {X' iprop} {_ *i X X'}%.
%worlds (*ib) (*i _ _) %.
%total A (*i _ A) %.
%unique *i %out %in %.
%sort *itot {A'} {_ *i A A'} %.
%mode *itot %in %out %.
%block *itotb {X prop} {X' iprop} {D*i *i X X'} {_ *itot X' D*i}%.
%worlds (*itotb fb pb) (*itot _ _) %.
%total {} (*itot _ _) %.
%% verified by %total above
%sort id-prop {_ prop} {_ prop} %.
%term id-prop/refl id-prop A A %.
%sort *iunique {_ *i A A'} {_ *i B A'} {_ id-prop A B} %.
%mode *iunique %in %in %out %.
%worlds (*ib fb pb) (*iunique _ _ _) %.
%total {} (*iunique _ _ _) %.
%% verified by %unique above
%sort true-respects-id {_ >> true A} {_ id-prop A' A} {_ >> true A'} %.
%mode true-respects-id %in %in %out %.
%term _ true-respects-id D _ D %.
%worlds (tb fb pb) (true-respects-id _ _ _) %.
%total {} (true-respects-id _ _ _) %.

Intuitionistic truth implies classical truth

The arguments are in a funny order because I copied from soundness. =)

%sort incl {_ >> true A} {_ *i A A'} {_ itrue A'} %.
%mode incl %out %in %in %.
%term _ incl mt *i/top imt %.
%term _
  %pi (incl (pair E1 E2) (*i/and D*2 D*1) (ipair E1' E2'))
  %<- (incl E1 D*1 E1')
  %<- (incl E2 D*2 E2') %.
%term _
  %pi (incl (fst E) D*1 (ifst (%the (itrue (iand A1 A2)) E')))
  %<- (*itot A2 D*2)
  %<- (incl E (*i/and D*2 D*1) E') %.
%term _
  %pi (incl (snd (%the (>> true (and A1 A2)) E)) D*2 (isnd E'))
  %<- (*itot _ D*1)
  %<- (incl E (*i/and D*2 D*1) E') %.
%term _ %pi (incl (%the (>> true C) (abort E)) D* (iabort E')) %<- (incl E *i/bot E') %.
%term _
  %pi (incl (%the (>> true (or A1 A2)) (inl E)) (*i/or D*2 D*1) (iinl E'))
  %<- (incl E D*1 E') %.
%term _
  %pi (incl (%the (>> true (or A1 A2)) (inr E)) (*i/or D*2 D*1) (iinr E'))
  %<- (incl E D*2 E') %.
%term _
  %pi (incl (case (%the (>> true (or A B)) E) E1 E2) D* (icase E' E1' E2'))
  %<- (*itot _ D*A)
  %<- (*itot _ D*B)
  %<- (incl E (*i/or D*B D*A) E')
  %<- ({x >> true A} {x' itrue A'} {_ {A-2} {D*' *i A-2 A'} {Did id-prop A-2 A} {E >> true A-2} %pi (incl E D*' x') %<- (*iunique D*' D*A Did) %<- (true-respects-id x Did E)} incl (E1 x) D* (E1' x'))
  %<- ({x >> true B} {x' itrue B'} {_ {B-2} {D*' *i B-2 B'} {Did id-prop B-2 B} {E >> true B-2} %pi (incl E D*' x') %<- (*iunique D*' D*B Did) %<- (true-respects-id x Did E)} incl (E2 x) D* (E2' x')) %.
%term _
  %pi (incl (%the (>> true (imp A B)) (lam E)) (*i/imp D* D*A) (ilam E'))
  %<- ({x >> true A} {x' itrue A'} {_ {A-2} {D*' *i A-2 A'} {Did id-prop A-2 A} {E >> true A-2} %pi (incl E D*' x') %<- (*iunique D*' D*A Did) %<- (true-respects-id x Did E)} incl (E x) D* (E' x')) %.
%term _
  %pi (incl (app E1 E2) D*B (iapp E1' E2'))
  %<- (*itot A D*A)
  %<- (incl E1 (*i/imp D*B D*A) E1')
  %<- (incl E2 D*A E2') %.
%block inclb [A] [A'] [D* *i A A'] {x >> true A} {x' itrue A'} {_ {A-2} {D*' *i A-2 A'} {Did id-prop A-2 A} {E >> true A-2} %pi (incl E D*' x') %<- (*iunique D*' D* Did) %<- (true-respects-id x Did E)}%.
%worlds (inclb fb *itotb) (incl _ _ _) %.
%total D (incl _ _ D) %.

Round-tripping the two translations is classically equivalent

%sort equiv {_ * A A'} {_ *i A'' A'} {_ >> true (iff A A'')} %.
%mode equiv %in %in %out %.
%term _ equiv D D' (iffi ([x] x) ([x] x)) %.
%term _
  %pi (equiv (*/and D*2 D*1) (*i/and D*2' D*1') (iffi ([x] pair (iffel E1 (fst x)) (iffel E2 (snd x))) ([x] pair (iffer E1 (fst x)) (iffer E2 (snd x)))))
  %<- (equiv D*1 D*1' E1)
  %<- (equiv D*2 D*2' E2) %.
%term _
  %pi (equiv (*/or D*2 D*1) (*i/imp *i/bot (*i/imp *i/bot (*i/or D*2' D*1'))) (iffi ([x] iffel notimpbot2 (cdni (case x ([x1] inl (iffel E1 x1)) ([x2] inr (iffel E2 x2))))) ([x] case (cdne (iffer notimpbot2 x)) ([x1] inl (iffer E1 x1)) ([x2] inr (iffer E2 x2)))))
  %<- (equiv D*1 D*1' E1)
  %<- (equiv D*2 D*2' E2) %.
%term _
  %pi (equiv (*/imp D*2 D*1) (*i/imp D*2' D*1') (iffi ([f >> true (imp A1 A2)] lam ([x >> true B1] iffel E2 (app f (iffer E1 x)))) ([f >> true (imp B1 B2)] lam ([x >> true A1] iffer E2 (app f (iffel E1 x))))))
  %<- (equiv D*1 D*1' (%the (>> true (iff A1 B1)) E1))
  %<- (equiv D*2 D*2' (%the (>> true (iff A2 B2)) E2)) %.
%term _ equiv */nbot *i/bot (iffi ([x] cabort (nbote x)) ([x] abort x)) %.
%term _
  %pi (equiv (*/not D*) (*i/imp *i/bot D*') (iffi ([x] lam ([y] cabort (notcase x ([u] throw u (iffer E y))))) ([x] noti (cont ([y] abort (app x (iffel E y)))))))
  %<- (equiv D* D*' E) %.
%block equivb {X prop} {X' iprop} {d*i *i X X'} {d* * X (inot (inot X'))} {_ equiv d* (*i/imp *i/bot (*i/imp *i/bot d*i)) (iffi ([x >> true X] iffel notimpbot2 (cdni x)) ([x >> true (imp (imp X bot) bot)] cdne (iffer notimpbot2 x)))}%.
%worlds (equivb tb fb) (equiv _ _ _) %.
%total D (equiv D _ _) %.

If A* is intuitionistically true, then A is classically true

%sort comp {_ itrue A'} {_ * A A'} {_ >> true A} %.
%mode comp %in %in %out %.
%term _
  %pi (comp (%the (itrue A') E') D* (iffer Eiff E))
  %<- (*itot A' D*i)
  %<- (incl E D*i E')
  %<- (equiv D* D*i Eiff) %.
%block comp-pb {X prop} {X' iprop} {d*i *i X X'} {d* * X (inot (inot X'))} {_ equiv d* (*i/imp *i/bot (*i/imp *i/bot d*i)) (iffi ([x >> true X] iffel notimpbot2 (cdni x)) ([x >> true (imp (imp X bot) bot)] cdne (iffer notimpbot2 x)))} {_ *itot X' d*i}%.
%worlds (comp-pb inclb fb) (comp _ _ _) %.
%total E1 (comp E1 _ _) %.
%sort comp/false {_ itrue (iimp A' ibot)} {_ * A A'} {_ >> false A} %.
%mode comp/false %in %in %out %.
%term _
  %pi (comp/false E D* (cont ([x] notcase E' ([u] throw u x))))
  %<- (comp E (*/not D*) E') %.
%worlds (comp-pb inclb fb) (comp/false _ _ _) %.
%total {} (comp/false _ _ _) %.
%sort comp/contra {_ itrue ibot} {_ >> contra} %.
%mode comp/contra %in %out %.
%term _ %pi (comp/contra E (nbote E')) %<- (comp E */nbot E') %.
%worlds (comp-pb inclb fb) (comp/contra _ _) %.
%total {} (comp/contra _ _) %.