Twelf 1.5R3, Aug 30, 2005 (%trustme)
%% OK %%
[Opening file /home/www/twelf/hcode/e9fbcbbeec08af49f8ae28cff66db426]
uninhabited : type.
%freeze uninhabited.
nat : type.
z : nat.
s : nat -> nat.
id-nat : nat -> nat -> type.
id-nat/refl : {N:nat} id-nat N N.
lt : nat -> nat -> type.
lt/z : {N:nat} lt z (s N).
lt/s : {N1:nat} {N2:nat} lt N1 N2 -> lt (s N1) (s N2).
id-lt : {N:nat} {M:nat} {N':nat} {M':nat} lt N M -> lt N' M' -> type.
id-lt/refl : {X1:nat} {X2:nat} {L:lt X1 X2} id-lt L L.
lt12 : nat -> nat -> type.
lt12/1 : {N:nat} lt12 N (s N).
lt12/2 : {N:nat} {M:nat} lt N M -> lt12 N (s M).
lt+ : {M:nat} {N:nat} lt M N -> lt M (s N) -> type.
%mode +{M:nat} +{N:nat} +{D:lt M N} -{D2:lt M (s N)} (lt+ D D2).
lt+/z : {X1:nat} lt+ lt/z lt/z.
lt+/s :
   {X1:nat} {X2:nat} {LT1:lt X1 X2} {LT2:lt X1 (s X2)}
      lt+ LT1 LT2 -> lt+ (lt/s LT1) (lt/s LT2).
