Output of lowerDict on "p4"

Output.hs

Prog [DDef {tyName = TypeDict,
            kVars = [(a, Star)],
            cVars = [],
            sVars = [],
            cases = [KCons {conName = ArrowTyDict,
                            fields = [ConTy TypeDict [VarTy a],ConTy TypeDict [VarTy b]],
                            outputs = [ConTy ArrowTyDict [VarTy a,VarTy b]]},
                     KCons {conName = IntDict,
                            fields = [],
                            outputs = [ConTy IntDict []]}]},
      DDef {tyName = TyEquality,
            kVars = [(a, Star),(b, Star)],
            cVars = [],
            sVars = [],
            cases = [KCons {conName = Refl,
                            fields = [],
                            outputs = [VarTy a,VarTy a]}]}]
     [VDef {valName = checkTEQ,
            valTy = ForAll []
                           (ArrowTy (ConTy TypeDict [VarTy t])
                                    (ArrowTy (ConTy TypeDict [VarTy u])
                                             (ConTy Maybe [ConTy TyEquality [VarTy t,VarTy u]]))),
            valExp = ELam (x, ConTy TypeDict [VarTy a])
                          (ELam (y, ConTy TypeDict [VarTy b])
                                (ECase (EVar x)
                                       [(Pat ArrowTy [a1,b1],
                                         ECase (EVar y)
                                               [(Pat ArrowTy [a2,b2],
                                                 ECase (EApp (EApp (EVar checkTEQ) (EVar a1))
                                                             (EVar a2))
                                                       [(Pat Just [refltmp],
                                                         ECase (EVar refltmp)
                                                               [(Pat Refl [],
                                                                 ECase (EApp (EApp (EVar checkTEQ)
                                                                                   (EVar b1))
                                                                             (EVar b2))
                                                                       [(Pat Just [refltmp],
                                                                         ECase (EVar refltmp)
                                                                               [(Pat Refl [],
                                                                                 EApp (EK Just)
                                                                                      (EK Refl))]),
                                                                        (Pat Nothing [],
                                                                         EK Nothing)])]),
                                                        (Pat Nothing [], EK Nothing)]),
                                                (Pat Int [], EK Nothing)]),
                                        (Pat Int [],
                                         ECase (EVar y)
                                               [(Pat ArrowTy [a2,b2], EK Nothing),
                                                (Pat Int [], EApp (EK Just) (EK Refl))])]))}]
     (EApp (EApp (EK ArrowTyDict) (EK IntDict)) (EK IntDict))