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