Nuprl - Pf map_map

A:Type, as:A List, f,g:Top. map(g;map(f;as)) ~ map(g o f;as)

By: Analyze 0 THEN Analyze 0 THEN ListInd -1 THEN Reduce 0 THEN UnivCD THEN Try Trivial THEN Try Analyze THEN Try Trivial THEN Try BackThruSomeHyp

Generated subgoals:

None

About: