Pretty amazed that Twelf manages to solve for this monstrous typing derivation

gistfile1.txt

%solve 
ctx/snoc (ctx/snoc ctx/nil (! ↑ unit)) (@ ([x:tm] ! ↑ unit))
   >> judgement/type (@ ([x:tm] @ ([y:tm] ! ↑ unit))).
 OK
- :
   ctx/snoc (ctx/snoc ctx/nil (! ↑ unit)) (@ ([x:tm] ! ↑ unit))
      >> judgement/type (@ ([x:tm] @ ([y:tm] ! ↑ unit)))
   = >>/,
        ([x:tm] [x':otm (ctx/snoc ctx/nil (! ↑ unit))]
            [x1:weaken (ctx/snoc ctx/nil (! ↑ unit)) x x'] [y:tm]
            [y':otm (ctx/snoc ctx/nil (! ↑ unit))]
            [x2:weaken (ctx/snoc ctx/nil (! ↑ unit)) y y']
            [x3:ctx/snoc ctx/nil (! ↑ unit)
                   >> judgement/eq-mem x' y' (@ ([x3:tm] ! ↑ unit))]
            >>/,
               ([x12:tm] [x'4:otm ctx/nil] [x4:weaken ctx/nil x12 x'4] [y5:tm]
                   [y'1:otm ctx/nil] [x5:weaken ctx/nil y5 y'1]
                   [x6:ctx/nil >> judgement/eq-mem x'4 y'1 (! ↑ unit)]
                   >>/·
                      (□/eq-type
                          (eq-type/def
                              (can-eq-type/def
                                  ([x16:val] [x7:can-mem x16 unit] x7)
                                  ([x15:val] [x7:can-mem x15 unit] x7)
                                  ([x14:val] [y7:val]
                                      [x7:can-eq-mem x14 y7 unit] x7)
                                  ([x13:val] [y6:val]
                                      [x7:can-eq-mem x13 y6 unit] x7)) =>/↑
                              =>/↑)))
               ([x7:tm] [x'3:otm ctx/nil] [x4:weaken ctx/nil x7 x'3]
                   [x5:ctx/nil >> judgement/mem x'3 (! ↑ unit)]
                   >>/·
                      (□/eq-type
                          (eq-type/def
                              (can-eq-type/def
                                  ([x11:val] [x6:can-mem x11 unit] x6)
                                  ([x10:val] [x6:can-mem x10 unit] x6)
                                  ([x9:val] [y4:val] [x6:can-eq-mem x9 y4 unit]
                                      x6)
                                  ([x8:val] [y3:val] [x6:can-eq-mem x8 y3 unit]
                                      x6))
                              =>/↑ =>/↑)))
               apply/eq-type stretch/eq-type)
        ([x:tm] [x':otm (ctx/snoc ctx/nil (! ↑ unit))]
            [x1:weaken (ctx/snoc ctx/nil (! ↑ unit)) x x']
            [x2:ctx/snoc ctx/nil (! ↑ unit)
                   >> judgement/mem x' (@ ([x4:tm] ! ↑ unit))]
            >>/,
               ([x5:tm] [x'2:otm ctx/nil] [x3:weaken ctx/nil x5 x'2] [y:tm]
                   [y':otm ctx/nil] [x4:weaken ctx/nil y y']
                   [x6:ctx/nil >> judgement/eq-mem x'2 y' (! ↑ unit)]
                   >>/·
                      (□/eq-type
                          (eq-type/def
                              (can-eq-type/def
                                  ([x7:val] [x8:can-mem x7 unit] x8)
                                  ([x8:val] [x7:can-mem x8 unit] x7)
                                  ([x9:val] [y2:val] [x7:can-eq-mem x9 y2 unit]
                                      x7)
                                  ([x10:val] [y1:val]
                                      [x7:can-eq-mem x10 y1 unit] x7))
                              =>/↑ =>/↑)))
               ([x11:tm] [x'1:otm ctx/nil] [x3:weaken ctx/nil x11 x'1]
                   [x4:ctx/nil >> judgement/mem x'1 (! ↑ unit)]
                   >>/· (□/type (is-type/def can-type/unit =>/↑)))
               apply/type stretch/type)
        apply/type stretch/type.