%worlds () (lt+ _ _).
%total T (lt+ T _).
lts : {N:nat} lt N (s N) -> type.
%mode +{N:nat} -{LT:lt N (s N)} (lts N LT).
lts/z : lts z lt/z.
lts/s : {N:nat} {D:lt N (s N)} lts N D -> lts (s N) (lt/s D).
%worlds () (lts _ _).
%total T (lts T _).
lt+-irrev :
   {N1:nat} {N2:nat} {L2:lt N1 (s N2)} {L1:lt N1 N2}
      lt+ L1 L2 -> ({L1':lt N1 N2} lt+ L1' L2 -> type).
%mode +{N1:nat} +{N2:nat} +{L2:lt N1 (s N2)} +{L1:lt N1 N2} +{L3:lt+ L1 L2}
   +{L1':lt N1 N2} -{L4:lt+ L1' L2} (lt+-irrev L1 L3 L1' L4).
- : {X1:nat} lt+-irrev lt/z lt+/z lt/z lt+/z.
- :
   {X1:nat} {X2:nat} {X3:lt X1 (s X2)} {L1:lt X1 X2} {L1+:lt+ L1 X3}
      {L2:lt X1 X2} {L2+:lt+ L2 X3}
      lt+-irrev L1 L1+ L2 L2+
         -> lt+-irrev (lt/s L1) (lt+/s L1+) (lt/s L2) (lt+/s L2+).
%worlds () (lt+-irrev _ _ _ _).
%total T (lt+-irrev T _ _ _).
can-lts : {N:nat} {LT:lt N (s N)} lts N LT -> type.
%mode +{N:nat} +{LT:lt N (s N)} -{LTS:lts N LT} (can-lts N LT LTS).
- : can-lts z lt/z lts/z.
- :
   {N:nat} {LT:lt N (s N)} {LTS:lts N LT}
      can-lts N LT LTS -> can-lts (s N) (lt/s LT) (lts/s LTS).
%worlds () (can-lts _ _ _).
%total T (can-lts T _ _).
can-lt+ : {M:nat} {N:nat} {LT:lt M N} {LT':lt M (s N)} lt+ LT LT' -> type.
%mode +{M:nat} +{N:nat} +{LT:lt M N} +{LT':lt M (s N)} -{LT+:lt+ LT LT'}
   (can-lt+ LT LT' LT+).
- : {X1:nat} can-lt+ lt/z lt/z lt+/z.
- :
   {X1:nat} {X2:nat} {LT:lt X1 X2} {LT':lt X1 (s X2)} {LT+:lt+ LT LT'}
      can-lt+ LT LT' LT+ -> can-lt+ (lt/s LT) (lt/s LT') (lt+/s LT+).
%worlds () (can-lt+ _ _ _).
%total T (can-lt+ T _ _).
lt-s-cong :
   {X1:nat} {X2:nat} {X3:nat} {X4:nat} {L1:lt X1 X2} {L1':lt X3 X4}
      id-lt L1 L1' -> id-lt (lt/s L1) (lt/s L1') -> type.
%mode +{X1:nat} +{X2:nat} +{X3:nat} +{X4:nat} +{L1:lt X1 X2} +{L1':lt X3 X4}
   +{ID1:id-lt L1 L1'} -{ID2:id-lt (lt/s L1) (lt/s L1')} (lt-s-cong ID1 ID2).
- : {X1:nat} {X2:nat} {X3:lt X1 X2} lt-s-cong id-lt/refl id-lt/refl.
%worlds () (lt-s-cong _ _).
%total {} (lt-s-cong _ _).
lt+-uniq :
   {X1:nat} {X2:nat} {X3:nat} {X4:nat} {L1:lt X1 X2} {L2:lt X3 X4}
      {L1':lt X1 (s X2)} {L2':lt X3 (s X4)}
      id-lt L1 L2 -> lt+ L1 L1' -> lt+ L2 L2' -> id-lt L1' L2' -> type.
%mode +{X1:nat} +{X2:nat} +{X3:nat} +{X4:nat} +{L1:lt X1 X2} +{L2:lt X3 X4}
   +{L1':lt X1 (s X2)} +{L2':lt X3 (s X4)} +{ID:id-lt L1 L2} +{L3:lt+ L1 L1'}
   +{L4:lt+ L2 L2'} -{ID2:id-lt L1' L2'} (lt+-uniq ID L3 L4 ID2).
- : {X1:nat} lt+-uniq id-lt/refl lt+/z lt+/z id-lt/refl.
- :
   {X1:nat} {X2:nat} {X3:lt X1 (s X2)} {X4:lt X1 (s X2)} {ID2:id-lt X3 X4}
      {ID:id-lt (lt/s X3) (lt/s X4)} {X5:lt X1 X2} {LT+1:lt+ X5 X3}
      {LT+2:lt+ X5 X4}
      lt-s-cong ID2 ID -> lt+-uniq id-lt/refl LT+1 LT+2 ID2
         -> lt+-uniq id-lt/refl (lt+/s LT+1) (lt+/s LT+2) ID.
%worlds () (lt+-uniq _ _ _ _).
%total T (lt+-uniq _ T _ _).
lts-uniq :
   {N1:nat} {N2:nat} {L1:lt N1 (s N1)} {L2:lt N2 (s N2)}
      id-nat N1 N2 -> lts N1 L1 -> lts N2 L2 -> id-lt L1 L2 -> type.
%mode +{N1:nat} +{N2:nat} +{L1:lt N1 (s N1)} +{L2:lt N2 (s N2)} +{ID:id-nat N1 N2}
   +{L3:lts N1 L1} +{L4:lts N2 L2} -{ID2:id-lt L1 L2} (lts-uniq ID L3 L4 ID2).
- : lts-uniq id-nat/refl lts/z lts/z id-lt/refl.
- :
   {X1:nat} {X2:lt X1 (s X1)} {X3:lt X1 (s X1)} {ID1:id-lt X2 X3}
      {ID:id-lt (lt/s X2) (lt/s X3)} {LT1:lts X1 X2} {LT2:lts X1 X3}
      lt-s-cong ID1 ID -> lts-uniq id-nat/refl LT1 LT2 ID1
         -> lts-uniq id-nat/refl (lts/s LT1) (lts/s LT2) ID.
%worlds () (lts-uniq _ _ _ _).
%total T (lts-uniq _ T _ _).
lt-opt-s : {N:nat} {M:nat} lt12 N M -> lt12 (s N) (s M) -> type.
%mode +{N:nat} +{M:nat} +{D:lt12 N M} -{D2:lt12 (s N) (s M)} (lt-opt-s D D2).
lt-opt-s/1 : {X1:nat} lt-opt-s lt12/1 lt12/1.
lt-opt-s/2 :
   {X1:nat} {X2:nat} {LT:lt X1 X2} lt-opt-s (lt12/2 LT) (lt12/2 (lt/s LT)).
%worlds () (lt-opt-s _ _).
%total {} (lt-opt-s _ _).
lt-opt : {N:nat} {M:nat} lt N M -> lt12 N M -> type.
%mode +{N:nat} +{M:nat} +{D:lt N M} -{D2:lt12 N M} (lt-opt D D2).
lt-opt/z1 : lt-opt lt/z lt12/1.
lt-opt/z2 : {X1:nat} lt-opt lt/z (lt12/2 lt/z).
lt-opt/s :
   {X1:nat} {X2:nat} {LT12:lt12 X1 X2} {LT12':lt12 (s X1) (s X2)} {LT:lt X1 X2}
      lt-opt-s LT12 LT12' -> lt-opt LT LT12 -> lt-opt (lt/s LT) LT12'.
%worlds () (lt-opt _ _).
%total T (lt-opt T _).
lt-opt-succ1 : {N:nat} {LT:lt N (s N)} lt-opt LT lt12/1 -> type.
%mode +{N:nat} +{LT:lt N (s N)} -{LTO:lt-opt LT lt12/1} (lt-opt-succ1 LT LTO).
- : lt-opt-succ1 lt/z lt-opt/z1.
- :
   {X1:nat} {LT:lt X1 (s X1)} {LTS:lt-opt LT lt12/1}
      lt-opt-succ1 LT LTS -> lt-opt-succ1 (lt/s LT) (lt-opt/s lt-opt-s/1 LTS).
%worlds () (lt-opt-succ1 _ _).
%total T (lt-opt-succ1 T _).
lt-opt-succ2 :
   {X1:nat} {X2:nat} {LT:lt X1 X2} {LT':lt X1 (s X2)}
      lt+ LT LT' -> lt-opt LT' (lt12/2 LT) -> type.
%mode +{X1:nat} +{X2:nat} +{LT:lt X1 X2} +{LT':lt X1 (s X2)} +{LT1:lt+ LT LT'}
   -{LT0:lt-opt LT' (lt12/2 LT)} (lt-opt-succ2 LT1 LT0).
- : {X1:nat} lt-opt-succ2 lt+/z lt-opt/z2.
- :
   {X1:nat} {X2:nat} {X3:lt X1 X2} {X4:lt X1 (s X2)} {LT+:lt+ X3 X4}
      {LTO:lt-opt X4 (lt12/2 X3)}
      lt-opt-succ2 LT+ LTO -> lt-opt-succ2 (lt+/s LT+) (lt-opt/s lt-opt-s/2 LTO).
%worlds () (lt-opt-succ2 _ _).
%total T (lt-opt-succ2 T _).
lt-opt2-s-uniq :
   {X1:nat} {X2:nat} {X3:nat} {X4:nat} {LT1:lt X1 X2} {LT1':lt X3 X4}
      {LT2:lt (s X1) (s X2)} {LT2':lt (s X3) (s X4)}
      id-lt LT1 LT1' -> lt-opt-s (lt12/2 LT1) (lt12/2 LT2)
         -> lt-opt-s (lt12/2 LT1') (lt12/2 LT2') -> id-lt LT2 LT2' -> type.
%mode +{X1:nat} +{X2:nat} +{X3:nat} +{X4:nat} +{LT1:lt X1 X2} +{LT1':lt X3 X4}
   +{LT2:lt (s X1) (s X2)} +{LT2':lt (s X3) (s X4)} +{ID:id-lt LT1 LT1'}
   +{D1:lt-opt-s (lt12/2 LT1) (lt12/2 LT2)}
   +{D2:lt-opt-s (lt12/2 LT1') (lt12/2 LT2')} -{ID2:id-lt LT2 LT2'}
   (lt-opt2-s-uniq ID D1 D2 ID2).
- :
   {X1:nat} {X2:nat} {X3:lt X1 X2}
      lt-opt2-s-uniq id-lt/refl lt-opt-s/2 lt-opt-s/2 id-lt/refl.
%worlds () (lt-opt2-s-uniq _ _ _ _).
%total {} (lt-opt2-s-uniq _ _ _ _).
lt-opt2-uniq :
   {X1:nat} {X2:nat} {X3:nat} {X4:nat} {LT1:lt X1 (s X2)} {LT1':lt X3 (s X4)}
      {LT2:lt X1 X2} {LT2':lt X3 X4}
      id-lt LT1 LT1' -> lt-opt LT1 (lt12/2 LT2) -> lt-opt LT1' (lt12/2 LT2')
         -> id-lt LT2 LT2' -> type.
%mode +{X1:nat} +{X2:nat} +{X3:nat} +{X4:nat} +{LT1:lt X1 (s X2)} +{LT1':lt X3 (s X4)}
   +{LT2:lt X1 X2} +{LT2':lt X3 X4} +{ID1:id-lt LT1 LT1'}
   +{L1:lt-opt LT1 (lt12/2 LT2)} +{L2:lt-opt LT1' (lt12/2 LT2')}
   -{ID2:id-lt LT2 LT2'} (lt-opt2-uniq ID1 L1 L2 ID2).
- : {X1:nat} lt-opt2-uniq id-lt/refl lt-opt/z2 lt-opt/z2 id-lt/refl.
- :
   {X1:nat} {X2:nat} {X3:lt X1 X2} {X4:lt X1 X2} {X5:lt (s X1) (s X2)}
      {X6:lt (s X1) (s X2)} {ID1:id-lt X3 X4}
      {LS:lt-opt-s (lt12/2 X3) (lt12/2 X5)}
      {LS':lt-opt-s (lt12/2 X4) (lt12/2 X6)} {ID:id-lt X5 X6} {X7:lt X1 (s X2)}
      {L:lt-opt X7 (lt12/2 X3)} {L':lt-opt X7 (lt12/2 X4)}
      lt-opt2-s-uniq ID1 LS LS' ID -> lt-opt2-uniq id-lt/refl L L' ID1
         -> lt-opt2-uniq id-lt/refl (lt-opt/s LS L) (lt-opt/s LS' L') ID.
%worlds () (lt-opt2-uniq _ _ _ _).
%total T (lt-opt2-uniq _ T _ _).
lt-opt-excl :
   {X1:nat} {LT:lt X1 (s X1)} {L:lt X1 X1}
      lt-opt LT lt12/1 -> lt-opt LT (lt12/2 L) -> uninhabited -> type.
%mode +{X1:nat} +{LT:lt X1 (s X1)} +{L:lt X1 X1} +{D1:lt-opt LT lt12/1}
   +{D2:lt-opt LT (lt12/2 L)} -{D3:uninhabited} (lt-opt-excl D1 D2 D3).
- :
   {X1:nat} {X2:lt X1 (s X1)} {X3:lt X1 X1} {L:lt-opt X2 lt12/1}
      {L':lt-opt X2 (lt12/2 X3)} {X:uninhabited} {X4:lt (s X1) (s X1)}
      {LS:lt-opt-s lt12/1 lt12/1} {LS':lt-opt-s (lt12/2 X3) (lt12/2 X4)}
      lt-opt-excl L L' X -> lt-opt-excl (lt-opt/s LS L) (lt-opt/s LS' L') X.
%worlds () (lt-opt-excl _ _ _).
%total T (lt-opt-excl T _ _).
exp : type.
lam : (exp -> exp) -> exp.
app : exp -> exp -> exp.
%block blocksimple : block {v:exp}.
id-exp : exp -> exp -> type.
id-exp/refl : {E:exp} id-exp E E.
id-lam-cong :
   {E:exp -> exp} {E':exp -> exp}
      ({v:exp} id-exp (E v) (E' v))
         -> id-exp (lam ([x:exp] E x)) (lam ([x:exp] E' x)) -> type.
- : {X1:exp -> exp} id-lam-cong ([v:exp] id-exp/refl) id-exp/refl.
%mode +{E:exp -> exp} +{E':exp -> exp} +{I1:{v:exp} id-exp (E v) (E' v)}
   -{I:id-exp (lam ([x:exp] E x)) (lam ([x:exp] E' x))} (id-lam-cong I1 I).
%worlds (blocksimple) (id-lam-cong _ _).
%total {} (id-lam-cong _ _).
id-app-cong :
   {E1:exp} {E1':exp} {E2:exp} {E2':exp}
      id-exp E1 E1' -> id-exp E2 E2' -> id-exp (app E1 E2) (app E1' E2') -> type.
- : {X1:exp} {X2:exp} id-app-cong id-exp/refl id-exp/refl id-exp/refl.
%mode +{E1:exp} +{E1':exp} +{E2:exp} +{E2':exp} +{I1:id-exp E1 E1'}
   +{I2:id-exp E2 E2'} -{I:id-exp (app E1 E2) (app E1' E2')}
   (id-app-cong I1 I2 I).
%worlds (blocksimple) (id-app-cong _ _ _).
%total {} (id-app-cong _ _ _).
isvar : exp -> type.
%block blockvar : block {v:exp} {iv:isvar v}.
case : exp -> type.
case/lam : {E:exp -> exp} case (lam ([x:exp] E x)).
case/app : {E1:exp} {E2:exp} case (app E1 E2).
case/var : {V:exp} isvar V -> case V.
can-case : {E:exp} case E -> type.
fake : {E:exp} {C:case E} can-case E C -> can-case E C -> type.
- :
   {X:exp} {Y:case X} {X':exp} {Y':case X'} {X1:exp} {X2:case X1}
      {E:can-case X1 X2} {F:can-case X1 X2}
      (can-case X Y -> can-case X' Y') -> fake E F.
%block blockcases : block {v:exp} {iv:isvar v} {d:can-case v (case/var iv)}.
can-case/lam : {E:exp -> exp} can-case (lam ([x:exp] E x)) case/lam.
can-case/app : {E1:exp} {E2:exp} can-case (app E1 E2) case/app.
%mode +{E:exp} -{C:case E} (can-case E C).
%worlds (blockcases) (can-case _ _).
%total T (can-case T _).
etree : type.
etree/lam : etree -> etree.
etree/app : etree -> etree -> etree.
etree/var : etree.
id-etree : etree -> etree -> type.
id-etree/refl : {E:etree} id-etree E E.
id-etree/app-cong :
   {E1:etree} {E1':etree} {E2:etree} {E2':etree}
      id-etree E1 E1' -> id-etree E2 E2'
         -> id-etree (etree/app E1 E2) (etree/app E1' E2') -> type.
%mode +{E1:etree} +{E1':etree} +{E2:etree} +{E2':etree} +{ID:id-etree E1 E1'}
   +{ID2:id-etree E2 E2'} -{ID':id-etree (etree/app E1 E2) (etree/app E1' E2')}
   (id-etree/app-cong ID ID2 ID').
- :
   {X1:etree} {X2:etree}
      id-etree/app-cong id-etree/refl id-etree/refl id-etree/refl.
%worlds () (id-etree/app-cong _ _ _).
%total {} (id-etree/app-cong _ _ _).
id-etree/lam-cong :
   {E:etree} {E':etree}
      id-etree E E' -> id-etree (etree/lam E) (etree/lam E') -> type.
%mode +{E:etree} +{E':etree} +{ID:id-etree E E'}
   -{ID':id-etree (etree/lam E) (etree/lam E')} (id-etree/lam-cong ID ID').
- : {X1:etree} id-etree/lam-cong id-etree/refl id-etree/refl.
%worlds () (id-etree/lam-cong _ _).
%total {} (id-etree/lam-cong _ _).
exp^ : nat -> etree -> type.
lam^ : {N:nat} {Et:etree} exp^ (s N) Et -> exp^ N (etree/lam Et).
app^ :
   {N:nat} {Et1:etree} {Et2:etree}
      exp^ N Et1 -> exp^ N Et2 -> exp^ N (etree/app Et1 Et2).
fvar^ : {N:nat} {x:exp} isvar x -> exp^ N etree/var.
bvar^ : {M:nat} {n:nat} lt n M -> exp^ M etree/var.
id-exp^ : {N:nat} {E1:etree} {M:nat} {E2:etree} exp^ N E1 -> exp^ M E2 -> type.
id-exp^/refl : {X1:nat} {X2:etree} {E:exp^ X1 X2} id-exp^ E E.
id-bvar^-cong :
   {N:nat} {N':nat} {X1:nat} {X2:nat} {LT:lt N X1} {LT':lt N' X2}
      id-nat N N' -> id-lt LT LT' -> id-exp^ (bvar^ N LT) (bvar^ N' LT') -> type.
- :
   {X1:nat} {X2:nat} {X3:lt X1 X2}
      id-bvar^-cong id-nat/refl id-lt/refl id-exp^/refl.
%mode +{N:nat} +{N':nat} +{X1:nat} +{X2:nat} +{LT:lt N X1} +{LT':lt N' X2}
   +{D1:id-nat N N'} +{D2:id-lt LT LT'}
   -{D^:id-exp^ (bvar^ N LT) (bvar^ N' LT')} (id-bvar^-cong D1 D2 D^).
%worlds (blockvar) (id-bvar^-cong _ _ _).
%total {} (id-bvar^-cong _ _ _).
id-app^-cong :
   {X1:nat} {X2:etree} {X3:nat} {X4:etree} {E1:exp^ X1 X2} {E1':exp^ X3 X4}
      {X5:etree} {X6:etree} {E2:exp^ X1 X5} {E2':exp^ X3 X6}
      id-exp^ E1 E1' -> id-exp^ E2 E2' -> id-exp^ (app^ E1 E2) (app^ E1' E2')
         -> type.
- :
   {X1:nat} {X2:etree} {X3:exp^ X1 X2} {X4:etree} {X5:exp^ X1 X4}
      id-app^-cong id-exp^/refl id-exp^/refl id-exp^/refl.
%mode +{X1:nat} +{X2:etree} +{X3:nat} +{X4:etree} +{E1:exp^ X1 X2} +{E1':exp^ X3 X4}
   +{X5:etree} +{X6:etree} +{E2:exp^ X1 X5} +{E2':exp^ X3 X6}
   +{D1:id-exp^ E1 E1'} +{D:id-exp^ E2 E2'}
   -{D2:id-exp^ (app^ E1 E2) (app^ E1' E2')} (id-app^-cong D1 D D2).
%worlds (blockvar) (id-app^-cong _ _ _).
%total {} (id-app^-cong _ _ _).
id-lam^-cong :
   {X1:nat} {X2:etree} {X3:nat} {X4:etree} {E:exp^ (s X1) X2}
      {E':exp^ (s X3) X4} id-exp^ E E' -> id-exp^ (lam^ E) (lam^ E') -> type.
- :
   {X1:nat} {X2:etree} {X3:exp^ (s X1) X2}
      id-lam^-cong id-exp^/refl id-exp^/refl.
%mode +{X1:nat} +{X2:etree} +{X3:nat} +{X4:etree} +{E:exp^ (s X1) X2}
   +{E':exp^ (s X3) X4} +{D1:id-exp^ E E'} -{D2:id-exp^ (lam^ E) (lam^ E')}
   (id-lam^-cong D1 D2).
%worlds (blockvar) (id-lam^-cong _ _).
%total {} (id-lam^-cong _ _).
bind :
   {N:nat} {Et:etree} ({v:exp} isvar v -> exp^ N Et) -> exp^ (s N) Et -> type.
%mode +{N:nat} +{Et:etree} +{E1:{v:exp} isvar v -> exp^ N Et} -{E:exp^ (s N) Et}
   (bind E1 E).
bind/match :
   {N:nat} {LT:lt N (s N)}
      lts N LT -> bind ([v:exp] [iv:isvar v] fvar^ v iv) (bvar^ N LT).
bind/fvar :
   {X1:nat} {X:exp} {V:isvar X}
      bind ([v:exp] [iv:isvar v] fvar^ X V) (fvar^ X V).
bind/bvar :
   {M:nat} {X1:nat} {LT:lt M X1} {LT':lt M (s X1)}
      lt+ LT LT' -> bind ([v:exp] [iv:isvar v] bvar^ M LT) (bvar^ M LT').
bind/app :
   {X1:nat} {X2:etree} {E2:{x:exp} isvar x -> exp^ X1 X2} {E2':exp^ (s X1) X2}
      {X3:etree} {E1:{x:exp} isvar x -> exp^ X1 X3} {E1':exp^ (s X1) X3}
      bind ([v:exp] [iv:isvar v] E2 v iv) E2'
         -> bind ([v:exp] [iv:isvar v] E1 v iv) E1'
         -> bind ([v:exp] [iv:isvar v] app^ (E1 v iv) (E2 v iv)) (app^ E1' E2').
bind/lam :
   {X1:nat} {X2:etree} {E:{x:exp} isvar x -> exp^ (s X1) X2}
      {E':exp^ (s (s X1)) X2}
      bind ([v:exp] [iv:isvar v] E v iv) E'
         -> bind ([v:exp] [iv:isvar v] lam^ (E v iv)) (lam^ E').
%worlds (blockvar) (bind _ _).
%total T (bind T _).
unbind-bvar :
   {M:nat} {N:nat} lt12 M (s N) -> ({v:exp} isvar v -> exp^ N etree/var) -> type.
%mode +{M:nat} +{N:nat} +{LT:lt12 M (s N)} -{E:{v:exp} isvar v -> exp^ N etree/var}
   (unbind-bvar LT E).
unbind-bvar/match :
   {X1:nat} unbind-bvar lt12/1 ([v:exp] [iv:isvar v] fvar^ v iv).
unbind-bvar/nomatch :
   {M:nat} {X1:nat} {LT:lt M X1}
      unbind-bvar (lt12/2 LT) ([v:exp] [iv:isvar v] bvar^ M LT).
%worlds (blockvar) (unbind-bvar _ _).
%total {} (unbind-bvar _ _).
unbind :
   {N:nat} {Et:etree} exp^ (s N) Et -> ({v:exp} isvar v -> exp^ N Et) -> type.
%mode +{N:nat} +{Et:etree} +{E1:exp^ (s N) Et} -{E2:{v:exp} isvar v -> exp^ N Et}
   (unbind E1 E2).
unbind/fvar :
   {X1:nat} {V':exp} {IV':isvar V'}
      unbind (fvar^ V' IV') ([v:exp] [iv:isvar v] fvar^ V' IV').
unbind/bvar :
   {M:nat} {X1:nat} {LT12:lt12 M (s X1)}
      {E:{x:exp} isvar x -> exp^ X1 etree/var} {LT:lt M (s X1)}
      unbind-bvar LT12 ([v:exp] [iv:isvar v] E v iv) -> lt-opt LT LT12
         -> unbind (bvar^ M LT) ([v:exp] [iv:isvar v] E v iv).
unbind/app :
   {X1:nat} {X2:etree} {E2:exp^ (s X1) X2} {E2':{x:exp} isvar x -> exp^ X1 X2}
      {X3:etree} {E1:exp^ (s X1) X3} {E1':{x:exp} isvar x -> exp^ X1 X3}
      unbind E2 ([v:exp] [iv:isvar v] E2' v iv)
         -> unbind E1 ([v:exp] [iv:isvar v] E1' v iv)
         -> unbind (app^ E1 E2)
               ([v:exp] [iv:isvar v] app^ (E1' v iv) (E2' v iv)).
unbind/lam :
   {X1:nat} {X2:etree} {E1:exp^ (s (s X1)) X2}
      {E1':{x:exp} isvar x -> exp^ (s X1) X2}
      unbind E1 ([v:exp] [iv:isvar v] E1' v iv)
         -> unbind (lam^ E1) ([v:exp] [iv:isvar v] lam^ (E1' v iv)).
%worlds (blockvar) (unbind _ _).
%total T (unbind T _).
bind-uniq :
   {X1:nat} {X2:etree} {X3:nat} {X4:etree} {Ea:{x:exp} isvar x -> exp^ X1 X2}
      {Ea':{x:exp} isvar x -> exp^ X3 X4} {Eb:exp^ (s X1) X2}
      {Eb':exp^ (s X3) X4}
      ({v:exp} {iv:isvar v} id-exp^ (Ea v iv) (Ea' v iv))
         -> bind ([v:exp] [x:isvar v] Ea v x) Eb
         -> bind ([v:exp] [x:isvar v] Ea' v x) Eb' -> id-exp^ Eb Eb' -> type.
%mode +{X1:nat} +{X2:etree} +{X3:nat} +{X4:etree} +{Ea:{x:exp} isvar x -> exp^ X1 X2}
   +{Ea':{x:exp} isvar x -> exp^ X3 X4} +{Eb:exp^ (s X1) X2}
   +{Eb':exp^ (s X3) X4} +{I1:{v:exp} {iv:isvar v} id-exp^ (Ea v iv) (Ea' v iv)}
   +{B1:bind ([v:exp] [x:isvar v] Ea v x) Eb}
   +{B2:bind ([v:exp] [x:isvar v] Ea' v x) Eb'} -{I2:id-exp^ Eb Eb'}
   (bind-uniq I1 B1 B2 I2).
unbind-uniq :
   {X1:nat} {X2:etree} {X3:nat} {X4:etree} {Ea:exp^ (s X1) X2}
      {Ea':exp^ (s X3) X4} {Eb:{x:exp} isvar x -> exp^ X1 X2}
      {Eb':{x:exp} isvar x -> exp^ X3 X4}
      id-exp^ Ea Ea' -> unbind Ea ([v:exp] [x:isvar v] Eb v x)
         -> unbind Ea' ([v:exp] [x:isvar v] Eb' v x)
         -> ({v:exp} {iv:isvar v} id-exp^ (Eb v iv) (Eb' v iv)) -> type.
%mode +{X1:nat} +{X2:etree} +{X3:nat} +{X4:etree} +{Ea:exp^ (s X1) X2}
   +{Ea':exp^ (s X3) X4} +{Eb:{x:exp} isvar x -> exp^ X1 X2}
   +{Eb':{x:exp} isvar x -> exp^ X3 X4} +{I1:id-exp^ Ea Ea'}
   +{U1:unbind Ea ([v:exp] [x:isvar v] Eb v x)}
   +{U2:unbind Ea' ([v:exp] [x:isvar v] Eb' v x)}
   -{I2:{v:exp} {iv:isvar v} id-exp^ (Eb v iv) (Eb' v iv)}
   (unbind-uniq I1 U1 U2 I2).
bind-unbind :
   {X1:nat} {X2:etree} {E^:{x:exp} isvar x -> exp^ X1 X2} {E^':exp^ (s X1) X2}
      bind ([v:exp] [x:isvar v] E^ v x) E^'
         -> unbind E^' ([v:exp] [x:isvar v] E^ v x) -> type.
%mode +{X1:nat} +{X2:etree} +{E^:{x:exp} isvar x -> exp^ X1 X2} +{E^':exp^ (s X1) X2}
   +{B:bind ([v:exp] [x:isvar v] E^ v x) E^'}
   -{U:unbind E^' ([v:exp] [x:isvar v] E^ v x)} (bind-unbind B U).
unbind-bind :
   {X1:nat} {X2:etree} {E^:exp^ (s X1) X2} {E^':{x:exp} isvar x -> exp^ X1 X2}
      unbind E^ ([v:exp] [x:isvar v] E^' v x)
         -> bind ([v:exp] [x:isvar v] E^' v x) E^ -> type.
%mode +{X1:nat} +{X2:etree} +{E^:exp^ (s X1) X2} +{E^':{x:exp} isvar x -> exp^ X1 X2}
   +{U:unbind E^ ([v:exp] [x:isvar v] E^' v x)}
   -{B:bind ([v:exp] [x:isvar v] E^' v x) E^} (unbind-bind U B).
- :
   {X1:nat} {X2:exp} {X3:isvar X2}
      bind-uniq ([v:exp] [iv:isvar v] id-exp^/refl) bind/fvar bind/fvar
         id-exp^/refl.
- :
   {X1:nat} {X2:nat} {X3:lt X1 (s X2)} {X4:lt X1 (s X2)} {ID+:id-lt X3 X4}
      {ID:id-exp^ (bvar^ X1 X3) (bvar^ X1 X4)} {X5:lt X1 X2} {LT+:lt+ X5 X3}
      {LT+':lt+ X5 X4}
      id-bvar^-cong id-nat/refl ID+ ID -> lt+-uniq id-lt/refl LT+ LT+' ID+
         -> bind-uniq ([v:exp] [iv:isvar v] id-exp^/refl) (bind/bvar LT+)
               (bind/bvar LT+') ID.
- :
   {X1:nat} {X2:lt X1 (s X1)} {X3:lt X1 (s X1)} {IDS:id-lt X2 X3}
      {ID:id-exp^ (bvar^ X1 X2) (bvar^ X1 X3)} {LTS:lts X1 X2} {LTS':lts X1 X3}
      id-bvar^-cong id-nat/refl IDS ID -> lts-uniq id-nat/refl LTS LTS' IDS
         -> bind-uniq ([v:exp] [iv:isvar v] id-exp^/refl) (bind/match LTS)
               (bind/match LTS') ID.
- :
   {X1:nat} {X2:etree} {X3:exp^ (s X1) X2} {X4:exp^ (s X1) X2} {X5:etree}
      {X6:exp^ (s X1) X5} {X7:exp^ (s X1) X5} {ID1:id-exp^ X3 X4}
      {ID2:id-exp^ X6 X7} {ID:id-exp^ (app^ X3 X6) (app^ X4 X7)}
      {X8:{v:exp} isvar v -> exp^ X1 X5}
      {F2:bind ([v:exp] [x:isvar v] X8 v x) X6}
      {F2':bind ([v:exp] [x:isvar v] X8 v x) X7}
      {X9:{v:exp} isvar v -> exp^ X1 X2}
      {F1:bind ([v:exp] [x:isvar v] X9 v x) X3}
      {F1':bind ([v:exp] [x:isvar v] X9 v x) X4}
      id-app^-cong ID1 ID2 ID
         -> bind-uniq ([v:exp] [iv:isvar v] id-exp^/refl) F2 F2' ID2
         -> bind-uniq ([v:exp] [iv:isvar v] id-exp^/refl) F1 F1' ID1
         -> bind-uniq ([v:exp] [iv:isvar v] id-exp^/refl) (bind/app F2 F1)
               (bind/app F2' F1') ID.
- :
   {X1:nat} {X2:etree} {X3:exp^ (s (s X1)) X2} {X4:exp^ (s (s X1)) X2}
      {ID1:id-exp^ X3 X4} {ID:id-exp^ (lam^ X3) (lam^ X4)}
      {X5:{v:exp} isvar v -> exp^ (s X1) X2}
      {F1:bind ([v:exp] [x:isvar v] X5 v x) X3}
      {F1':bind ([v:exp] [x:isvar v] X5 v x) X4}
      id-lam^-cong ID1 ID
         -> bind-uniq ([v:exp] [iv:isvar v] id-exp^/refl) F1 F1' ID1
         -> bind-uniq ([v:exp] [iv:isvar v] id-exp^/refl) (bind/lam F1)
               (bind/lam F1') ID.
%worlds (blockvar) (bind-uniq _ _ _ _).
%total T (bind-uniq _ T _ _).
lem :
   {N:nat} {Et:etree} {Eb:{v:exp} isvar v -> exp^ N Et}
      {Eb':{v:exp} isvar v -> exp^ N Et}
      uninhabited -> ({v:exp} {iv:isvar v} id-exp^ (Eb v iv) (Eb' v iv)) -> type.
%mode +{N:nat} +{Et:etree} +{Eb:{v:exp} isvar v -> exp^ N Et}
   +{Eb':{v:exp} isvar v -> exp^ N Et} +{X:uninhabited}
   -{D:{v:exp} {iv:isvar v} id-exp^ (Eb v iv) (Eb' v iv)} (lem Eb Eb' X D).
%worlds (blockvar) (lem _ _ _ _).
%total {} (lem _ _ _ _).
- :
   {X1:nat} {X2:exp} {X3:isvar X2}
      unbind-uniq id-exp^/refl unbind/fvar unbind/fvar
         ([v:exp] [iv:isvar v] id-exp^/refl).
- :
   {X1:nat} {X2:lt X1 X1} {X:uninhabited}
      {ID:{x:exp} {x1:isvar x} id-exp^ (fvar^ x x1) (bvar^ X1 X2)}
      {X3:lt X1 (s X1)} {A:lt-opt X3 lt12/1} {B:lt-opt X3 (lt12/2 X2)}
      lem ([v:exp] [x:isvar v] fvar^ v x) ([v:exp] [x:isvar v] bvar^ X1 X2) X
         ([v:exp] [iv:isvar v] ID v iv)
         -> lt-opt-excl A B X
         -> unbind-uniq id-exp^/refl (unbind/bvar unbind-bvar/match A)
               (unbind/bvar unbind-bvar/nomatch B)
               ([v:exp] [iv:isvar v] ID v iv).
- :
   {X1:nat} {X2:lt X1 X1} {X:uninhabited}
      {ID:{x:exp} {x1:isvar x} id-exp^ (bvar^ X1 X2) (fvar^ x x1)}
      {X3:lt X1 (s X1)} {B:lt-opt X3 lt12/1} {A:lt-opt X3 (lt12/2 X2)}
      lem ([v:exp] [x:isvar v] bvar^ X1 X2) ([v:exp] [x:isvar v] fvar^ v x) X
         ([v:exp] [iv:isvar v] ID v iv)
         -> lt-opt-excl B A X
         -> unbind-uniq id-exp^/refl (unbind/bvar unbind-bvar/nomatch A)
               (unbind/bvar unbind-bvar/match B) ([v:exp] [iv:isvar v] ID v iv).
- :
   {X1:nat} {X2:lt X1 (s X1)} {A:lt-opt X2 lt12/1} {B:lt-opt X2 lt12/1}
      unbind-uniq id-exp^/refl (unbind/bvar unbind-bvar/match A)
         (unbind/bvar unbind-bvar/match B) ([v:exp] [iv:isvar v] id-exp^/refl).
- :
   {X1:nat} {X2:nat} {LT2:lt X1 X2} {LT2':lt X1 X2} {ID1:id-lt LT2 LT2'}
      {ID:{x:exp} isvar x -> id-exp^ (bvar^ X1 LT2) (bvar^ X1 LT2')}
      {LT:lt X1 (s X2)} {Opt1:lt-opt LT (lt12/2 LT2)}
      {Opt2:lt-opt LT (lt12/2 LT2')}
      ({v:exp} {iv:isvar v} id-bvar^-cong id-nat/refl ID1 (ID v iv))
         -> lt-opt2-uniq id-lt/refl Opt1 Opt2 ID1
         -> unbind-uniq id-exp^/refl (unbind/bvar unbind-bvar/nomatch Opt1)
               (unbind/bvar unbind-bvar/nomatch Opt2)
               ([v:exp] [iv:isvar v] ID v iv).
- :
   {X1:nat} {X2:etree} {X3:{x:exp} isvar x -> exp^ X1 X2}
      {X4:{x:exp} isvar x -> exp^ X1 X2} {X5:etree}
      {X6:{x:exp} isvar x -> exp^ X1 X5} {X7:{x:exp} isvar x -> exp^ X1 X5}
      {ID1:{x:exp} {x1:isvar x} id-exp^ (X3 x x1) (X4 x x1)}
      {ID2:{x:exp} {x1:isvar x} id-exp^ (X6 x x1) (X7 x x1)}
      {ID:{x:exp} {x1:isvar x}
             id-exp^ (app^ (X3 x x1) (X6 x x1)) (app^ (X4 x x1) (X7 x x1))}
      {X8:exp^ (s X1) X5} {E2:unbind X8 ([v:exp] [x:isvar v] X6 v x)}
      {E2':unbind X8 ([v:exp] [x:isvar v] X7 v x)} {X9:exp^ (s X1) X2}
      {E1:unbind X9 ([v:exp] [x:isvar v] X3 v x)}
      {E1':unbind X9 ([v:exp] [x:isvar v] X4 v x)}
      ({v:exp} {iv:isvar v} id-app^-cong (ID1 v iv) (ID2 v iv) (ID v iv))
         -> unbind-uniq id-exp^/refl E2 E2' ([v:exp] [iv:isvar v] ID2 v iv)
         -> unbind-uniq id-exp^/refl E1 E1' ([v:exp] [iv:isvar v] ID1 v iv)
         -> unbind-uniq id-exp^/refl (unbind/app E2 E1) (unbind/app E2' E1')
               ([v:exp] [iv:isvar v] ID v iv).
- :
   {X1:nat} {X2:etree} {X3:{x:exp} isvar x -> exp^ (s X1) X2}
      {X4:{x:exp} isvar x -> exp^ (s X1) X2}
      {ID1:{x:exp} {x1:isvar x} id-exp^ (X3 x x1) (X4 x x1)}
      {ID:{x:exp} {x1:isvar x} id-exp^ (lam^ (X3 x x1)) (lam^ (X4 x x1))}
      {X5:exp^ (s (s X1)) X2} {E:unbind X5 ([v:exp] [x:isvar v] X3 v x)}
      {E':unbind X5 ([v:exp] [x:isvar v] X4 v x)}
      ({v:exp} {iv:isvar v} id-lam^-cong (ID1 v iv) (ID v iv))
         -> unbind-uniq id-exp^/refl E E' ([v:exp] [iv:isvar v] ID1 v iv)
         -> unbind-uniq id-exp^/refl (unbind/lam E) (unbind/lam E')
               ([v:exp] [iv:isvar v] ID v iv).
%worlds (blockvar) (unbind-uniq _ _ _ _).
%total T (unbind-uniq _ T _ _).
- : {X1:nat} {X2:exp} {X3:isvar X2} bind-unbind bind/fvar unbind/fvar.
- :
   {N:nat} {LT:lt N (s N)} {Opt:lt-opt LT lt12/1} {LTS:lts N LT}
      lt-opt-succ1 LT Opt
         -> bind-unbind (bind/match LTS) (unbind/bvar unbind-bvar/match Opt).
- :
   {X1:nat} {X2:nat} {LT:lt X1 X2} {LT':lt X1 (s X2)} {LT+:lt+ LT LT'}
      {Opt:lt-opt LT' (lt12/2 LT)}
      lt-opt-succ2 LT+ Opt
         -> bind-unbind (bind/bvar LT+) (unbind/bvar unbind-bvar/nomatch Opt).
- :
   {X1:nat} {X2:etree} {X3:{v:exp} isvar v -> exp^ X1 X2} {X4:exp^ (s X1) X2}
      {B2:bind ([v:exp] [x:isvar v] X3 v x) X4}
      {U2:unbind X4 ([v:exp] [x:isvar v] X3 v x)} {X5:etree}
      {X6:{v:exp} isvar v -> exp^ X1 X5} {X7:exp^ (s X1) X5}
      {B1:bind ([v:exp] [x:isvar v] X6 v x) X7}
      {U1:unbind X7 ([v:exp] [x:isvar v] X6 v x)}
      bind-unbind B2 U2 -> bind-unbind B1 U1
         -> bind-unbind (bind/app B2 B1) (unbind/app U2 U1).
- :
   {X1:nat} {X2:etree} {X3:{v:exp} isvar v -> exp^ (s X1) X2}
      {X4:exp^ (s (s X1)) X2} {B:bind ([v:exp] [x:isvar v] X3 v x) X4}
      {U:unbind X4 ([v:exp] [x:isvar v] X3 v x)}
      bind-unbind B U -> bind-unbind (bind/lam B) (unbind/lam U).
%worlds (blockvar) (bind-unbind _ _).
%total T (bind-unbind T _).
- : {X1:nat} {X2:exp} {X3:isvar X2} unbind-bind unbind/fvar bind/fvar.
- :
   {X1:nat} {X2:lt X1 (s X1)} {LTS:lts X1 X2} {Opt:lt-opt X2 lt12/1}
      can-lts X1 X2 LTS
         -> unbind-bind (unbind/bvar unbind-bvar/match Opt) (bind/match LTS).
- :
   {X1:nat} {X2:nat} {LT:lt X1 X2} {LT':lt X1 (s X2)} {LT+:lt+ LT LT'}
      {Opt:lt-opt LT' (lt12/2 LT)}
      can-lt+ LT LT' LT+
         -> unbind-bind (unbind/bvar unbind-bvar/nomatch Opt) (bind/bvar LT+).
- :
   {X1:nat} {X2:etree} {X3:exp^ (s X1) X2} {X4:{v:exp} isvar v -> exp^ X1 X2}
      {U2:unbind X3 ([v:exp] [x:isvar v] X4 v x)}
      {B2:bind ([v:exp] [x:isvar v] X4 v x) X3} {X5:etree} {X6:exp^ (s X1) X5}
      {X7:{v:exp} isvar v -> exp^ X1 X5}
      {U1:unbind X6 ([v:exp] [x:isvar v] X7 v x)}
      {B1:bind ([v:exp] [x:isvar v] X7 v x) X6}
      unbind-bind U2 B2 -> unbind-bind U1 B1
         -> unbind-bind (unbind/app U2 U1) (bind/app B2 B1).
- :
   {X1:nat} {X2:etree} {X3:exp^ (s (s X1)) X2}
      {X4:{v:exp} isvar v -> exp^ (s X1) X2}
      {U:unbind X3 ([v:exp] [x:isvar v] X4 v x)}
      {B:bind ([v:exp] [x:isvar v] X4 v x) X3}
      unbind-bind U B -> unbind-bind (unbind/lam U) (bind/lam B).
%worlds (blockvar) (unbind-bind _ _).
%total T (unbind-bind T _).
exp->db : {E:exp} case E -> ({Et:etree} exp^ z Et -> type).
%mode +{E:exp} +{C:case E} -{Et:etree} -{E^:exp^ z Et} (exp->db E C Et E^).
exp->db/var :
   {V:exp} {IV:isvar V} exp->db V (case/var IV) etree/var (fvar^ V IV).
exp->db/lam :
   {Et:etree} {E^'':{x:exp} isvar x -> exp^ z Et} {E^':exp^ (s z) Et}
      {E2:exp -> exp} {CASE:{x:exp} isvar x -> case (E2 x)}
      bind ([v:exp] [x:isvar v] E^'' v x) E^'
         -> ({v:exp} {iv:isvar v}
                can-case v (case/var iv)
                   -> exp->db (E2 v) (CASE v iv) Et (E^'' v iv))
         -> ({v:exp} {iv:isvar v}
                can-case v (case/var iv) -> can-case (E2 v) (CASE v iv))
         -> exp->db (lam ([v:exp] E2 v)) case/lam (etree/lam Et) (lam^ E^').
exp->db/app :
   {E2:exp} {CASE2:case E2} {Et2:etree} {E2':exp^ z Et2} {E1:exp}
      {CASE1:case E1} {Et1:etree} {E1':exp^ z Et1}
      exp->db E2 CASE2 Et2 E2' -> exp->db E1 CASE1 Et1 E1' -> can-case E2 CASE2
         -> can-case E1 CASE1
         -> exp->db (app E1 E2) case/app (etree/app Et1 Et2) (app^ E1' E2').
%worlds (blockcases) (exp->db _ _ _ _).
%total T (exp->db T _ _ _).
uniq->db :
   {E2:exp} {C:case E2} {Et:etree} {E^:exp^ z Et} {Et':etree} {E^':exp^ z Et'}
      exp->db E2 C Et E^ -> exp->db E2 C Et' E^' -> id-etree Et Et'
         -> id-exp^ E^ E^' -> type.
%mode +{E2:exp} +{C:case E2} +{Et:etree} +{E^:exp^ z Et} +{Et':etree}
   +{E^':exp^ z Et'} +{E1:exp->db E2 C Et E^} +{E3:exp->db E2 C Et' E^'}
   -{ID1:id-etree Et Et'} -{ID2:id-exp^ E^ E^'} (uniq->db E1 E3 ID1 ID2).
- :
   {X1:exp} {X2:isvar X1}
      uniq->db exp->db/var exp->db/var id-etree/refl id-exp^/refl.
- :
   {X1:etree} {X2:etree} {X3:exp^ (s z) X1} {X4:exp^ (s z) X2}
      {ID^2:id-exp^ X3 X4} {ID^:id-exp^ (lam^ X3) (lam^ X4)}
      {IDe1:id-etree X1 X2} {IDe:id-etree (etree/lam X1) (etree/lam X2)}
      {X5:{v:exp} isvar v -> exp^ z X1} {X6:{v:exp} isvar v -> exp^ z X2}
      {ID^1:{x:exp} {x1:isvar x} id-exp^ (X5 x x1) (X6 x x1)}
      {F:bind ([v:exp] [x:isvar v] X5 v x) X3}
      {F':bind ([v:exp] [x:isvar v] X6 v x) X4} {X7:exp -> exp}
      {X8:{x:exp} isvar x -> case (X7 x)}
      {T:{x:exp} {x1:isvar x}
            can-case x (case/var x1) -> exp->db (X7 x) (X8 x x1) X1 (X5 x x1)}
      {T':{x:exp} {x1:isvar x}
             can-case x (case/var x1) -> exp->db (X7 x) (X8 x x1) X2 (X6 x x1)}
      {C:{x:exp} {x1:isvar x}
            can-case x (case/var x1) -> can-case (X7 x) (X8 x x1)}
      {C':{x:exp} {x1:isvar x}
             can-case x (case/var x1) -> can-case (X7 x) (X8 x x1)}
      id-lam^-cong ID^2 ID^ -> id-etree/lam-cong IDe1 IDe
         -> bind-uniq ([v:exp] [iv:isvar v] ID^1 v iv) F F' ID^2
         -> ({v:exp} {iv:isvar v} {c:can-case v (case/var iv)}
                uniq->db (T v iv c) (T' v iv c) IDe1 (ID^1 v iv))
         -> uniq->db
               (exp->db/lam F
                   ([v:exp] [iv:isvar v] [x:can-case v (case/var iv)] T v iv x)
                   ([v:exp] [iv:isvar v] [x:can-case v (case/var iv)] C v iv x))
               (exp->db/lam F'
                   ([v:exp] [iv:isvar v] [x:can-case v (case/var iv)] T' v iv x)
                   ([v:exp] [iv:isvar v] [x:can-case v (case/var iv)] C' v iv x))
               IDe ID^.
- :
   {X1:etree} {X2:etree} {X3:exp^ z X1} {X4:exp^ z X2} {X5:etree} {X6:etree}
      {X7:exp^ z X5} {X8:exp^ z X6} {ID^1:id-exp^ X3 X4} {ID^2:id-exp^ X7 X8}
      {ID^:id-exp^ (app^ X3 X7) (app^ X4 X8)} {IDe1:id-etree X1 X2}
      {IDe2:id-etree X5 X6} {IDe:id-etree (etree/app X1 X5) (etree/app X2 X6)}
      {X9:exp} {X10:case X9} {T2:exp->db X9 X10 X5 X7}
      {T2':exp->db X9 X10 X6 X8} {X11:exp} {X12:case X11}
      {T1:exp->db X11 X12 X1 X3} {T1':exp->db X11 X12 X2 X4}
      {C2:can-case X9 X10} {C1:can-case X11 X12} {C2':can-case X9 X10}
      {C1':can-case X11 X12}
      id-app^-cong ID^1 ID^2 ID^ -> id-etree/app-cong IDe1 IDe2 IDe
         -> uniq->db T2 T2' IDe2 ID^2 -> uniq->db T1 T1' IDe1 ID^1
         -> uniq->db (exp->db/app T2 T1 C2 C1) (exp->db/app T2' T1' C2' C1') IDe
               ID^.
%worlds (blockcases) (uniq->db _ _ _ _).
%total T (uniq->db T _ _ _).
db->exp : {Et:etree} exp^ z Et -> ({E:exp} case E -> type).
%mode +{ET:etree} +{E^:exp^ z ET} -{E:exp} -{C:case E} (db->exp ET E^ E C).
db->exp/fvar :
   {V:exp} {IV:isvar V} db->exp etree/var (fvar^ V IV) V (case/var IV).
db->exp/lam :
   {ET:etree} {E^':{x:exp} isvar x -> exp^ z ET} {E:exp -> exp}
      {X1:{v:exp} isvar v -> case (E v)} {E^:exp^ (s z) ET}
      ({v:exp} {iv:isvar v}
          can-case v (case/var iv) -> db->exp ET (E^' v iv) (E v) (X1 v iv))
         -> unbind E^ ([v:exp] [x:isvar v] E^' v x)
         -> db->exp (etree/lam ET) (lam^ E^) (lam ([x:exp] E x)) case/lam.
db->exp/app :
   {ET2:etree} {E2^:exp^ z ET2} {E2:exp} {X1:case E2} {ET1:etree}
      {E1^:exp^ z ET1} {E1:exp} {X2:case E1}
      db->exp ET2 E2^ E2 X1 -> db->exp ET1 E1^ E1 X2
         -> db->exp (etree/app ET1 ET2) (app^ E1^ E2^) (app E1 E2) case/app.
%worlds (blockcases) (db->exp _ _ _ _).
%total T (db->exp T _ _ _).
uniq->exp :
   {ET:etree} {ET':etree} {E^:exp^ z ET} {E^':exp^ z ET'} {E:exp} {C:case E}
      {E':exp} {C':case E'}
      id-exp^ E^ E^' -> db->exp ET E^ E C -> db->exp ET' E^' E' C'
         -> id-exp E E' -> type.
%mode +{ET:etree} +{ET':etree} +{E^:exp^ z ET} +{E^':exp^ z ET'} +{E:exp} +{C:case E}
   +{E':exp} +{C':case E'} +{ID1:id-exp^ E^ E^'} +{E1:db->exp ET E^ E C}
   +{E2:db->exp ET' E^' E' C'} -{ID:id-exp E E'} (uniq->exp ID1 E1 E2 ID).
- :
   {X1:exp} {X2:isvar X1}
      uniq->exp id-exp^/refl db->exp/fvar db->exp/fvar id-exp/refl.
- :
   {X1:exp -> exp} {X2:exp -> exp} {ID2:{x:exp} id-exp (X1 x) (X2 x)}
      {ID:id-exp (lam ([x:exp] X1 x)) (lam ([x:exp] X2 x))} {X3:etree}
      {E:{x:exp} isvar x -> exp^ z X3} {E':{x:exp} isvar x -> exp^ z X3}
      {X4:{x:exp} isvar x -> case (X1 x)} {X5:{x:exp} isvar x -> case (X2 x)}
      {ID1:{x:exp} {x1:isvar x} id-exp^ (E x x1) (E' x x1)}
      {T:{x:exp} {x1:isvar x}
            can-case x (case/var x1) -> db->exp X3 (E x x1) (X1 x) (X4 x x1)}
      {T':{x:exp} {x1:isvar x}
             can-case x (case/var x1) -> db->exp X3 (E' x x1) (X2 x) (X5 x x1)}
      {X6:exp^ (s z) X3} {UB:unbind X6 ([v:exp] [x:isvar v] E v x)}
      {UB':unbind X6 ([v:exp] [x:isvar v] E' v x)}
      id-lam-cong ([v:exp] ID2 v) ID
         -> ({v:exp} {iv:isvar v} {c:can-case v (case/var iv)}
                uniq->exp (ID1 v iv) (T v iv c) (T' v iv c) (ID2 v))
         -> unbind-uniq id-exp^/refl UB UB' ([v:exp] [iv:isvar v] ID1 v iv)
         -> uniq->exp id-exp^/refl
               (db->exp/lam
                   ([v:exp] [iv:isvar v] [c:can-case v (case/var iv)] T v iv c)
                   UB)
               (db->exp/lam
                   ([v:exp] [iv:isvar v] [c:can-case v (case/var iv)] T' v iv c)
                   UB')
               ID.
- :
   {X1:exp} {X2:exp} {X3:exp} {X4:exp} {ID1:id-exp X1 X2} {ID2:id-exp X3 X4}
      {ID:id-exp (app X1 X3) (app X2 X4)} {X5:etree} {X6:exp^ z X5} {X7:case X3}
      {X8:case X4} {T2:db->exp X5 X6 X3 X7} {T2':db->exp X5 X6 X4 X8} {X9:etree}
      {X10:exp^ z X9} {X11:case X1} {X12:case X2} {T1:db->exp X9 X10 X1 X11}
      {T1':db->exp X9 X10 X2 X12}
      id-app-cong ID1 ID2 ID -> uniq->exp id-exp^/refl T2 T2' ID2
         -> uniq->exp id-exp^/refl T1 T1' ID1
         -> uniq->exp id-exp^/refl (db->exp/app T2 T1) (db->exp/app T2' T1') ID.
%worlds (blockcases) (uniq->exp _ _ _ _).
%total T (uniq->exp _ T _ _).
inverseEDE :
   {E:exp} {C:case E} {Et:etree} {E^:exp^ z Et}
      exp->db E C Et E^ -> db->exp Et E^ E C -> type.
%mode +{E:exp} +{C:case E} +{Et:etree} +{E^:exp^ z Et} +{ED:exp->db E C Et E^}
   -{DE:db->exp Et E^ E C} (inverseEDE ED DE).
- : {X1:exp} {X2:isvar X1} inverseEDE exp->db/var db->exp/fvar.
- :
   {X1:exp -> exp} {X2:{x:exp} isvar x -> case (X1 x)} {X3:etree}
      {X4:{x:exp} isvar x -> exp^ z X3}
      {T:{x:exp} {x1:isvar x}
            can-case x (case/var x1) -> exp->db (X1 x) (X2 x x1) X3 (X4 x x1)}
      {T':{x:exp} {x1:isvar x}
             can-case x (case/var x1) -> db->exp X3 (X4 x x1) (X1 x) (X2 x x1)}
      {X5:exp^ (s z) X3} {B:bind ([v:exp] [x:isvar v] X4 v x) X5}
      {U:unbind X5 ([v:exp] [x:isvar v] X4 v x)}
      {C:{x:exp} {x1:isvar x}
            can-case x (case/var x1) -> can-case (X1 x) (X2 x x1)}
      ({v:exp} {iv:isvar v} {c:can-case v (case/var iv)}
          inverseEDE (T v iv c) (T' v iv c)) -> bind-unbind B U
         -> inverseEDE
               (exp->db/lam B
                   ([v:exp] [iv:isvar v] [x:can-case v (case/var iv)] T v iv x)
                   ([v:exp] [iv:isvar v] [x:can-case v (case/var iv)] C v iv x))
               (db->exp/lam
                   ([v:exp] [iv:isvar v] [x:can-case v (case/var iv)] T' v iv x)
                   U).
- :
   {X1:exp} {X2:case X1} {X3:etree} {X4:exp^ z X3} {T2:exp->db X1 X2 X3 X4}
      {T2':db->exp X3 X4 X1 X2} {X5:exp} {X6:case X5} {X7:etree} {X8:exp^ z X7}
      {T1:exp->db X5 X6 X7 X8} {T1':db->exp X7 X8 X5 X6} {C2:can-case X1 X2}
      {C1:can-case X5 X6}
      inverseEDE T2 T2' -> inverseEDE T1 T1'
         -> inverseEDE (exp->db/app T2 T1 C2 C1) (db->exp/app T2' T1').
%worlds (blockcases) (inverseEDE _ _).
%total T (inverseEDE T _).
can-can-case : {E:exp} {C:case E} can-case E C -> type.
fake : type.
- :
   {X1:exp} {E:case X1} {V:can-case X1 E} {X2:exp} {E':case X2}
      {V':can-case X2 E'} (can-can-case E V -> can-can-case E' V') -> fake.
%block blockcancases : block {v:exp} {iv:isvar v} {c:can-case v (case/var iv)}
   {cc:can-can-case (case/var iv) c}.
- : {X1:exp} {X2:exp} can-can-case case/app can-case/app.
- : {X1:exp -> exp} can-can-case case/lam can-case/lam.
%mode +{E:exp} +{C:case E} -{CC:can-case E C} (can-can-case C CC).
%worlds (blockcancases) (can-can-case _ _).
%total {} (can-can-case _ _).
inverseDED :
   {Et:etree} {E^:exp^ z Et} {E:exp} {C:case E}
      db->exp Et E^ E C -> exp->db E C Et E^ -> type.
%mode +{Et:etree} +{E^:exp^ z Et} +{E:exp} +{C:case E} +{DE:db->exp Et E^ E C}
   -{ED:exp->db E C Et E^} (inverseDED DE ED).
- : {X1:exp} {X2:isvar X1} inverseDED db->exp/fvar exp->db/var.
- :
   {E:exp -> exp} {Case:{x:exp} isvar x -> case (E x)}
      {C:{x:exp} {x1:isvar x}
            can-case x (case/var x1) -> can-case (E x) (Case x x1)} {Et:etree}
      {E^:{x:exp} isvar x -> exp^ z Et}
      {T:{x:exp} {x1:isvar x}
            can-case x (case/var x1) -> db->exp Et (E^ x x1) (E x) (Case x x1)}
      {T':{x:exp} {x1:isvar x}
             can-case x (case/var x1) -> exp->db (E x) (Case x x1) Et (E^ x x1)}
      {X1:exp^ (s z) Et} {U:unbind X1 ([v:exp] [x:isvar v] E^ v x)}
      {B:bind ([v:exp] [x:isvar v] E^ v x) X1}
      ({v:exp} {iv:isvar v} {c:can-case v (case/var iv)}
          can-can-case (case/var iv) c -> can-can-case (Case v iv) (C v iv c))
         -> ({v:exp} {iv:isvar v} {c:can-case v (case/var iv)}
                can-can-case (case/var iv) c
                   -> inverseDED (T v iv c) (T' v iv c))
         -> unbind-bind U B
         -> inverseDED
               (db->exp/lam
                   ([v:exp] [iv:isvar v] [x:can-case v (case/var iv)] T v iv x)
                   U)
               (exp->db/lam B
                   ([v:exp] [iv:isvar v] [x:can-case v (case/var iv)] T' v iv x)
                   ([v:exp] [iv:isvar v] [x:can-case v (case/var iv)] C v iv x)).
- :
   {X1:exp} {X2:case X1} {C2:can-case X1 X2} {X3:exp} {X4:case X3}
      {C1:can-case X3 X4} {X5:etree} {X6:exp^ z X5} {T2:db->exp X5 X6 X1 X2}
      {T2':exp->db X1 X2 X5 X6} {X7:etree} {X8:exp^ z X7}
      {T1:db->exp X7 X8 X3 X4} {T1':exp->db X3 X4 X7 X8}
      can-can-case X2 C2 -> can-can-case X4 C1 -> inverseDED T2 T2'
         -> inverseDED T1 T1'
         -> inverseDED (db->exp/app T2 T1) (exp->db/app T2' T1' C2 C1).
%worlds (blockcancases) (inverseDED _ _).
%total T (inverseDED T _).
exp-->db : {Et:etree} exp -> exp^ z Et -> type.
exp-->db/ :
   {E:exp} {C:case E} {Et:etree} {E^:exp^ z Et}
      exp->db E C Et E^ -> can-case E C -> exp-->db E E^.
%mode -{Et:etree} +{E:exp} -{E^:exp^ z Et} (exp-->db E E^).
%worlds () (exp-->db _ _).
%total {} (exp-->db _ _).
uniq-->db :
   {X1:etree} {E:exp} {E1:exp^ z X1} {X2:etree} {E2:exp^ z X2}
      exp-->db E E1 -> exp-->db E E2 -> id-exp^ E1 E2 -> type.
- :
   {X1:exp} {X2:case X1} {X3:etree} {X4:exp^ z X3} {X5:etree} {X6:exp^ z X5}
      {ED:exp->db X1 X2 X3 X4} {ED':exp->db X1 X2 X5 X6} {X7:id-etree X3 X5}
      {ID:id-exp^ X4 X6} {C:can-case X1 X2} {C':can-case X1 X2}
      uniq->db ED ED' X7 ID -> uniq-->db (exp-->db/ ED C) (exp-->db/ ED' C') ID.
%mode +{X1:etree} +{E:exp} +{E1:exp^ z X1} +{X2:etree} +{E2:exp^ z X2}
   +{E3:exp-->db E E1} +{E':exp-->db E E2} -{ID:id-exp^ E1 E2}
   (uniq-->db E3 E' ID).
%worlds () (uniq-->db _ _ _).
%total {} (uniq-->db _ _ _).
db-->exp : {Et:etree} exp^ z Et -> exp -> type.
db-->exp/ :
   {Et:etree} {E^:exp^ z Et} {E:exp} {X1:case E}
      db->exp Et E^ E X1 -> db-->exp E^ E.
%mode +{Et:etree} +{E^:exp^ z Et} -{E:exp} (db-->exp E^ E).
%worlds () (db-->exp _ _).
%total {} (db-->exp _ _).
uniq-->exp :
   {X1:etree} {E:exp^ z X1} {E1:exp} {E2:exp}
      db-->exp E E1 -> db-->exp E E2 -> id-exp E1 E2 -> type.
- :
   {X1:etree} {X2:exp^ z X1} {X3:exp} {X4:case X3} {X5:exp} {X6:case X5}
      {DE:db->exp X1 X2 X3 X4} {DE':db->exp X1 X2 X5 X6} {ID:id-exp X3 X5}
      uniq->exp id-exp^/refl DE DE' ID
         -> uniq-->exp (db-->exp/ DE) (db-->exp/ DE') ID.
%mode +{X1:etree} +{E:exp^ z X1} +{E1:exp} +{E2:exp} +{E3:db-->exp E E1}
   +{E':db-->exp E E2} -{ID:id-exp E1 E2} (uniq-->exp E3 E' ID).
%worlds () (uniq-->exp _ _ _).
%total {} (uniq-->exp _ _ _).
db-->exp-->db :
   {X1:etree} {E^:exp^ z X1} {E:exp} db-->exp E^ E -> exp-->db E E^ -> type.
- :
   {E:exp} {Case:case E} {C:can-case E Case} {Et:etree} {E^:exp^ z Et}
      {DE:db->exp Et E^ E Case} {ED:exp->db E Case Et E^}
      can-can-case Case C -> inverseDED DE ED
         -> db-->exp-->db (db-->exp/ DE) (exp-->db/ ED C).
%mode +{X1:etree} +{E^:exp^ z X1} +{E:exp} +{DE:db-->exp E^ E} -{ED:exp-->db E E^}
   (db-->exp-->db DE ED).
%worlds () (db-->exp-->db _ _).
%total {} (db-->exp-->db _ _).
exp-->db-->exp :
   {X1:etree} {E:exp} {E^:exp^ z X1} exp-->db E E^ -> db-->exp E^ E -> type.
- :
   {X1:exp} {X2:case X1} {X3:etree} {X4:exp^ z X3} {ED:exp->db X1 X2 X3 X4}
      {DE:db->exp X3 X4 X1 X2} {C:can-case X1 X2}
      inverseEDE ED DE -> exp-->db-->exp (exp-->db/ ED C) (db-->exp/ DE).
%mode +{X1:etree} +{E:exp} +{E^:exp^ z X1} +{ED:exp-->db E E^} -{DE:db-->exp E^ E}
   (exp-->db-->exp ED DE).
%worlds () (exp-->db-->exp _ _).
%total {} (exp-->db-->exp _ _).
%query 1 *

exp-->db (lam ([f:exp] lam ([x:exp] app f (app f (app f (app f x)))))) DB.
---------- Solution 1 ----------
DB =
   lam^
      (lam^
          (app^ (bvar^ (s z) (lt/s lt/z))
              (app^ (bvar^ (s z) (lt/s lt/z))
                  (app^ (bvar^ (s z) (lt/s lt/z))
                      (app^ (bvar^ (s z) (lt/s lt/z)) (bvar^ z lt/z)))))).
____________________________________________

%query 1 *

db-->exp
   (lam^
       (app^ (app^ (bvar^ z lt/z) (lam^ (lam^ (bvar^ z lt/z))))
           (lam^ (lam^ (bvar^ (s z) (lt/s lt/z)))))) HOAS.
---------- Solution 1 ----------
HOAS =
   lam
      ([x:exp]
          app (app x (lam ([x1:exp] lam ([x2:exp] x2))))
             (lam ([x1:exp] lam ([x2:exp] x1)))).
____________________________________________

[Closing file /home/www/twelf/hcode/e9fbcbbeec08af49f8ae28cff66db426]
%% OK %%