definition full_subset: ∀s:REL. Ω^s.
- apply (λs.{x | ⊤});
+ apply (λs.{x | True});
intros; simplify; split; intro; assumption.
qed.
qed.
*)
+axiom daemon : False.
+
theorem extS_singleton:
∀o1,o2.∀a.∀x.extS o1 o2 a {(x)} = ext o1 o2 a x.
intros; unfold extS; unfold ext; unfold singleton; simplify;
split; intros 2; simplify; simplify in f;
[ cases f; cases e; cases x1; change in f2 with (x =_1 w); apply (. #‡f2); assumption;
- | split; try apply I; exists [apply x] split; try assumption; change with (x = x); apply rule #;] qed.
+ | split; try apply I; exists [apply x] split; try assumption; change with (x = x); apply rule #;] qed.
\ No newline at end of file