fix f : !a.!b.!c.(a+b)+c=a+(b+c).

	\a:#.\b:#.\c:#.

	case c of #0 -> transE (a+b)+0 a+b a+(b+0) 
		{
			defP0 a+b
		, 
			symmE a+(b+0) a+b (thmPE a b+0 b (defP0 b))
		}

	| v' -> (transE5 (a+b)+v'
			((a+b)+v)'
			(a+(b+v))'
			 a+(b+v)'
			 a+(b+v')

			{ defPS  a+b  v
			, succE  (a+b)+v  a+(b+v)  (f a b v)
			, symmE  a+(b+v)' (a+(b+v))'  (defPS a b+v)
			, thmPE  a  (b+v)'  b+v'  (symmE b+v' (b+v)' (defPS b v))
			}
		)