- Definition proof2expr Γ Δ τ Σ (ξ0: VV -> LeveledHaskType Γ ★)
- {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [unlev τ] @ getlev τ] ->
- FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}).
+ Definition proof2expr Γ Δ τ l Σ (ξ0: VV -> LeveledHaskType Γ ★)
+ {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ] @ l] ->
+ FreshM (???{ ξ : _ & Expr Γ Δ ξ τ l}).