dfNormalize %X :=
  let p := dfOrder X
      (es, os) := evenAndOddPermutations p
   in withSymbols [i]
        (sum (map (\σ -> subrefs X (map 1#i_(σ %1) (between 1 p))) es)
       - sum (map (\σ -> subrefs X (map 1#i_(σ %1) (between 1 p))) os))
       / fact p

antisymmetrize := dfNormalize

wedge %X %Y := X !. Y

Lie.wedge %X %Y := X !. Y - Y !. X

ι %X %Y := withSymbols [i] dfOrder Y * (X...~i . dfNormalize Y..._i)

Lie %X %Y :=
  match dfOrder Y as integer with
    | #0 -> ι X (d Y)
    | #N -> d (ι X Y)
    | _ -> ι X (d Y) + d (ι X Y)