Prove proof constraint independence

harp-project / AML-Formalization

GNU Lesser General Public License v2.1

10 stars 5 forks source link

Prove proof constraint independence #442

Open berpeti opened 2 weeks ago

berpeti commented 2 weeks ago

Suppose we have a matching logic proof, which existentially generalises over x. If we know that x is a fresh variable, prove that we can construct an equivalent proof with existentially generalises over y, which is also a fresh variable.

berpeti commented 1 week ago

Could the same idea be applied for kt and advanced_kt, if the pattern is mu-free?