Nuprl - Proof: mapoutl append

A,B:Type, L1,L2:(A+B) List. mapoutl(L1 @ L2) ~ (mapoutl(L1) @ mapoutl(L2))

By: InductionOnList THEN Reduce 0 THEN Analyze 0 THEN Analyze 4 THEN Reduce 0 THEN EasyHyp THEN Analyze THEN EasyHyp

Generated subgoals:

None

About: