Nuprl - Proof: card split prod intseg family 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card split prod intseg family 1

1. a :

2. b :

3. c : {a...b}
4. B : {a..b

}

Type

(i:{a..b

}

B(i)) ~ ((i:{a..c

}

B(i))

(i:{c..b

}

B(i)))

By:	Use:[A:= {a..b} \| P(i):= i<c] Inst: Thm* (x:A. Dec(P(x))) Thm* Thm* ((x:AB(x)) ~ ((x:A st P(x)B(x))(x:A st P(x)B(x)))) THEN Rewrite by Hyp:-1

Generated subgoal:

1   ((i:{a..b} st i<cB(i))(i:{a..b} st i<cB(i)))
  ~
  ((i:{a..c}B(i))(i:{c..b}B(i)))
3 steps

About:

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