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

At: RepsTruth wf

Tr:(TermProp), tr:Term, L:(TermProp). RepsTruth(L; Tr; tr) Prop

By: GenUnivCD

Generated subgoals:

11. Tr: TermProp
2. tr: Term
3. L: TermProp
RepsTruth(L; Tr; tr) Prop
1 step
 
21. Tr: TermProp{i}
2. tr: Term
TermProp{i} Type{i'}
Auto
 
31. Tr: TermProp
Term Type
Auto
 
4 TermProp{i} Type{i'}Auto

About:
functionuniversememberpropall

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