transformation ``apply`` should consider ``let`` as a premise
In the following example, I can do apply A
but not apply B
. It would be nicer if apply
considers the let
as a premise of the property to apply
function f int : int
predicate p int int
axiom A: forall x y. x = f y -> p x y
axiom B: forall y. let x = f y in p x y
goal g : p 17 42