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: Apr 27 2024 at 20:14 UTC