Hello,
I cannot figure out how to solve the following question for the While case in Concrete Semantics:
lemma L_bury: "X ⊆ Y ⟹ L (bury c Y) X = L c X"
proof (induction c arbitrary: X Y)
Can someone give me a pointer?
Last updated: Feb 01 2025 at 20:19 UTC