data LL 1 = [
  | emp { }
  | con { lHead : @(0), lTail : LL @(0) }
]

bind 1 n1 : {n:int | true}
bind 2 m1 : {m:int | true}
bind 3 n2 : {n:int | true}
bind 4 m2 : {m:int | true}

constraint:
  env [1; 2; 3; 4]
  lhs {v:int | (con n1 (con n2 emp) = con m1 (con m2 emp)) }
  rhs {v:int | n1 = m1 && n2 = m2 }
  id 0 tag []