David Wang (Jan 08 2024 at 21:17): David Wang (Jan 08 2024 at 21:17):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: Dec 21 2024 at 16:20 UTC