Nuprl - Proof: repst wf 1

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

At: repst wf 1

1. t: Term
2. x: Term

(t reps x) Prop

By: Unfold `repst` 0

Generated subgoal:

1 (t reps x Term) Prop 1 step

About:

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