Nuprl - Proof: fun exp add sq 2 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fun exp add sq 2 1 1 1 1

1. f : Top

, x:Top. (f^n+1(x)) ~ (f(f^n(x)))

By:	UnivCD THEN Unfold `fun_exp` 0 THEN RW (AddrC [1] (RecUnfoldC `primrec`)) 0 THEN SplitOnConclITE THENL [Auto;Id] THEN Subst ((n+1-1) ~ n) 0 THENL [Auto;Reduce 0] THEN Trivial

Generated subgoals:

None

About:

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