@@ -47,8 +47,10 @@ delab' ist tm fullname = de [] tm
4747 deFn env (P _ n _) [l,r] | n == pairTy = PPair un (de env l) (de env r)
4848 | n == eqCon = PRefl un
4949 | n == UN "lazy" = de env r
50− | n == UN "Exists" = PDPair un (de env l) Placeholder
51− (de env r)
50+ deFn env (P _ n _) [ty, Bind x (Lam _) r]
51+ | n == UN "Exists"
52+ = PDPair un (PRef un x) (de env ty)
53+ (de env (instantiate (P Bound x ty) r))
5254 deFn env (P _ n _) [_,_,l,r] | n == pairCon = PPair un (de env l) (de env r)
5355 | n == eqTy = PEq un (de env l) (de env r)
5456 | n == UN "Ex_intro" = PDPair un (de env l) Placeholder