fun ifact2 {n:nat} .<>. (n : int(n)) :<> [r:int] (FACT(n, r) | int(r)) =
  let
    fun loop { i : nat | i <= n }{r:int} .<n-i>. (pf : FACT(i, r)
                                                 | n : int(n), i : int(i), r : int(r)) :<>
      [r:int] (FACT(n, r) | int(r)) =
      if n - i > 0 then
        let
          val (pfmul | r1) = imul2((i + 1, r))
        in
          loop(FACTind(pf, pfmul) | n, i + 1, r1)
        end
      else
        (pf | r)
    
    // end of [if]
    // end of [loop]
  in
    loop(FACTbas() | n, 0, 1)
  end

// end of [ifact2]