- x1...xn are bound in E and P, H is bound in P
- H is an identifier that will have the type of E in P
- P is the proof that the two existentially quantified predicates are equal*)
- x1...xn are bound in E and P, H is bound in P
- H is an identifier that will have the type of E in P
- P is the proof that the two existentially quantified predicates are equal*)