1. T : Type
2. T List
3. P : TTProp
4. x,y:T. Dec(P(x,y))
5. x,y:T. P(x,y)  P(y,x)
  Q:(TT). x,y:T. Q(x,y)  P(x,y)

By:

RenameVar `f' 4 THEN InstConcl [x,y. dec2bool(f(x,y))] THEN Reduce 0 THEN Try (All (Unfolds [`all`;`decidable`;`decision`]) THEN All (Unfold `or`) (THEN (Complete Auto) THEN Try (MoveToConcl -1 THEN GenConcl (f(x,y) = d) THEN Analyze -2 (THEN (All (h.Unfold `dec2bool` h THEN Reduce h) (THEN (Complete Auto) THEN Try (GenConcl (f(x,y) = d) THEN Analyze -2 THEN Unfold `dec2bool` 0 THEN Reduce 0)

None

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