Email Gateway (Feb 03 2023 at 10:46): Email Gateway (Feb 03 2023 at 10:46):From: "YAMADA, Akihisa" <ayamada@trs.cm.is.nagoya-u.ac.jp>
Dear list,
there is this (very reasonable) line in Set.thy:
lemma subset_antisym [intro!]: "A ⊆ B ⟹ B ⊆ A ⟹ A = B"
I guess this is not immediately applicable to a goal like:
lemma "(A::'a set) ≠ B ⟹ foo"
However,
apply safe_step
yields these subgoals:
1. ¬ foo ⟹ A ⊆ B
2. ¬ foo ⟹ B ⊆ A
while
apply (safe del: subset_antisym)
fails.
Is this expected?
Best,
Akihisa
Last updated: Apr 20 2024 at 01:05 UTC