(7steps total) PrintForm Definitions Lemmas ElisTarskiPf B Sections NuprlLIB Doc

At: reps wf 1 1
1. u: Type
2. t: u Term
3. x: u
(t IN u & ref(t) = x) Prop
By: Analyze 2
Generated subgoal:

12. t: Term
3. t IN u
4. x: u
5. t IN u
ref(t) u		1 step

About:
universeequalmemberprop

(7steps total) PrintForm Definitions Lemmas ElisTarskiPf B Sections NuprlLIB Doc