Prepare for scott encodings

mced/Base/Inference.mced

@@ -54,10 +54,9 @@ let isSolved (l : List App) : Bool :=
   isNil ?App (filter ?App (λ a : App. isUnknown $ appTerm a) l).
 
 let sequenceRecApp (recapp : List (Bool × Eval Term)) : Eval (List App) :=
-  sequenceEval ?App $
-    map ?(Bool × Eval Term) ?(Eval App)
-      (recursionProduct ?Bool ?(Eval Term) ?(Eval App) λ b : Bool. λ t : Eval Term.
-        mapEval ?Term ?App (mkApp b) t)
+  traverseEval ?(Bool × Eval Term) ?App
+    (recursionProduct ?Bool ?(Eval Term) ?(Eval App) λ b : Bool. λ t : Eval Term.
+      mapEval ?Term ?App (mkApp b) t)
     recapp.
 
 -- apply f to all applications in a term
@@ -172,8 +171,8 @@ let tryHNFEqn : UnsEqn -> Eval UnsEqn :=
     pureEval ?UnsEqn $ mkUnsEqn' eqnC t1 t2.
 
 -- partition equations into solved and unsolved
-let partitionSolved (ctx : Nat) (eqns : List UnsEqn) : List SEqn × List UnsEqn :=
-  eqns ?(List SEqn × List UnsEqn)
+let partitionSolved (ctx : Nat) : List UnsEqn -> List SEqn × List UnsEqn :=
+  recursionList' ?UnsEqn ?(List SEqn × List UnsEqn)
     (prodPair ?(List SEqn) ?(List UnsEqn) [SEqn|] [UnsEqn|])
     (λ eq : UnsEqn. λ rec : List SEqn × List UnsEqn.
       maybe ?SEqn ?(List SEqn × List UnsEqn)

mced/Base/ReduceMultiApp.mced

@@ -11,16 +11,17 @@ let reduceMultiApp : Term -> Term :=
       (λ t1 : Term. λ app1 : List App.
         ψ reduceAppL = map ?App ?App $ productMap2 ?Bool ?Term ?Term reduceMultiApp
                       : List App -> List App.
-        ψ t          = appLTerm (reduceMultiApp t1) (reduceAppL app1) : Term. matchTerm ?Term
+        ψ t1r        = reduceMultiApp t1 : Term.
+        ψ app1r      = reduceAppL app1 : List App.
+        ψ t          = appLTerm t1r app1r : Term. matchTerm ?Term
           (λ _ : Var. t)
           (λ _ : Sort. t)
           (λ _ : Binder. λ _ : String. λ _, _ : Term. t)
-          (λ t2 : Term. λ app2 : List App.
-            reduceMultiApp $ appLTerm t2 (reduceAppL $ app ?App app2 app1))
+          (λ t2 : Term. λ app2 : List App. appLTerm t2 (app ?App app2 app1r))
           (λ _ : Char. t)
           t
           (λ _ : Term. t)
-          t1)
+          t1r)
       charTerm
       unknownTerm
       (λ t : Term. unquoteTerm (reduceMultiApp t)).

mced/Bootstrap/Stage-1/List.mced

@@ -28,14 +28,20 @@ let recursionList' := Λ A : * Λ X : * λ rn : X λ rc : Π _ : A Π _ : X X λ
   [[<l X> rn] rc]
   : ∀ A : * ∀ X : * Π rn : X Π rc : Π _ : A Π _ : X X Π l : [List A] X.
 
