Lean4Lean: Lean 4 kernel in Lean

Stream: general

[Mario Carneiro]

I'm pleased to announce the initial (alpha) release of lean4lean, a lean 4 kernel implementation written entirely in lean 4. This is the first complete kernel implementation other than the original (AFAIK). In fact, even the elaborator, which is essentially a strictly more complexified version of the kernel (because it also has to deal with things like metavariables), doesn't know all the tricks that the kernel does, especially around validity checking for inductives and anything to do with nested inductives.

It is essentially a "Rewrite it in Lean" direct port of the C++ code. For now it is just the core implementation, there is no frontend to speak of, but it provides Environment.addDecl' which is a drop-in replacement for Environment.addDecl. It also makes use of Lean data structures (Expr, Environment, etc) so it should be compatible with other lean metaprograms, and is a good starting point for hacking the kernel (e.g. adding print messages, tracing reduction, profiling, etc).

A stretch goal for the project is to also add lean metatheory and maybe prove some properties about the kernel. The main thing that was done to facilitate this is that it only uses pure lean data structures: no IO, no ST, and almost no partial (there are some inherited partial from lean functions and some TODOs in the code). I think it is feasible to get to a point where one could prove soundness at least in principle.

The natural question for self-verification projects like this is: where is the "cheat", what makes this not the kind of verification that is precluded by Goedel's incompleteness theorems? Well, the reduction process is not obviously structurally recursive and you need some stupendously large ordinals to find a decreasing metric for #reduce. Absent that, you essentially have to treat reduction as a potentially non-terminating process. Luckily, this accords well with another fact of life: Lean doesn't run reduction forever anyway, because it has (deterministic) timeout and deep recursion errors if you try. So for this implementation we just run reduction for N steps where N is a large number and timeout if it doesn't complete. With this truncated reduction, it is possible to prove termination in lean, as well as soundness.

[Jason Rute]

Sorry, what does “soundness” mean in this setting? Do you have a particular model in mind?

[Mario Carneiro]

yes, #leantt

[Jason Rute]

So every theorem provable by the kernel plus the standard lean axioms holds in ZFC + infinitely many large cardinals (under the usual interpretation of types as sets, etc.)?

[Mario Carneiro]

Formalizing the results of my thesis has been a long standing goal of mine. A kernel is a slightly different kind of task which doesn't overlap that much with metatheory, but it's a start: at least one can state claims like consistency or soundness using lean data types

[Jason Rute]

I agree. I’m just wrapping my head around what the statement of the theorem for soundness would be. (Consistency is easier to state of course.)

[Mario Carneiro]

yes that's the right statement (modulo some details)

[Mario Carneiro]

there are basically two theorems of interest: (1) everything the lean kernel accepts is a theorem of LeanTT, and (2) there is a model of LeanTT in ZFC + omega universes, so in particular False is not a theorem of LeanTT

[Mario Carneiro]

Here LeanTT represents the "abstract representation" of the type theory, more or less what you get in my thesis

[Mario Carneiro]

I have more real worries about (1) being false than (2). In a big program there is a lot of room for trivial errors

[Utensil Song]

Mario Carneiro said:

yes, #leantt

Also with updates from https://lean-lang.org/papers/thesis-sebastian.pdf#section.3.2 , I assume?

[Yaël Dillies]

It's Lean all the way down!

[Scott Morrison]

So what is the path to lean4lean4checker, and having it run in Mathlib CI?

[Vincent Beffara]

Anyone wants to implement the "reflections on trusting trust" concept in lean4? https://www.cs.cmu.edu/~rdriley/487/papers/Thompson_1984_ReflectionsonTrustingTrust.pdf

[Mario Carneiro]

Scott Morrison said:

So what is the path to lean4lean4checker, and having it run in Mathlib CI?

I have already copied the core of lean4checker into lean4lean because it's the easiest way to test the program, although I haven't thought about how to distribute it yet. (It's still at the riddled-with-bugs stage, I was excited to release it but I hadn't actually tried to run it yet because I was afraid of what I would find. I'm sure it's at least a few more days of debugging before it will check mathlib and we can do actual profiling.)

[Joachim Breitner]

Would it be (hypothetically, for now) possible to replace the C++ kernel in lean with the lean-implemented one at some point? Would we expect any gains (besides that more of the lean code is accessible to people knowing only lean)?

