Nuprl - Proof: reps wf2 1 1 1

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

At: reps wf2 1 1 1

1. t: Term
2. x: Term
3. t IN Term

is_subst0(.ref(t))

By: FwdThru Thm* a:Term, A:Type. a IN A ref(a) A [3]

Generated subgoals:

None

About:

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