-let length := Λ X : * λ l : [List X]
-  [[<l Nat> zero] λ x : X λ n : Nat [suc n]]
+let matchList' := Λ A : * Λ X : * λ rn : X λ rc : Π _ : A Π _ : [List A] X
+  [[<<recursionList A> X> rn] λ a : A λ as : [List A] λ _ : X [[rc a] as]]
+  : ∀ A : * ∀ X : * Π _ : X Π _ : Π _ : A Π _ : [List A] X Π _ : [List A] X.
+
+--------------------------------------------------------------------------------
+
+let length := Λ X : *
+  [[<<recursionList' X> Nat> zero] λ x : X λ n : Nat [suc n]]
   : ∀ X : * Π _ : [List X] Nat.
 
 let nilLength := Λ X : * β zero zero : ∀ X : * = zero [<length X> <nil X>].
 
-let isNil := Λ X : * λ l : [List X]
-  [[<l Bool> true] λ _ : X λ _ : Bool false]
+let isNil := Λ X : *
+  [[<<matchList' X> Bool> true] λ _ : X λ _ : [List X] false]
   : ∀ X : * Π _ : [List X] Bool.
 
 let listEq := Λ X : * λ eqX : Π _ : X Π _ : X Bool
@@ -47,27 +53,27 @@ let listEq := Λ X : * λ eqX : Π _ : X Π _ : X Bool
 let pureList := Λ X : * λ x : X [[<cons X> x] <nil X>] : ∀ X : * Π _ : X [List X].
 
 let app := Λ X : * λ l1 : [List X] λ l2 : [List X]
-  [[<l1 [List X]> l2] λ x : X λ rec : [List X] [[<cons X> x] rec]]
+  [[[<<recursionList' X> [List X]> l2] λ x : X λ rec : [List X] [[<cons X> x] rec]] l1]
   : ∀ X : * Π _ : [List X] Π _ : [List X] [List X].
 
 let snoc := Λ X : * λ x : X λ xs : [List X] [[<app X> xs] [<pureList X> x]]
   : ∀ X : * Π _ : X Π _ : [List X] [List X].
 
-let filter := Λ X : * λ f : Π _ : X Bool λ l : [List X]
-  [[<l [List X]> <nil X>]
+let filter := Λ X : * λ f : Π _ : X Bool
+  [[<<recursionList' X> [List X]> <nil X>]
     λ x : X λ rec : [List X] [[[<ifthenelse [List X]> [f x]] [[<cons X> x] rec]] rec]]
   : ∀ X : * Π f : Π _ : X Bool Π _ : [List X] [List X].
 
-let foldl := Λ A : * Λ B : * λ f : (Π _ : B Π _ : A B) λ l : [List A]
-  [[<l Π _ : B B>
+let foldl := Λ A : * Λ B : * λ f : (Π _ : B Π _ : A B)
+  [[<<recursionList' A> Π _ : B B>
   λ b : B b]
   λ a : A λ rec : Π _ : B B λ b : B [[f [rec b]] a]].
 
 let foldr := Λ A : * Λ B : * λ f : (Π _ : A Π _ : B B) λ l : [List A] λ b : B
-  [[<l B> b] λ a : A λ rec : B [[f a] rec]].
+  [[[<<recursionList' A> B> b] λ a : A λ rec : B [[f a] rec]] l].
 
-let reverseAcc := Λ X : * λ l : [List X]
-  [[<l Π _ : [List X] [List X]>
+let reverseAcc := Λ X : *
+  [[<<recursionList' X> Π _ : [List X] [List X]>
     λ acc : [List X] acc]
     λ x : X λ rec : Π _ : [List X] [List X] λ acc : [List X] [rec [[<cons X> x] acc]]].
 
@@ -79,8 +85,8 @@ let scanl := Λ A : * Λ B : * λ f : (Π _ : B Π _ : A B) λ b : B
   [<pureList B> b]]
   λ a : A λ as : [List A] λ rec : [List B] [[<cons B> [[[<<foldl A> B> f] [[<cons A> a] as]] b]] rec]].
 
-let map := Λ X : * Λ Y : * λ f : Π _ : X Y λ l : [List X]
-  [[<l [List Y]> <nil Y>] λ x : X λ rec : [List Y] [[<cons Y> [f x]] rec]].
+let map := Λ X : * Λ Y : * λ f : Π _ : X Y
+  [[<<recursionList' X> [List Y]> <nil Y>] λ x : X λ rec : [List Y] [[<cons Y> [f x]] rec]].
 
 let intersperse :=
   Λ X : * λ x : X λ l : [List X] [[[<<recursionList X> [List X]> <nil X>]

mced/Bootstrap/Stage-1/View.mced

@@ -6,9 +6,17 @@ let beta := Λ X : * λ x : X β x x.
 let idTop := λ x : * x.
 let Top := = idTop idTop.
 
+let beta' := Λ X : * λ x : X β idTop x.
+
 let intrTop := β idTop idTop : Top.
 let toTop := Λ T : * λ t : T β idTop t : ∀ T : * Π _ : T Top.
 
+let ycomb := Λ T : * λ t : (Π _ : T T) β idTop [λ x : * [t [x x]] λ x : * [t [x x]]]
+  : ∀ T : * Π _ : (Π _ : T T) Top.
+
+let ycombBeta := Λ T : * λ f : (Π _ : T T) β [ycomb f] [ycomb f]
+  : ∀ T : * Π f : (Π _ : T T) (= [ycomb f] [f [ycomb f]]).
+
 let conv := Λ S : * Λ T : * Λ s : S λ t : T Λ eq : (= s t) φ eq s t.
 
 let View := λ T : * λ t : Top ι x : T (= x t) : Π T : * Π _ : Top *.
@@ -36,6 +44,10 @@ let extView := Λ S : * Λ T : * λ t : Top Λ v : Π x : S [[View T] β idTop [
 let Cast := λ S : * λ T : * [[View Π _ : S T] intrTop]
   : Π S : * Π T : * *.
 
+let extCast := Λ S : * Λ T : * Λ v : Π x : S [[View T] [<beta' S> x]]
+  <[<<extView S> T> intrTop] v>
+  : ∀ S : * ∀ T : * ∀ _ : (Π x : S [[View T] [<beta' S> x]]) [[Cast S] T].
+
 let intrCast := Λ S : * Λ T : * Λ t : (Π _ : S T) Λ t' : (Π x : S = [t x] x)
  <[<<extView S> T> intrTop] (λ x : S <<[<intrView T> β idTop x] [t x]> [t' x]>)>
   : ∀ S : * ∀ T : * ∀ t : (Π _ : S T) ∀ _ : (Π x : S = [t x] x) [[Cast S] T].

mced/Bootstrap/Stage-2/Term.mced

@@ -234,9 +234,9 @@ let multiTermRest := <<pr2 Term> [List [[Product Term] InfixData]]>
 --     : Π _ : MultiTerm Term.
 
 let multiTermToTermRight := λ m : MultiTerm
-  [[[<<recursionList [[Product Term] InfixData]> Term>
+  [[[<<matchList' [[Product Term] InfixData]> Term>
     [multiTermSingle m]]
-    λ h : [[Product Term] InfixData] λ t : [List [[Product Term] InfixData]] λ _ : Term
+    λ h : [[Product Term] InfixData] λ t : [List [[Product Term] InfixData]]
       [[appToTerm
         [[[<<foldr [[Product Term] InfixData]> [[Product Term] InfixData]>
           λ x : [[Product Term] InfixData] λ acc : [[Product Term] InfixData]

mced/Bootstrap/Stage-3/Eval.mced

@@ -166,8 +166,8 @@ b-let mapEval [T, T' : *] (f : T -> T') (t : Eval T) : Eval T' :=
   bindEval ?T ?T' t (λ x : T. pureEval ?T' (f x)).
 b-let seqEval [T, T' : *] (t : Eval T) (t' : Eval T') : Eval T' :=
   bindEval ?T ?T' t (λ _ : T. t').
-b-let sequenceEval [T : *] (l : List (Eval T)) : Eval (List T) :=
-  l ?(Eval (List T))
+b-let sequenceEval [T : *] : List (Eval T) -> Eval (List T) :=
+  recursionList' ?(Eval T) ?(Eval (List T))
     (pureEval ?(List T) (nil ?T))
     (λ x : Eval T. λ rec : Eval (List T). bindEval ?T ?(List T) x
       λ x' : T. mapEval ?(List T) ?(List T) (cons ?T x') rec).
@@ -229,7 +229,7 @@ b-let annLet (n : String) (t, T : Term) : Eval Unit :=
 b-let setMEnv (eval : Term) (NT, ns : String) : Eval Unit :=
   liftMtoEval ?Unit (primSetEval (TermToInitTerm eval) NT ns).
 b-let shellCmd (cmd : String) (args : List String) : Eval String :=
-  liftMtoEval ?String (primShellCmd cmd args).
+  liftMtoEval ?String (primShellCmd cmd (listStringToStringList args)).
 b-let checkTerm (T : *) (t : Term) : Eval T :=
   liftMtoEval ?T (primCheckTerm T (TermToInitTerm t)).
 b-let parse (nt : String) (T : *) (text : String) : Eval (Product T String) :=
@@ -257,10 +257,11 @@ b-let writeFile (fName, s : String) : Eval Unit :=
   liftMtoEval ?Unit (primWriteFile fName s).
 
 b-let commandLine : Eval (List String) :=
-  liftMtoEval ?(List String) primCommandLine.
+  mapEval ?init$stringList ?(List String) stringListToListString
+    (liftMtoEval ?init$stringList primCommandLine).
 
 b-let setDebug (opts : List String) : Eval Unit :=
-  liftMtoEval ?Unit (primSetDebug opts).
+  liftMtoEval ?Unit (primSetDebug (listStringToStringList opts)).
 
 b-let printLineEval (s : String) : Eval Unit := printEval φ"${s}\n".
 
@@ -318,9 +319,9 @@ b-let letInfoToNewStmt (i : LetInfo) : Eval Unit :=
 b-let ElabLet : * := LetInfo -> Eval LetInfo.
 
 b-let runEvalLets' : List ElabLet -> ElabLet :=
-  recursionList ?ElabLet ?ElabLet
+  recursionList' ?ElabLet ?ElabLet
     (pureEval ?LetInfo)
-    (λ el : ElabLet. λ _ : List ElabLet. λ rec : ElabLet.
+    (λ el : ElabLet. λ rec : ElabLet.
       λ i : LetInfo. bindEval ?LetInfo ?LetInfo (el i) rec).
 
 b-let runEvalLets (els : List ElabLet) (i : LetInfo) : Eval Unit :=

mced/Bootstrap/Stage-3/ListExt.mced

@@ -9,17 +9,17 @@ b-let showList [X : *] (showX : X -> String) (l : List X) : String :=
   φ"[${stringConcat (intersperse ?String ", " (map ?X ?String showX l))}]".
 
 b-let lookupDefault [A : *] (n : Nat) (d : A) (l : List A) : A :=
-  l ?(Nat -> A)
+  recursionList' ?A ?(Nat -> A)
     (λ _ : Nat. d)
     (λ a : A. λ rec : Nat -> A.
       recursionNat ?A a (λ k : Nat. λ _ : A. rec k))
-    n.
+    l n.
 
-b-let head [A : *] (l : List A) : Maybe A :=
-  l ?(Maybe A) (nothing ?A) (λ a : A. λ _ : Maybe A. just ?A a).
+b-let head [A : *] : List A -> Maybe A :=
+  matchList' ?A ?(Maybe A) (nothing ?A) (λ a : A. λ _  : List A. just ?A a).
 
-b-let tail [A : *] (l : List A) : List A :=
-  recursionList ?A ?(List A) [A|] (λ a : A. λ l' : List A. λ _ : List A. l') l.
+b-let tail [A : *] : List A -> List A :=
+  matchList' ?A ?(List A) [A|]          (λ _ : A. λ as : List A. as).
 
 b-let findMaybe [A : *] (P : A -> Bool) (l : List A) : Maybe A :=
   head ?A (filter ?A P l).
@@ -34,8 +34,8 @@ b-let maybeToList [A : *] : Maybe A -> List A :=
   maybe ?A ?(List A) [A|] (λ a : A. [A|a]).
 
 b-let mapHead [A : *] (f : Maybe A -> Maybe A) : List A -> List A :=
-  recursionList ?A ?(List A) (maybeToList ?A (f (nothing ?A)))
-    (λ a : A. λ as, _ : List A. app ?A (maybeToList ?A (f (just ?A a))) as).
+  matchList' ?A ?(List A) (maybeToList ?A (f (nothing ?A)))
+    (λ a : A. λ as : List A. app ?A (maybeToList ?A (f (just ?A a))) as).
 
 b-let initsNonEmpty [A : *] (l : List A) : List (Product A (List A)) :=
   recursionList ?A ?(List (Product A (List A)))
@@ -60,13 +60,14 @@ b-let countToZeroExc (n : Nat) :=
     n.
 
 b-let zipWith [A, B, C : *] (f : A -> B -> C) (l : List A) (l' : List B) : List C :=
-  l ?(List B -> List C)
+  recursionList' ?A ?(List B -> List C)
     (λ _ : List B. [C|])
     (λ a : A. λ rec : List B -> List C.
-      recursionList ?B ?(List C) [C|] (λ b : B. λ bs : List B. λ _ : List C. cons ?C (f a b) (rec bs)))
-    l'.
+      matchList' ?B ?(List C) [C|] (λ b : B. λ bs : List B. cons ?C (f a b) (rec bs)))
+    l l'.
 
-b-let zip [A, B : *] (l : List A) (l' : List B) : List (Product A B) := zipWith ?A ?B ?(Product A B) (prodPair ?A ?B) l l'.
+b-let zip [A, B : *] (l : List A) (l' : List B) : List (Product A B) :=
+  zipWith ?A ?B ?(Product A B) (prodPair ?A ?B) l l'.
 
 b-let zipWith3 [A, B, C, D : *] (f : A -> B -> C -> D) (l : List A) (l' : List B) (l'' : List C) : List D :=
   zipWith ?A ?(Product B C) ?D (λ a : A. λ bc : Product B C. f a (pr1 ?B ?C bc) (pr2 ?B ?C bc)) l (zip ?B ?C l' l'').
@@ -80,8 +81,8 @@ b-let zipWith4 [A, B, C, D, E : *] (f : A -> B -> C -> D -> E)
     (λ a : A. λ bcd : TripleProduct B C D.
       f a (pr31 ?B ?C ?D bcd) (pr32 ?B ?C ?D bcd) (pr33 ?B ?C ?D bcd)) l (zip3 ?B ?C ?D l' l'' l''').
 
-b-let concat [A : *] (l : List (List A)) : List A :=
-  l ?(List A) [A|] (λ l' : List A. λ rec : List A. app ?A l' rec).
+b-let concat [A : *] : List (List A) -> List A :=
+  recursionList' ?(List A) ?(List A) [A|] (λ l' : List A. λ rec : List A. app ?A l' rec).
 
 b-let drop [A : *] (n : Nat) (l : List A) : List A :=
   n ?(List A) l (tail ?A).

mced/Bootstrap/Stage-3/Quoters.mced

@@ -7,5 +7,5 @@ b-let quoteProduct [A, B : *] (quotedA, quotedB : Term) (quoteA : A -> Term) (qu
   λ x : Product A B. θ{prodPair ?γ{quotedA} ?γ{quotedB} γ{quoteA (pr1 ?A ?B x)} γ{quoteB (pr2 ?A ?B x)}}.
 
 b-let quoteList [X : *] (quotedX : Term) (quoteX : X -> Term) : List X -> Term :=
-  recursionList ?X ?Term θ{nil ?γ{quotedX}}
-    (λ x : X. λ _ : List X. λ rec : Term. θ{cons ?γ{quotedX} γ{quoteX x} γ{rec}}).
+  recursionList' ?X ?Term θ{nil ?γ{quotedX}}
+    (λ x : X. λ rec : Term. θ{cons ?γ{quotedX} γ{quoteX x} γ{rec}}).

mced/Bootstrap/Stage-3/StringHelpers.mced

@@ -5,16 +5,23 @@
 b-let stringToList (s : String) : List Char :=
   s ?(List Char) (λ c : Char. λ rec : List Char. cons ?Char c rec) (nil ?Char).
 
-b-let stringFromList (s : List Char) : String :=
-  s ?String stringNil stringCons.
+b-let stringFromList : List Char -> String :=
+  recursionList' ?Char ?String stringNil stringCons.
 
 b-let stringApp (s, s' : String) : String :=
   s ?String stringCons s'.
 
-b-let stringConcat (l : List String) : String :=
-  l ?String stringNil stringApp.
+b-let stringConcat : List String -> String :=
+  recursionList' ?String ?String stringNil stringApp.
 
 -- Equality
 
 b-let stringEq (s, s' : String) : Bool :=
   listEq ?Char charEq (stringToList s) (stringToList s').
+
+b-let listStringToStringList : List String -> init$stringList :=
+  recursionList' ?String ?init$stringList
+    stringListNil stringListCons.
+
+b-let stringListToListString (s : init$stringList) : List String :=
+  s ?(List String) (nil ?String) (cons ?String).

mced/Bootstrap/Stage-3/TermHelpers.mced

@@ -19,9 +19,9 @@ let indexToIndex' (i : DBIndex) : DBIndex' :=
 
 let digitListToIndex' (l : List Dec) : DBIndex' := foldl ?Dec ?DBIndex' consDecToIndex' l init$index'$.
 let digitListToIndex : List Dec -> DBIndex :=
-  recursionList ?Dec ?DBIndex
+  matchList' ?Dec ?DBIndex
     (init$index$0_index'_ init$index'$)
-    (λ d : Dec. λ ds : List Dec. λ _ : DBIndex. consDecToIndex (digitListToIndex' ds) d).
+    (λ d : Dec. λ ds : List Dec. consDecToIndex (digitListToIndex' ds) d).
 
 let natToIndex (n : Nat) : DBIndex := digitListToIndex $ natToDecList n.
 let natToVar (n : Nat) : Term := varTerm $ init$var$_index_ $ natToIndex n.

mced/Bootstrap/Stage-3/TermRec.mced

@@ -10,8 +10,7 @@ b-let mapAppList [X, Y : *] (f : X -> Y) (l : List (Product Bool X)) : List (Pro
 
 b-let distList [X, Y, Z : *]
   : List (TripleProduct X Y Z) -> Product (List (Product X Y)) (List (Product X Z)) :=
-  λ l : List (TripleProduct X Y Z).
-  l ?(Product (List (Product X Y)) (List (Product X Z)))
+  recursionList' ?(TripleProduct X Y Z) ?(Product (List (Product X Y)) (List (Product X Z)))
     (prodPair ?(List (Product X Y)) ?(List (Product X Z)) (nil ?(Product X Y)) (nil ?(Product X Z)))
     (recursionTripleProduct ?X ?Y ?Z
       ?(Product (List (Product X Y)) (List (Product X Z))

mced/Test/Bootstrap/Eval.mced

@@ -333,10 +333,9 @@ elet letInfoToNewStmt (i : LetInfo) : Eval Unit :=
 
 let ElabLet : * := LetInfo -> Eval LetInfo.
 
-elet runEvalLets' : List ElabLet -> ElabLet := recursionList ?_ ?_
+elet runEvalLets' : List ElabLet -> ElabLet := recursionList' ?_ ?_
   (pureEval ?LetInfo)
-  (λ el : ElabLet. λ _ : List ElabLet. λ rec : ElabLet.
-    λ i : LetInfo. el i >>= rec).
+  (λ el : ElabLet. λ rec : ElabLet. λ i : LetInfo. el i >>= rec).
 
 elet runEvalLets (els : List ElabLet) (i : LetInfo) : Eval Unit :=
   runEvalLets' els i >>= letInfoToNewStmt.

mced/Test/COC/Conversion.mced

@@ -6,7 +6,7 @@ module COC:Conversion.
 
 Given MCTerm MCSVar MCAst MCSq MCLambda MCPi MCApp natToVar indexToNat init$index.
 Given MCVar MCSort Binder String stringCons stringNil stringEq Char.
-Given List cons nil reverse Product Bool true false ifthenelse pr1 pr2.
+Given List cons nil recursionList' reverse Product Bool true false ifthenelse pr1 pr2.
 Given TripleProduct mkTripleProduct pr31 pr32 pr33.
 Given LetInfo letInfoName letInfoTerm letInfoType.
 Given Maybe just nothing maybe bindMaybe mapMaybe.
@@ -15,8 +15,8 @@ importModule DatatypesTest:Nat.
 importModule DatatypesTest:NatConversions.
 importModule COC:Theory.
 
-let findMaybe [A : *] (pred : A -> Bool) (l : List A) : Maybe Nat :=
-  l ?(Maybe Nat)
+let findMaybe [A : *] (pred : A -> Bool) : List A -> Maybe Nat :=
+  recursionList' ?A ?(Maybe Nat)
     (nothing ?Nat)
     (λ a : A. λ rec : Maybe Nat. ifthenelse ?(Maybe Nat) (pred a) (just ?Nat zero) (mapMaybe ?Nat ?Nat succ rec)).
 
@@ -36,14 +36,15 @@ let toCOCTerm (t : MCTerm) : Maybe Term :=
             (just ?Term (Pi x x'))
             (nothing ?Term)) (t' (cons ?String n l))) (t l))
     (λ t : List String -> Maybe Term. λ app : List (Product Bool (List String -> Maybe Term)). λ l : List String.
-      (reverse ?(Product Bool (List String -> Maybe Term)) app) ?(Maybe Term)
+      recursionList' ?(Product Bool (List String -> Maybe Term)) ?(Maybe Term)
         (t l)
         (λ a : Product Bool (List String -> Maybe Term). λ rec : Maybe Term.
           maybe ?Term ?(Maybe Term) (nothing ?Term)
             (λ x : Term. ifthenelse ?(Maybe Term) (pr1 ?Bool ?(List String -> Maybe Term) a)
               (nothing ?Term)
               (maybe ?Term ?(Maybe Term) (nothing ?Term)
-                (λ x' : Term. just ?Term (App x' x)) rec)) (pr2 ?Bool ?(List String -> Maybe Term) a l)))
+                (λ x' : Term. just ?Term (App x' x)) rec)) (pr2 ?Bool ?(List String -> Maybe Term) a l))
+        (reverse ?(Product Bool (List String -> Maybe Term)) app))
     (λ _ : Char. λ _ : List String. nothing ?Term)
     (λ _ : List String. nothing ?Term)
     (λ _ : List String -> Maybe Term. λ _ : List String. nothing ?Term) -- nothing on unquote