[Henrik Böving]

As I understand the interaction point of the Compiler with the Kernel is through C FFI, passing in Environment among other things. And since we can @[export] functions to make them available as callable functions through C FFI it should definitely be possible to link in the lean4lean kernel from a technical POV.

[Joachim Breitner]

I more wonder: What qualities do we want from a kernel implemenation? Is there something that a reimplementation like lean4lean could provide that would make us want to use that as the “the” kernel?
I guess as per the other recent discussions, lean is “only” the proof assistant, and the built-in kernel is mostly a sanity check, so speed and maybe good error messages matter most? Whereas correctness is actually less important compared to when used as an external checker afterwards.

[Mario Carneiro]

Correctness is obviously one of the most important aspects of a kernel implementation. The other main one is performance, and this is why lean4lean uses all the optimizations from the original. (It is difficult to second-guess whether a kernel optimization is really critical or not because it might show up only in certain kinds of programs that stress particular parts of the implementation.) I expect there to be some performance drop relative to the C++ implementation because the compiler might not be able to optimize the lean code as well, we will have to see.

[Mario Carneiro]

There are three main remaining components in the C++ code:

1. the kernel
2. the (old) compiler frontend (Expr -> IR)
3. the interpreter

It would be possible to upstream lean4lean and this basically crosses (1) off the list. Similarly, (2) is "just" a matter of porting the old code, although I think this is hampered somewhat by the desire to "do it better this time" and so now the whole compiler is being redesigned and this could take a while. (3) seems the hardest to move to lean, because it has some really extreme performance requirements and I can't see lean ever being good enough for that (even C/C++/Rust can't make optimal interpreter code sometimes and you have to drop to assembly to get the right codegen). But with those components covered lean could move to a fully self-hosted system and drop the requirement of a C++ compiler, and my impression is that this is a long term goal of the project.

[Mario Carneiro]

By the way, lean4lean does not support reduceBool, despite a fair amount of thinking on how to do it. (For those who haven't already guessed, the recent discussion of reduceBool stems from investigations into reimplementing and validating the kernel.) To do it in pure lean, you would need the interpreter to also exist in pure lean, which is a separate project (item (3) on the list). The simple cheat would be to just call it as an opaque function but this tanks some of the metatheory goals. There are more elaborate ways to specify it somewhat abstractly.

[Joachim Breitner]

Could lean4lean support reduceBool by normalising the Expr, i.e. _not_ invoking the compiled code? Presumably that would be rather slow, and people use reduceBool precisely when that would be too slow, but would there be otherwise a difference?

[Mac Malone]

Mario Carneiro said:

(3) seems the hardest to move to lean, because it has some really extreme performance requirements and I can't see lean ever being good enough for that (even C/C++/Rust can't make optimal interpreter code sometimes and you have to drop to assembly to get the right codegen).

With the new LLVM backend, replacing the interpreter with JIT could work. Furthermore, with the new in-Lean compiler, it would be possible to swap out implementations with manually construct LLVM definitions (which can include inline assembly). Thus, fully hosted compiler+interpreter should be possible in the future.

[Mario Carneiro]

