data Vec 1 = [
| mkNil { }
| mkCons { head : @(0), tail : Vec }
]
bind 1 x : {v : int | true}
bind 2 y : {v : int | true}
bind 3 xs : {v : Vec int | v = mkNil }
bind 4 ys : {v : Vec int | true}
bind 5 l1 : {v : Vec int | v = mkCons x xs }
bind 6 l2 : {v : Vec int | v = mkCons y ys }
bind 7 l3 : {v : Vec int | true }
constraint:
env [1;2;3;4;5;6]
lhs {v : int | l1 = l2 }
rhs {v : int | x = y }
id 1 tag []
constraint:
env [1;2;3;4;5;6]
lhs {v : int | l1 = l2 }
rhs {v : int | xs = ys }
id 2 tag []
constraint:
env [1;3;5;7]
lhs {v : int | l1 = l3 }
rhs {v : int | is$mkCons l3 }
id 3 tag []
constraint:
env [1;3;5;7]
lhs {v : int | l1 = l3 }
rhs {v : int | x = head l3 }
id 4 tag []
constraint:
env [1;3;5;7]
lhs {v : int | l1 = l3 }
rhs {v : int | mkNil = tail l3 }
id 5 tag []