=================================================
================== LANG3a =======================
=================================================

=================================================
================== SYNTAX =======================
=================================================

k = type | k1 -> k2
t = A | !t | all A:k.t | t1 -o t2 | \A:k.t | t t
e = x | \A:k.e | e t | \r(x):t.e | e1 e2
d = . | d,A:k
g = . | g,r(x:t)
r = . | !

abbreviation: exists A:k.t = all B:type. (all A:k. t -o B) -o B
abbreviation: t1 * t2 = all B:type. (t1 -o t2 -o B) -o B
abbreviation: t1 x t2 = !(t1 * t2)
abbreviation: t1 -> t2 = !(t1 -o t2)
abbreviation: t1 <o> t2 = (t1 -> t2) * (t2 -> t1)
abbreviation: t1 <-> t2 = (t1 -> t2) x (t2 -> t1)
abbreviation: t1 =o> t2 = t1 -o (t2 * (t2 -o t1))
abbreviation: t1 =>> t2 = t1 -> (t2 * (t2 -o t1))
abbreviation: <> = all A:type. A->A
abbreviation: () = !<>
abbreviation: true = exists A:type.A

=================================================
================= SEMANTICS =====================
=================================================

...,A:k,... |- A:k

d |- t:type
------------
d |- !t:type

d,A:k |- t:type
-------------------
d |- all A:k.t:type

d |- t1:type
d |- t2:type
------------------
d |- t1 -o t2:type

d,A:k1 |- t:k2
-------------------
d |- \A:k1.t:k1->k2

d |- t1:ka->kb
d |- t2:ka
--------------
d |- t1 t2:kb

=================================================

d |- t
----------
d |- t = t

d |- t2 = t1
------------
d |- t1 = t2

d |- t1 = t2
d |- t2 = t3
------------
d |- t1 = t3

d |- (\A:k.t1) t2 = [A<-t2](t1)

=================================================

d |- t = t'
-------------
d |- !t = !t'

d |- t = t'
---------------------------
d |- all A:k.t = all A:k.t'

d |- t1 = t1'
d |- t2 = t2'
--------------------------
d |- t1 -o t2 = t1' -o t2'

d |- t = t'
---------------------
d |- \A:k.t = \A:k.t'

d |- t1 = t1'
d |- t2 = t2'
--------------------
d |- t1 t2 = t1' t2'

=================================================

d;!g,r(x:t) |- x: r(t)

d,A:k;r(g) |- e: t
---------------------------------
d;r(g) |- r(\A:k.e): r(all A:k.t)

d;g |- e: r(all A:k.tb)
d |- ta:k
-----------------------
d;g |- e ta: [A<-ta]tb

d;r'(g),r(x:ta) |- e:tb
-------------------------------------------
d;r'(g) |- r'(\r(x):r(ta).e):r'(r(ta)-o tb)

d;g1 |- e1:r(ta -o tb)
d;g2 |- e2:ta
----------------------
d;g1,g2 |- (e1 e2):tb

d;g |- e: t'
d |- t' = t
----------------
d;g |- e: t

=================================================
========== LANG2->LANG3b TRANSLATION ============
=================================================

K(cap~) = type
K(cap+) = type->type
K(type) = type
K(res) = type

U(A) = A
U({}) = ()
U({A p}) = X A
U(u1+u2) = U(u1) * U(u2)

A(a) = \P:type. exists Q:type. (P =>> Q) x !(A[a] Q)
A[A] = A
A[{}] = \P:type. <>
A[{A p}] = \P:type. (P =o> X A)
A[a1+a2] = \P:type. !(A(a1) P) * !(A(a2) P)

