Nuprl - Proof: reps wf2 1 1

(6steps total) PrintForm Lemmas ElisTarskiPf B Sections NuprlLIB Doc

At: reps wf2 1 1

1. t: Term
2. x: Term

(t IN Term & ref(t) = x) Prop

By: Auto

Generated subgoal:

1 3. t IN Term
is_subst0(.ref(t)) 1 step

About:

(6steps total) PrintForm Lemmas ElisTarskiPf B Sections NuprlLIB Doc