func (l Bool) Implies(r Bool) Bool {
	ctx := l.ctx
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_implies(ctx.c, l.c, r.c)
	})
	runtime.KeepAlive(l)
	runtime.KeepAlive(r)
	return Bool(val)
}
Implies returns a Value that is true if l implies r.
package z3
import "runtime"
import "C"
func (l Bool) Eq(r Bool) Bool {
	ctx := l.ctx
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_eq(ctx.c, l.c, r.c)
	})
	runtime.KeepAlive(l)
	runtime.KeepAlive(r)
	return Bool(val)
}
func (l Bool) NE(r Bool) Bool {
	return l.ctx.Distinct(l, r)
}
func (ctx *Context) Distinct(vals ...Value) Bool {
	cargs := make([]C.Z3_ast, len(vals)+0)
	for i, arg := range vals {
		cargs[i+0] = arg.impl().c
	}
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_distinct(ctx.c, C.uint(len(cargs)), &cargs[0])
	})
	runtime.KeepAlive(&cargs[0])
	return Bool(val)
}
func (l Bool) Not() Bool {
	ctx := l.ctx
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_not(ctx.c, l.c)
	})
	runtime.KeepAlive(l)
	return Bool(val)
}
func (cond Bool) IfThenElse(cons Value, alt Value) Value {
	ctx := cond.ctx
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_ite(ctx.c, cond.c, cons.impl().c, alt.impl().c)
	})
	runtime.KeepAlive(cond)
	runtime.KeepAlive(cons)
	runtime.KeepAlive(alt)
	return val.lift(KindUnknown)
}
func (l Bool) Iff(r Bool) Bool {
	ctx := l.ctx
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_iff(ctx.c, l.c, r.c)
	})
	runtime.KeepAlive(l)
	runtime.KeepAlive(r)
	return Bool(val)
}