C(u#a) = \P:type. U(u) * !(A(a) P)

S(u1#a1<=a2) = all Q:type.!(A(a1) Q) -> !(A(a2) (Q*U(u1)))

T(A) = A
T(<t1,t2>) = !T(t1) * !T(t2)
T(all A:k.t) = all A:K(k).!T(t)
T(all A:cap+ where c1<=a1,...,cn<=an.t) = all A:type->type. !S(c1<=a1) -> ... -> !S(cn<=an) -> !T(t)
T((u#a,t)->0) = all P:type. P -> U(u) -o !(A(a) P) -o !T(t) -o true
T(A handle) = <>

D(.) = .
D(A:k,d) = A:K(k), D(d)
D(A:cap+ where u1#A<=a1,...,un#A<=an,d) = A:type->type, D(d)

G(.;.) = .
G(.;x:t,g) = !(x:T(t)),G(.;g)
G(A:k,d;g) = G(d;g)
G(A:cap+ where c1<=a1,...,cn<=an,d;g) = !(xA1:S(c1<=a1)),...,!(xAn:S(cn<=an)),G(d;g)

V(x) = x
V(v[t:type]) = V(v) T(t)
V(v[A:res]) = V(v) A
V(v[u:cap~]) = V(v) U(u)
V(v[a:cap+]) = V(v) A[a]

d;g |- v: all A:cap+ where u1#A<=a1,...,un#A<=an.t ~~> e
d;g |- u1#a <= a1 ~~> e1
...
d;g |- un#a <= an ~~> en
d;g |- a:cap+
-----------------------------------------------
d;g |- v[a:cap+]: [A<-a]t ~~> e A[a] e1 ... en

d;g |- v: t' ~~> e
d |- t' = t:type ~~> e'
-----------------------
d;g |- v: t ~~> e'.1 e

H(\A:k.h) = !\A:K(k).H(h)
H(\A:cap+ where c1<=a1,...,cn<=an.h) = !\A:type->type.!\!xA1:!S(c1<=a1)...!\!xAn:!S(cn<=an).H(h)
H(\(u#a,x:t).e) = !\P:type.!\zP:P.\zU:U(u).\!zA:!(A(a) P).\!x:!T(t).E(e)
H(<v1,v2>) = (V(v1),V(v2))

d;g |- h: t' ~~> e
d |- t' = t:type ~~> e'
-----------------------
d;g |- h: t ~~> e'.1 e

E(let x=v in e) = let !x=V(v) in E(e)
E(let x=h in e) = let !x=H(h) in E(e)
E(let x=v.n in e) = let !x=V(v).n in E(e)
E(let new A,x in e) =
  unpack A,xA = new () in
  let zU = <zU,xA> in
  let !x = () in
  E(e)

d;g |- v: A handle
d |- u = u'+{A~}:cap~ ~~> eu
d;g;u'#a |- e ~~> e'
------------------------------
d;g;u#a |- let free v in e ~~>
  let <zU,xA> = eu.1 zU in
  let _ = free A xA in
  e'

d;g |- v: A handle
c = u#a
d |- u = u1+u2:cap~ ~~> eu     // eu:U(u)<->U(u1)*U(u2)
d |- u1#a <= a'+{A+} ~~> es    // es:!S(u1#a <= a'+{A+})
d;g;c |- e ~~> e'
---------------------------
d;g;c |- let use v in e ~~>
  let <zU1,zU2> = eu.1 zU in   // zU:U(c), zU1:U(u1), zU2:U(u2)
  let !zA' = es P zA in         // zA:!(A(a'+{A+}) (P*U(u1)))
  let Q,(!xPQ,!zA'') = zA' in    // xPQ:(P*U(u1)=>>Q), zA'':!(A[a'+{A+}] Q)
  let (_,!zA''') = zA'' in      // zA''':!(A({A+}) Q)
  let R,(!xQR,!xRA) = zA''' in  // xQR:(Q=>>R),  xRA:R=>>X A
  let !xPR = trans xPQ xQR in   // xPA:(P*U(u1)=>>R)
  let !xPA = trans xPR xRA in   // xPA:(P*U(u1)=>>X A)
  let <xA,xAP> = xPA <zP,zU1> in  // xA:X A, xAP:(A -o P*U(U1))
  let xA = use A xA in
  let <zP,zU1> = xAP xA in
  let zU = eu.2 <zU1,zU2> in
  e'

d;g |- v1: (u'#a',t)->0 ~~> e1
d;g |- v2: t ~~> e2
d |- u = ub+u':cap~ ~~> eu         // eu:U(u)<->U(ub)*U(U')
d |- ub#a <= a' ~~> es             // es:!S(ub#a <= a')
------------------------------
d;g;u#a |- v1 v2 ~~>
  let <zUb,zU'> = eu.1 zU in       // zUb:U(ub), zU':U(U')
  let !zA' = es P zA in             // zA':!(A(a') (P*U(ub))
  e1 (P*U(ub)) <zP,zUb> zU' zA' e2

d |- u = {}:cap~ ~~> eu
d |- a = {}:cap+ ~~> ea
-----------------------
d;g;u#a |- halt ~~>
  let _ = eu.1 zU in
  pack [P,zP] as true

=================================================

d |- u1 = u1':cap~ ~~> e1
d |- u2 = u2':cap~ ~~> e2
-------------------------
d |- u1+u2 = u1'+u2':cap~ ~~> lprod e1 e2

d |- u:cap~
------------------
d |- {}+u = u:cap~ ~~> lprodlunitleftleft

d |- u1:cap~
d |- u2:cap~
-----------------------
d |- u1+u2 = u2+u1:cap~ ~~> lprodcomm

d |- u1:cap~
d |- u2:cap~
d |- u3:cap~
---------------------------------
d |- (u1+u2)+u3 = u1+(u2+u3):cap~ ~~> symm lprodassoc

d |- a1 = a1':cap+ ~~> e1
d |- a2 = a2':cap+ ~~> e2
-------------------------
d |- a1+a2 = a1'+a2':cap+ ~~>
  !\P:type. exist (!\Q:type.prod refl (prod (e1 Q) (e2 Q)))

d |- a:cap+
------------------
d |- {}+a = a:cap+ ~~>
TODO: transcribe from code
  !\P:type.
  let f1 = (
  ) in
  let f2 = (
  ) in
  (f1,f2)

d |- a1:cap+
d |- a2:cap+
-----------------------
d |- a1+a2 = a2+a1:cap+ ~~>
  !\P:type. exist (!\Q:type.prod refl prodcomm)

d |- a1:cap+
d |- a2:cap+
d |- a3:cap+
---------------------------------
d |- (a1+a2)+a3 = a1+(a2+a3):cap+ ~~>
  !\P:type.
  let f1 = (
    !\[Q,(!xPQ, (!x12, !x3))]:!(A((a1+a2)+a3) P).// xPQ:P=>>Q, x12:!(A(a1+a2) Q), x3:!(A(a3) Q)
    let R,(!xQR,(!x1,!x2)) = x12 in           // xQR:Q=>>R, x1:!(A(a1) R), x2:!(A(a2) R)
    let S,(!xRS,!xA2) = x2 in                // xRS:R=>>S, xA2:!(A[a2] S)
    let S',(!xRS',!xA1) = x1 in              // xRS':R=>>S' xA1:!(A[a1] S')
    let !y1 = !pack[S',(trans xQR xRS', xA1) as (A(a1) Q) in
    let !y2 = !pack[S,(trans xQR xRS, xA2)] as (A(a2) Q) in
    let !y23 = !pack[Q,(refl,(y2,x3))] as (A(a2+a3) Q) in
    !pack[Q,(xPQ,(y1,y23))] as (A(a1+(a2+a3)) P)
  ) in
  let f2 = (
    !\[Q,(!xPQ, (!x1, !x23))]:!(A(a1+(a2+a3)) P).// xPQ:P=>>Q, x1:!(A(a1) Q), x3:!(A(a2+a3) Q)
    let R,(!xQR,(!x2,!x3)) = x23 in           // xQR:Q=>>R, x2:!(A(a2) R), x3:!(A(a3) R)
    let S,(!xRS,!xA2) = x2 in                // xRS:R=>>S, xA2:!(A[a2] S)
    let S',(!xRS',!xA3) = x3 in              // xRS':R=>>S' xA3:!(A[a3] S')
    let !y3 = !pack[S',(trans xQR xRS', xA3) as (A(a3) Q) in
    let !y2 = !pack[S,(trans xQR xRS, xA2)] as (A(a2) Q) in
    let !y12 = !pack[Q,(refl,(x1,y2))] as (A(a1+a2) Q) in
    !pack[Q,(xPQ,(y12,y3))] as (A((a1+a2)+a3) P)
  ) in
  (f1,f2)

d |- a1:cap+
--------------------
d |- a1 = a1+a1:cap+ ~~>
TODO: transcribe from code
//  !\P:type. dup


=================================================

...,(A:cap+ where ...,uk#A<=ak,...),... |- u#A<=a ~~> xAk

d |- A:res
--------------------
d |- {A~}#{} <= {A+} ~~>
  !\P:type.
  !\!x1:!(A({}) P).           // x1:!(A({}) P)
  let !xUA = getright in       // xUA: P*(X A)=>>(X A)
  let !xAA = refl in           // xAA: (X A)=>>(X A)
  !pack[X A,(xUA,xAA)] as (A({A+}) (P*(X A)))

d |- a1 = a2:cap+ ~~> e       // e:all P:type.!(A(a1) P)<->!(A(a2) P)
-----------------
d |- {}#a1 <= a2 ~~>
  !\P:type.
  !\x1:!(A(a1) P).            // x1:!(A(a1) P)
  let !x2 = (e P).1 x1         // x2:!(A(a2) P)
  let Q,(!xPQ,!xA) = x2 in      // xPQ:P=>>Q, xA:!(A[a2] Q)
  let !xUP = getleft in        // xUP:P*() =>> P
  let !xUQ = trans xUP xPQ in  // xUQ:P*() =>> Q
  !pack[Q,(xUQ,xA)] as (A(a2) P*())

d |- u1#a1 <= a2 ~~> e1       // e1: !all Q:type.!(A(a1) Q) -> !(A(a2) (Q*U(u1)))
d |- u2#a2 <= a3 ~~> e2       // e2: !all Q:type.!(A(a2) Q) -> !(A(a3) (Q*U(u2)))
-------------------
d |- u1+u2#a1 <= a3 ~~>
  !\P:type.
  !\x1:!(A(a1) P).            // x1:!(A(a1) P)
  let !x2 = e1 P x1 in         // x2:!(A(a2) (P*U(u1)))
  let !x3 = e2 (P*U(u1)) x2 in // x3:!(A(a3) ((P*U(u1))*U(u2)))
  let Q,(!xP1_2Q,!xA) = x3 in          // xP1_2Q:(P*U(u1))*U(u2)=>>Q, xA:!(A[a3] Q)
  let !y = extractinter lprodassoc in // y:P*(U(u1))*U(u2))=>>(P*U(u1))*U(u2)
  let !xP_12Q = trans y xP1_2 in      // xP_12Q:P*(U(u1))*U(u2))=>>Q
  !pack[Q,(xP_12Q,xA) as (A(a3) (P*U(u1+u2)))

d |- u1#a1 <= a1' ~~> e1        // e1: !all Q:type.!(A(a1) Q) -> !(A(a1') (Q*U(u1)))
d |- u2#a2 <= a2' ~~> e2        // e2: !all Q:type.!(A(a2) Q) -> !(A(a2') (Q*U(u2)))
---------------------------
d |- u1+u2#a1+a2 <= a1'+a2' ~~>
  !\P:type.
  !\x:!(A(a1+a2) P).            // x:!(A(a1+a2) P)
  let Q,(!xPQ,!xA12) = x in       // xPQ:P=>>Q, xA12:!(A[a1+a2] Q)
  let (!xA1,!xA2) = xA12 in       // xA1:!(A(a1) Q), xA2:!(A(a2) Q)
  let !x1' = e1 Q xA1 in         // x1':!(A(a1') (Q*U(u1)))
  let !x2' = e2 Q xA2 in         // x2':!(A(a2') (Q*U(u2)))
  let Q1',(!xQQ1,!xA1') = x1' in  // xQQ1:Q*U(u1)=>>Q1', xA1':!(A[a1'] Q1')
  let Q2',(!xQQ2,!xA2') = x2' in  // xQQ2:Q*U(u2)=>>Q2', xA2':!(A[a2'] Q2')
  let !xQ12_Q1 = getrightleft in // xQ12_Q1:Q*U(u1+u2)=>>Q*U(u1)
  let !xQ12_Q2 = getrightright in// xQ12_Q2:Q*U(u1+u2)=>>Q*U(u2)
  let !xQ121 = trans xQ12_Q1 xQQ1 in // xQ121:Q*U(u1+u2)=>>Q1'
  let !xQ122 = trans xQ12_Q2 xQQ2 in // xQ122:Q*U(u1+u2)=>>Q2'
  let !y1 = !pack[Q1',(xQ121,xA1')] as (A(a1') (Q*U(u1+u2))) in
  let !y2 = !pack[Q2',(xQ122,xA2')] as (A(a2') (Q*U(u1+u2))) in
  let !xPUQU = lprodleft xPQ in// xPUQU:P*U(u1+u2)=>>Q*U(u1+u2)
  !pack[Q*U(u1+u2),(xPUQU,(y1,y2))] as (A(a1'+a2') (P*U(u1+u2)))


/*
d |- u:cap~
d |- a:cap+
-------------- (optional)
d |- u#a <= {}
*/
=================================================

d |- t:type
---------------
d |- t = t:type ~~> refl

d |- t2 = t1:type ~~> e
-----------------
d |- t1 = t2:type ~~> symm e

d |- t1 = t2:type ~~> e1
d |- t2 = t3:type ~~> e2
-----------------
d |- t1 = t3:type ~~> trans e1 e2

d |- u:cap~
---------------
d |- u = u:cap~ ~~> refl

d |- u2 = u1:cap~ ~~> e
-----------------
d |- u1 = u2:cap~ ~~> symm e

d |- u1 = u2:cap~ ~~> e1
d |- u2 = u3:cap~ ~~> e2
-----------------
d |- u1 = u3:cap~ ~~> trans e1 e2

d |- a:cap+
---------------
d |- a = a:cap+ ~~> \P:type.refl

d |- a2 = a1:cap+ ~~> e
-----------------
d |- a1 = a2:cap+ ~~> \P:type. symm (e P)

d |- a1 = a2:cap+ ~~> e1
d |- a2 = a3:cap+ ~~> e2
-----------------
d |- a1 = a3:cap+ ~~> \P:type. trans (e1 P) (e2 P)

d |- t1 = t1':type ~~> e1
d |- t2 = t2':type ~~> e2
-----------------------------
d |- <t1,t2> = <t1',t2'>:type ~~> prod e1 e2

d,A:k |- t = t':type ~~> e
--------------------------------
d |- all A:k.t = all A:k.t':type ~~> all !\A:K(k).e

d |- u1 = u1':type ~~> eu1
...
d |- un = un':type ~~> eun
d |- a1 = a1':type ~~> ea1
...
d |- an = an':type ~~> ean
d |- t = t':type ~~> et
--------------------------------------------------------------------------------------------------
d |- all A:cap+ where u1#A<=a1,...,un#A<=an.t = all A:cap+ where u1'#A<=a1',...,un'#A<=an'.t':type ~~>
  all !\A:type->type. fun s1 (... (fun sn et)...)
  where sk = all !\P:type. funright
    (trans
      (eak (P*U(uk)))
      (exist (!\Q:type. prodleft (extractleft (lprodright euk)))))

d |- u = u':cap~ ~~> eu
d |- a = a':cap+ ~~> ea
d |- t = t':type ~~> et
----------------------------------------
d |- (u#a,t)->0 = (u'#a',t')->0:type ~~>
  all !\P:type. funright (lfun eu (lfun (ea P) (lfunleft et)))

=================================================
=================== LEMMAS ======================
=================================================

Translation lemmas:
 // easy proofs by induction:
  - if |- d and d |- u:cap~ then D(d),X:type->type |- U(u):type
  - if |- d and d |- a:cap+ then D(d),X:type->type |- A(a):type->type
  - if |- d and d |- t:type then D(d),X:type->type |- T(t):type

 // proofs in proof4.ml:
  - if |- d and d |- u1=u2:cap~~~>e then D(d),X:type->type;G(d;.) |- e: U(u1)<->U(u2)
  - if |- d and d |- a1=a2:cap+~~>e then D(d),X:type->type;G(d;.) |- e: !all P:type.!(A(a1) P)<->!(A(a2) P)
  - if |- d and d |- u1#a1<=a2~~>e then D(d),X:type->type;G(d;.) |- e: !S(u1#a1<=a2)
  - if |- d and d |- t1=t2:type~~>e then D(d),X:type->type;G(d;.) |- e: !T(t1)<->!T(t2)

 // proofs below:
 -- if |- d and d |- A':cap+ and d |- a:cap+ then A([A'<-a']a) = [A'<-A[a']]A(a)
 -- if |- d and d |- A':cap+ and d |- u:cap~ then U([A'<-a']u) = [A'<-a'']U(u) for any a''
 -- if |- d and d |- A':cap~ and d |- a:cap+ then A([A'<-u']a) = [A'<-u'']A(a) for any u''
 -- if |- d and d |- A':cap~ and d |- u:cap~ then U([A'<-u']u) = [A'<-U(u')]U(u)
 -- if |- d and d |- A':cap+ and d |- t:type then T([A'<-a']t) = [A'<-A[a']]T(t)
 -- if |- d and d |- A':cap~ and d |- t:type then T([A'<-u']t) = [A'<-U(u')]T(t)
 -- if |- d and d |- A':type and d |- t:type then T([A'<-t']t) = [A'<-T(t')]T(t)

 // proofs in proof4.ml:
  - if |- d and d |- g then:
    - if d;g |- v:t then D(d),X:type->type;G(d;g),g' |- V(v):!T(t)
    - if d;g |- h:t then D(d),X:type->type;G(d;g),g' |- H(h):!T(t)
    - if d;g;u#a |- e then D(d),X:type->type,P:type;G(d;g),g',zP:P,zU:U(u),!(zA:A(a) P) |- E(e):true
    where g' = !(new:() -o exists A:type.X A),
               !(free:all A:type.X A->()),
               !(use:all A:type.X A->X A)


=================================================

If |- d and d |- A':cap+ and d |- a:cap+ then A([A'<-a']a) = [A'<-A[a']]A(a)
If |- d and d |- A':cap~ and d |- a:cap+ then A([A'<-u']a) = [A'<-u'']A(a) for any u''

A(a) = \P:type. exists Q:type. (P =>> Q) x !(A[a] Q)
A([A'<-a']a)    = \P:type. exists Q:type. (P =>> Q) x !(A[[A'<-a']a]    Q)
[A'<-A[a']]A(a) = \P:type. exists Q:type. (P =>> Q) x !([A'<-A[a']]A(a) Q)
must show A[[A'<-a']a] = [A'<-A[a']]A(a)


CASE:

d |- A':cap+
A[A'] = A'

A[[A'<-a']A'] = A[a']
[A'<-A[a']]A[A'] = [A'<-A[a']]A' = A[a']


CASE:

d |- A':cap~
A[A'] = A'

Impossible case: d |- A':cap~ and d |- A':cap+ cannot both be true


EASY CASES:

A[A] = A
A[{}] = \P:type. <>
A[{A p}] = \P:type. (P =o> X A)
A[{A' p}] = \P:type. (P =o> X A')
A[a1+a2] = \P:type. !(A(a1) P) * !(A(a2) P)

=================================================

If |- d and d |- A':cap+ and d |- u:cap~ then U([A'<-a']u) = [A'<-a'']U(u) for any a''
If |- d and d |- A':cap~ and d |- u:cap~ then U([A'<-u']u) = [A'<-U(u')]U(u)


CASE:

d |- A':cap~
U(A') = A'

U([A'<-u']A') = U(u')
[A'<-U(u')]U(A') = [A'<-U(u')]A' = U(u')


CASE:

d |- A':cap+
U(A') = A'

Impossible case: d |- A':cap+ and d |- A':cap~ cannot both be true


EASY CASES:

U(A) = A
U({}) = ()
U({A p}) = X A
U({A' p}) = X A'
U(u1+u2) = U(u1) * U(u2)

=================================================

If |- d and d |- A':cap+ and d |- t:type then T([A'<-a']t) = [A'<-A[a']]T(t)
If |- d and d |- A':cap~ and d |- t:type then T([A'<-u']t) = [A'<-U(u')]T(t)

EASY CASES:

T(A') = A'
T(A) = A
T(<t1,t2>) = !T(t1) * !T(t2)
T(all A:k.t) = all A:K(k).!T(t)
T(A' handle) = <>
T(A handle) = <>

CASE:

T((u#a,t)->0) = all P:type. P -> U(u) -o !(A(a) P) -o !T(t) -o true

(if d |- A':cap~):
  T([A'<-u'](u#a,t)->0) = all P:type. P -> U([A'<-u']u) -o !(A([A'<-u']a) P) -o !T([A'<-u']t) -o true
                        = all P:type. P -> [A'<-U(u')]U(u) -o !([A'<-U(u')]A(a) P) -o ![A'<-U(u')]T(t) -o true
                        = [A'<-U(u')]T((u#a,t)->0)

(if d |- A':cap+):
  T([A'<-a'](u#a,t)->0) = all P:type. P -> U([A'<-a']u) -o !(A([A'<-a']a) P) -o !T([A'<-a']t) -o true
                        = all P:type. P -> [A'<-A[a']]U(u) -o !([A'<-A[a']]A(a) P) -o ![A'<-A[a']]T(t) -o true
                        = [A'<-A[a']]T((u#a,t)->0)


CASE:

T(all A:cap+ where u1#A<=a1,...,un#A<=an.t) = all A:type->type. !S(u1#A<=a1) -> ... -> !S(un#A<=an) -> !T(t)

Similar to case above.


=================================================

If |- d and d |- A':type and d |- t:type then T([A'<-t']t) = [A'<-T(t')]T(t)


EASY CASES:

T(A') = A'
T(A) = A
T(<t1,t2>) = !T(t1) * !T(t2)
T(all A:k.t) = all A:K(k).!T(t)
T(all A:cap+ where c1<=a1,...,cn<=an.t) = all A:type->type. !S(c1<=a1) -> ... -> !S(cn<=an) -> !T(t)
T((u#a,t)->0) = all P:type. P -> U(u) -o !(A(a) P) -o !T(t) -o true
T(A' handle) = <>
T(A handle) = <>