IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
is prime factorization wf a,b:, f:({a..b}). is_prime_factorization(a; b; f) Prop
By:
Def of is_prime_factorization(<term>; <term>; <term>)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
a,b:
, f:({a..b
}
). is_prime_factorization(a; b; f) 
Prop
