liquid-fixpoint-8.10.7: tests/proof/T387.fq

// minimized version of LH #1371 

fixpoint "--rewrite"

data Thing 0 = [
       | Op { left : Thing, right : Thing}
       | N  { eNum : int}
     ]

define killer (a1 : Thing,  a2 : Thing) : Thing = {
  if (is$N a1) 
    then (if (is$N a2) then (a1) else (Op (left a2) (killer (N (eNum a1)) (right a2)))) 
    else (Op (left a1) (killer (right a1) a2))
}

constant killer : (func(0 , [Thing; Thing; Thing]))

bind 1 e2  : {v : Thing | true }
bind 2 tmp : {v : Thing | v = (killer (N 666) e2) }

expand [1 : True]

constraint:
  env [1;2]
  lhs {VV : Thing | [] }
  rhs {VV : Thing | [1 + 2 = 3]}
  id 1 tag []