84 { return Proof(Expr(d_pfOp, d_em->newVarExpr(name), pf.getExpr())); }  in newPf()
94 { return Proof(Expr(d_pfOp, d_em->newVarExpr(name), e, pf.getExpr())); }  in newPf()
114   kids.push_back(pf.getExpr());  in newPf()
147     kids.push_back(i->getExpr());  in newPf()
180     kids.push_back(i->getExpr());  in newPf()
194     kids.push_back(i->getExpr());  in newPf()
205     kids.push_back(i->getExpr());  in newPf()
216   kids.push_back(pf.getExpr());  in newPf()
229     kids.push_back(i->getExpr());  in newPf()
236   Expr v(label.getExpr());  in newPf()
243   return Proof(d_tm->getEM()->newClosureExpr(LAMBDA, u, pf.getExpr()));  in newPf()
248   Expr v(label.getExpr());  in newPf()
254   return Proof(d_tm->getEM()->newClosureExpr(LAMBDA, u, pf.getExpr()));  in newPf()
263     const Expr& v = labels[i].getExpr();  in newPf()
270 		"LAMBDA expression.\nExpected: "+tp.getExpr().toString()  in newPf()
271 		+"\nFound: "+v.getType().getExpr().toString());  in newPf()
274   return Proof(d_tm->getEM()->newClosureExpr(LAMBDA, u, pf.getExpr()));  in newPf()
282     const Expr& v = labels[i].getExpr();  in newPf()
288   return Proof(d_tm->getEM()->newClosureExpr(LAMBDA, u, pf.getExpr()));  in newPf()