The distributivity of multiplication over addition means that the following equation holds

for m, n1 and n2 ranging over integers. A direct encoding of the equation is given by the following (proof) function interface:// prfun mul_distribute {m,n1,n2:int}{p1,p2:int} (MUL(m, n1, p1), MUL(m, n2, p2)): MUL(m, n1+n2, p1+p2) //

primplement mul_distribute {m,n1,n2}{p1,p2} (pf1, pf2) = let // prfun auxnat {m:nat}{p1,p2:int} .<m>. ( pf1: MUL(m, n1, p1), pf2: MUL(m, n2, p2) ) : MUL(m, n1+n2, p1+p2) = ( case+ (pf1, pf2) of | (MULbas(), MULbas()) => MULbas() | (MULind pf1, MULind pf2) => MULind(auxnat (pf1, pf2)) ) (* end of [auxnat] *) // in // sif m >= 0 then ( auxnat (pf1, pf2) ) // end of [then] else let prval MULneg(pf1) = pf1 prval MULneg(pf2) = pf2 in MULneg(auxnat (pf1, pf2)) end // end of [else] // end // end of [mul_distribute]