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

At: reps wf

u:Type, t:(u Term), x:u. (t reps x u) Prop

By: GenUnivCD

Generated subgoals:

11. u: Type
2. t: u Term
3. x: u
(t reps x u) Prop
3 steps
 
21. u: Type
2. t: u Term
u Type
Auto
 
31. u: Type
(u Term) Type
Auto
 
4 Type{i} Type{i'}Auto

About:
universememberpropall

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