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

At: ReflectsProp wf

P:(TermProp), qP:Term, L:(TermProp). ReflectsProp(P; qP; L) Prop

By: GenUnivCD

Generated subgoals:

11. P: TermProp
2. qP: Term
3. L: TermProp
ReflectsProp(P; qP; L) Prop
1 step
 
21. P: TermProp{i}
2. qP: Term
TermProp{i} Type{i'}
Auto
 
31. P: TermProp
Term Type
Auto
 
4 TermProp{i} Type{i'}Auto

About:
functionuniversememberpropall

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