Nuprl - Pf absval_elim 1 1 1

(8steps) PrintForm Definitions int 2 Sections StandardLIB Doc

At: absval elim 1 1 1

1. P: Prop
2. x:

P(if 0x x else -x fi) P(x)

By: BoolCasesOnCExp (0x) THEN AbReduce 0

Generated subgoals:

None

About:

(8steps) PrintForm Definitions int 2 Sections StandardLIB Doc