Nuprl - Proof: fappend-increasing

n,m:, f:((n-1)(m-1)). increasing(f;n-1) increasing(f[n-1:=m-1];n)

By: Auto THEN ParallelOp -1 THEN Unfold `fappend` 0 THEN Reduce 0 THEN SplitOnConclITE THEN SplitOnConclITE THEN EasyHyp'

Generated subgoals:

None

About: