(l1',r1') <- congruenceNewtypes l1 r1
return (mkFunTy l1' l2', mkFunTy r1' r2')
-- TyconApp Inductive case; this is the interesting bit.
(l1',r1') <- congruenceNewtypes l1 r1
return (mkFunTy l1' l2', mkFunTy r1' r2')
-- TyconApp Inductive case; this is the interesting bit.