liquid-fixpoint-0.9.6.3.2: tests/pos/ext_double_unfold.fq
fixpoint "--rewrite"
fixpoint "--extensionality"
constant f : (func(0 , [int; int]))
define f (x : int) : int = {(13)}
constant g : (func(0, [int; int; int]))
define g (a : int, b : int) : int = {(f b)}
constant k : (func(0, [int; int; int]))
define k (u : int, m : int) : int = {(13)}
expand [1 : True; 2 : True]
constraint:
env []
lhs {VV1 : Tuple | true }
rhs {VV2 : Tuple | (g = k) }
id 1 tag []