fixpoint "--rewrite"

constant len: (func(1, [(Main.List  @(0)); int]))
constant Cons: (func(2, [@(0); (Main.List  @(0)); (Main.List @(0))]))
constant Nil: (Main.List @(0))

match len Nil = 0
match len Cons x xs = (1 + len xs)

constraint:
  env []
  lhs {v : int | true }
  rhs {v : int | len (Cons 1 (Cons 2 (Cons 3 Nil))) = 3}
  id 1 tag []

expand [1 : True]