I'm not talking about replacing the interpreter with something else, I'm talking about writing the interpreter itself in lean. We will always have a need for an interpreter, and it is very important that the interpreter be fast because it has a multiplicative effect on all code run through the interpreter. A JIT would not replace the interpreter, it would only supplement it (I can't think of any interpreted language which was able to move to 100% JIT, they usually keep the interpreter and go back and forth based on dynamic performance measurements).

[Mario Carneiro]

Joachim Breitner said:

Could lean4lean support reduceBool by normalising the Expr, i.e. _not_ invoking the compiled code? Presumably that would be rather slow, and people use reduceBool precisely when that would be too slow, but would there be otherwise a difference?

It could. The simplest way to do that would be to have reduceBool be a def instead of an opaque, since that is effectively what you are saying: it is defeq to its value after unfolding. I think the main issue with doing this in practice is that quite often this reduction won't work because it will get stuck on an opaque for something the compiler implements externally. It could also explode in time/space requirements as you note, it's hard to predict this in advance.

[Jason Rute]

Mario Carneiro said:

A JIT would not replace the interpreter, it would only supplement it (I can't think of any interpreted language which was able to move to 100% JIT, they usually keep the interpreter and go back and forth based on dynamic performance measurements).

What does Julia do in this regard?

[Mario Carneiro]

From what I can tell, Julia is indeed "100% JIT". I also saw the term "just ahead of time" used to describe it, and it's not too dissimilar to what lean currently does: it runs the compiler on the spot when you write an expression at the repl, and executes the result (no tracing and optimistic re-compilation like in actual JIT languages like Java or JS). I think lean could do this in theory, and the theory is getting closer to practice as the work on LLVM JIT / GccJit progresses.

[Mario Carneiro]

There does seem to be a julia interpreter package but it's not part of the default distribution

[Mario Carneiro]

and if the interpreter is relegated to this kind of place in the lean ecosystem it wouldn't be a big deal if it was written in 100% lean since the majority case would be all be efficient native code generated by the JIT

[Joachim Breitner]

Ah, so reduceBool not only evaluates “normal” definitions (possibly with implemented_by or csimp attributes), but also opaque definitions where only a compiled definition exists, and normal reduction can't even do anything.

[Mario Carneiro]

Update: lean4lean is now tested and working on all of the Lean package. I think it's ready for performance testing...

[Mario Carneiro]

Initial numbers show a 36% slowdown relative to the C++ code:

$ time build/bin/lean4lean --fresh Lean
Executed in   20.98 secs    fish           external
   usr time   20.76 secs  405.00 micros   20.76 secs
   sys time    0.15 secs  237.00 micros    0.15 secs

$ time build/bin/lean4checker --fresh Lean
Executed in   15.19 secs    fish           external
   usr time   15.02 secs  520.00 micros   15.02 secs
   sys time    0.07 secs  161.00 micros    0.07 secs

Alas, lean code still can't quite compete. :( But this was more or less as expected, and the important part is that it's not an order of magnitude slower.

[Scott Morrison]

Still, for a first speed test, that is really competitive!

[Scott Morrison]

And certainly fast enough to happily use in CI.

[Scott Morrison]

Should I set it up to run on all of Mathlib?

[Scott Morrison]

Maybe that doesn't even need a fast machine. lean4checker only takes ~15 minutes in CI.

[Mario Carneiro]

yes please

[Joachim Breitner]

Same order of magnitude on first try is pretty good, congrats! Still wondering if this could be used to de-C++ lean itself some more :-)

[Scott Morrison]

Unfortunately it appears to be quite a bit slower on Mathlib:

% time lake env ../lean4checker/build/bin/lean4checker --fresh Mathlib
lake env ../lean4checker/build/bin/lean4checker --fresh Mathlib  1201.51s user 73.39s system 99% cpu 21:15.51 total

while

% time lake env ../lean4lean/build/bin/lean4lean --fresh Mathlib

is still running with 4 hours on the clock. :-(

[Mario Carneiro]

Oh that's not good

[Mario Carneiro]

I expect the issue to be a bug in the checker, not a performance issue

[Mario Carneiro]

Lean is a fairly good test suite but it doesn't have everything

[Mario Carneiro]

Could you replace addDecl with this:

def addDecl (d : Declaration) (verbose := false) : M Unit := do
  match d with
  | .axiomDecl d => println! "adding axiomDecl {d.name}"
  | .defnDecl d => println! "adding defnDecl {d.name}"
  | .thmDecl d => println! "adding thmDecl {d.name}"
  | .opaqueDecl d => println! "adding opaqueDecl {d.name}"
  | .quotDecl => println! "adding quotDecl"
  | .mutualDefnDecl d => println! "adding mutualDefnDecl {d.map (·.name)}"
  | .inductDecl _ _ d _ => println! "adding inductDecl {d.map (·.name)}"
  match (← get).env.addDecl' d true verbose (← read).env0 with
  | .ok env => modify fun s => { s with env := env }
  | .error ex =>
    throwKernelException ex

and then log the output to see where it got stuck?

[Mario Carneiro]

(I'm actually kind of surprised you haven't reported any deep recursion or deterministic timeout errors. I somewhat arbitrarily set 1000 iterations in every place where it is not structurally recursive, and it's not actually that hard to write code that exceeds this many iterations if you try.)

[Mario Carneiro]

Another thing is that you can use non---fresh mode and compile all the environments separately. This is actually a better test for lean4lean than --fresh mode because it validates lean4lean's expressions against the C++ kernel generated exprs stored in the oleans

[Mario Carneiro]

(It's also way faster since it is multithreaded)

[Scott Morrison]

Okay, just got back to this thread, and killed it at the 8 hour mark.

[Scott Morrison]

I think you must have also changed Environment.addDecl', as this doesn't typecheck:

function expected at
  Environment.addDecl' __do_lift✝¹.env d
term has type
  Except KernelException Environment

[Scott Morrison]

% time lake env ../lean4lean/build/bin/lean4lean
lean4lean found a problem in Std.Data.String.Lemmas

and then runs forever.

[Mario Carneiro]

Scott Morrison said:

I think you must have also changed Environment.addDecl', as this doesn't typecheck:

function expected at
  Environment.addDecl' __do_lift✝¹.env d
term has type
  Except KernelException Environment

Oops, you can ignore the last two arguments

[Mario Carneiro]

I did manage to reproduce the Std.Data.String.Lemmas error, will investigate

[Mario Carneiro]

@Scott Morrison I pushed a fix for the issue above, and now Std also passes. Could you rerun the mathlib test?

[Mario Carneiro]

I found and fixed a (caching) bug in lean4lean, and the two kernels should now be very close in behavior. The test from above is now 18.89s (lean4lean) / 14.87 (lean4checker), i.e. a 27% slowdown (an improvement over the 36% reported above) although this might be noise, I don't think the caching issue shows up in Lean because it doesn't have many proofs in it.

I'm going to try running the mathlib test again and see if there are any performance cliffs.

[Mario Carneiro]

Hey @Scott Morrison , can I get you to do one more mathlib run with lean4lean? I think I've solved the last performance issues, and I have tested that every file in mathlib is within 2x of the C++, but I haven't tried doing it with --fresh and without it one has to be careful to limit the number of threads or it uses up all my memory building 12 copies of mathlib in memory.

[Scott Morrison]

Yes, but I'm away from the computer until tomorrow.

[Scott Morrison]

% time lake env ../lean4lean/build/bin/lean4lean --fresh Mathlib

killed after 9 hours.

[Scott Morrison]

@Mario Carneiro

[Mario Carneiro]

@Scott Morrison That's weird, are you sure you ran it on the latest version? I definitely managed to get it to complete in an hour or so

[Mario Carneiro]

Oh I think mathlib moved on since my test: AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_natTrans seems to be very hard, the lean kernel takes 9.4s and lean4lean takes at least 5 minutes

[Mario Carneiro]

(In those 9.4s, lean calls inferType on just over 1 million subterms. Maybe this proof should be refactored...)

[Mario Carneiro]

Here are the results of running lean4lean --fresh Mathlib and collecting data on the longest definitions. All definitions which took more than 1 second to run are listed (in units of milliseconds), and when lean was more than 2x faster it is also listed.

35084 (lean 17464) lemma AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_inv_app
23737              lemma UpperHalfPlane.isometry_vertical_line
23050              lemma CategoryTheory.Idempotents.DoldKan.hε
18733 (lean  8649) lemma AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_hom_app
17587 (lean  8519) lemma AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_natTrans
15256 (lean  4382) lemma CliffordAlgebra.GradedAlgebra.lift_ι_eq
10301 (lean  4433) lemma HasFPowerSeriesAt.comp
 9927 (lean  4934) lemma Ideal.powQuotSuccInclusion_injective
 7749 (lean  3365) lemma ModuleCat.monModuleEquivalenceAlgebra.proof_25
 7319              lemma ModuleCat.MonoidalCategory.pentagon
 6826 (lean  2582) lemma TensorProduct.directSum_symm_lof_tmul
 6701 (lean  2726) lemma finsuppTensorFinsupp_single
 6453 (lean  2879) lemma cauchySeq_finset_of_geometric_bound
 6369              lemma Submodule.pow_induction_on_right'
 6049 (lean  2715) lemma ModuleCat.monModuleEquivalenceAlgebra.proof_11
 5268 (lean  2467) lemma ModuleCat.monModuleEquivalenceAlgebra.proof_9
 5048 (lean  2296) lemma ModuleCat.monModuleEquivalenceAlgebra.proof_10
 4069              def GradedModule.isModule
 3288              lemma Ideal.homogeneousHull_eq_iSup
 3250 (lean  1610) lemma GradedModule.isModule.proof_4
 3130              lemma GradedModule.isModule.proof_6
 3121              lemma GradedModule.isModule.proof_5
 3114              lemma GradedModule.isModule.proof_2
 3109              lemma GradedModule.isModule.proof_1
 3019              lemma GradedModule.isModule.proof_3
 2961 (lean  1354) lemma CategoryTheory.Pretriangulated.shiftFunctorZero_op_hom_app
 2902 (lean  1315) lemma UpperHalfPlane.modular_T_smul
 2821 (lean   826) lemma TensorProduct.directSum.proof_4
 2784 (lean  1196) lemma Algebra.TensorProduct.opAlgEquiv.proof_14
 2289 (lean  1099) lemma Ideal.powQuotSuccInclusion_apply_coe
 2044 (lean   985) lemma ModuleCat.monModuleEquivalenceAlgebra.proof_8
 1994 (lean   893) lemma Module.torsion_by_prime_power_decomposition
 1924              lemma CommRingCat.instCreatesLimitCommRingCatMaxInstCommRingCatLargeCategoryRingCatMaxInstRingCatLargeCategoryForget₂InstConcreteCategoryCommRingCatInstCommRingCatLargeCategoryInstConcreteCategoryRingCatInstRingCatLargeCategoryHasForgetToRingCat.proof_2
 1811              lemma ContinuousLinearMap.prodMapL.proof_19
 1735              def GradedRing.proj
 1638              lemma Ideal.IsHomogeneous.isPrime_of_homogeneous_mem_or_mem
 1506              lemma AlgebraicGeometry.PresheafedSpace.colimitCocone.proof_3
 1432              lemma norm_iteratedFDerivWithin_comp_le_aux
 1430 (lean   623) lemma DirectSum.decompose_one
 1308 (lean   552) lemma CategoryTheory.Idempotents.DoldKan.hη
 1289              lemma Module.equiv_directSum_of_isTorsion
 1239 (lean   597) lemma DirectSum.decompose_symm_one
 1169 (lean   383) lemma CategoryTheory.Bicategory.adjointifyCounit_left_triangle
 1155 (lean   444) lemma TensorProduct.directSumRight_tmul_lof
 1131 (lean   417) lemma TensorProduct.directSumLeft_symm_lof_tmul
 1111 (lean   482) lemma Algebra.TensorProduct.map_ker
 1098              lemma RingCat.instCreatesLimitRingCatMaxInstRingCatLargeCategorySemiRingCatMaxInstSemiRingCatLargeCategoryForget₂InstConcreteCategoryRingCatInstRingCatLargeCategoryInstConcreteCategorySemiRingCatInstSemiRingCatLargeCategoryHasForgetToSemiRingCat.proof_2
 1085 (lean   433) lemma CategoryTheory.Localization.instIsEquivalenceFunctorCategoryFunctorsInvertingInstCategoryFunctorsInvertingWhiskeringLeftFunctor.proof_2
 1064 (lean   488) lemma Ordinal.sup_sum
 1055 (lean   386) lemma QuadraticForm.tmul_comp_tensorAssoc
 1054 (lean   270) lemma CategoryTheory.FreeBicategory.liftHom₂_congr
 1048 (lean   484) lemma Algebra.TensorProduct.opAlgEquiv.proof_15
 1014 (lean   504) lemma FormalMultilinearSeries.changeOrigin_eval

[Mario Carneiro]

I expect that basically all of these are "bad" proofs, which take a long time not because of any deep mathematical reason but rather because something unexpected is being unfolded. Note in particular that essentially none of the large tactic-heavy proofs show up in this list - these are slow for the elaborator but quite light on the kernel. The stuff that shows up here is in deeply dependent situations like in category theory and algebraic topology where defeq problems are necessary in order to even state proof goals.

[Johan Commelin]

That list is impressively short!

[Scott Morrison]

@Mario Carneiro, there's something worrying here: I'm sure that I just rebuilt Mathlib master locally, and rebuilt the latest lean4lean, but my latest run of lean4lean --fresh Mathlib was still going after 4 hours...

[Mario Carneiro]

oops, both the performance bugs from friday and the one I fixed an hour ago were not pushed :sweat_smile:

[Mario Carneiro]

the above test was done on https://github.com/digama0/lean4lean/commit/2d54c3d87b0a1f294523fa25d4a9e5a9b14999e5

[Scott Morrison]

lake env ../lean4lean/build/bin/lean4lean --fresh Mathlib  1752.20s user 137.67s system 99% cpu 31:33.01 total

[Scott Morrison]

(Compared to 21 minutes from the C++ kernel. Nice!)

[Siddhartha Gadgil]

@Mario Carneiro Can you clarify some implementation details (for my battles for the Trepplein port)?
This is regarding the functions whnf and whnfCore and the parameter cheapProj. Am I correct that:

• The difference between these is that whnf (and whnf') include unfolding definitions but this is not the case in whnfCore (and whnfCore').
• If cheapProj is true, then the less agressive normalization whnfCore is called to avoid too much looping at the cost of less complete normalization.
• When proving defEqwe set cheapProj as true and pass this on recursively, so equality may fail to be proved but crashes are avoided.

For context, the current state of the port is that it is crashing with a stackoverflow while type-checking the (huge) definition Nat.Linear.ExprCnstr.denote_toNormPolyand I traced this to recursive simplification of the struct in a projection. It looks like the sort of thing the above was meant to block so it would help if this is clear (on the flip side reducing normalization may mean types are not proved equal).

[Mario Carneiro]

I also had issues with that theorem

[Mario Carneiro]

I don't think cheapProj is used to distinguish between whnf and whnfCore

[Siddhartha Gadgil]

In reduceProj I see the line let mut c ← (if cheapProj then whnfCore struct cheapRec cheapProj else whnf struct)

[Mario Carneiro]

oh no you are right, it is only used in L302 where it does that

[Mario Carneiro]

I don't have a whole lot of insight into how and why these flags are passed around, but I guess you should do it if you aren't already and it is leading to a timeout

[Siddhartha Gadgil]

Thanks. I will experiment with an analogous flag. The structure of the code is a bit different in lean4lean versus trepplein 3, but something analogous can be done.

[Mario Carneiro]

(I swear I'm not trying to make these line up with the eve of lean community meetings but these things happen!) I want to share a major new development in the lean4lean repo: an initial formalization of lean's type theory, modeled after chapter 2.1-2.2 of #leantt. It is still missing the definition of inductive types, but it does explicitly define the environment and valid environment modifications, unlike #leantt which leaves the environment implicit.

[Mario Carneiro]

It uses a separate type VExpr which is like Expr but with some constructors removed and others macro expanded. A tool I'm particularly proud of is the vexpr(..) macro, which lets you define a VExpr from an Expr, meaning that we can reuse all of lean's elaboration features. In fact, this was so effective that it allowed me to write this borderline-cheating definition of the quotient extension:

def VEnv.addQuot (env : VEnv) : Option VEnv := do
  let env ← env.addConst ``Quot vconst(type_of% @Quot)
  let env ← env.addConst ``Quot.mk vconst(type_of% @Quot.mk)
  let env ← env.addConst ``Quot.ind vconst(type_of% @Quot.ind)
  env.addConst ``Quot.lift vconst(type_of% @Quot.lift)

which expands to

def Lean4Lean.VEnv.addQuot : VEnv → Option VEnv :=
fun env => do
  let env ←
    VEnv.addConst env `Quot
        (some
          { uvars := 1,
            type :=
              VExpr.forallE (VExpr.sort (VLevel.param 0))
                (VExpr.forallE (VExpr.forallE (VExpr.bvar 0) (VExpr.forallE (VExpr.bvar 1) (VExpr.sort VLevel.zero)))
                  (VExpr.sort (VLevel.param 0))) })
  let env ←
    VEnv.addConst env `Quot.mk
        (some
          { uvars := 1,
            type :=
              VExpr.forallE (VExpr.sort (VLevel.param 0))
                (VExpr.forallE (VExpr.forallE (VExpr.bvar 0) (VExpr.forallE (VExpr.bvar 1) (VExpr.sort VLevel.zero)))
                  (VExpr.forallE (VExpr.bvar 1)
                    (VExpr.app (VExpr.app (VExpr.const `Quot [VLevel.param 0]) (VExpr.bvar 2)) (VExpr.bvar 1)))) })
   ...