(2steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: delete fenum value is inj gen

  P,Q:(Prop), f:({u:P(u) }{v:Q(v) }).
  Inj({u:P(u) }; {v:Q(v) }; f)
  
  (m:{u:P(u) }, k:{v:Q(v) }.
  (Inj({u:P(u) & u = m }; {v:Q(v) & v = k };
  (Inj(Replace value k by f(m) in f))


By: SimilarTo: Thm: delete fenum value is inj genW


Generated subgoal:

1 1. P : Prop
2. Q : Prop
3. f : {u:P(u) }{v:Q(v) }
4. Inj({u:P(u) }; {v:Q(v) }; f)
5. m : {u:P(u) }
6. k : {v:Q(v) }
7. (Replace value k by f(m) in f {u:P(u) & u = m }{v:Q(v) & v = k }
7. & Inj({u:P(u) & u = m }; {v:Q(v) & v = k };
7. & Inj(Replace value k by f(m) in f)
  Inj({u:P(u) & u = m }; {v:Q(v) & v = k };
  Inj(Replace value k by f(m) in f)

1 step

About:
intsetfunctionequalmemberpropimpliesandall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(2steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc