intro t;
constructor 1;
[ apply (Oform t);
- | apply (□_t ∘ Ext⎽t);
- | apply (◊_t ∘ Rest⎽t);
+ | apply (□⎽t ∘ Ext⎽t);
+ | apply (◊⎽t ∘ Rest⎽t);
| apply hide; intros 2; split; intro;
[ change with ((⊩) \sup ⎻* ((⊩) \sup ⎻ U) ≤ (⊩) \sup ⎻* ((⊩) \sup ⎻ V));
apply (. (#‡(lemma_10_4_a ?? (⊩) V)^-1));
apply (. (or_prop2 : ?) ^ -1);
apply oa_leq_refl; ]]
| apply hide; intros 2; split; intro;
- [ change with (◊_t ((⊩) \sup * U) ≤ ◊_t ((⊩) \sup * V));
+ [ change with (◊⎽t ((⊩) \sup * U) ≤ ◊⎽t ((⊩) \sup * V));
apply (. ((lemma_10_4_b ?? (⊩) U)^-1)‡#);
apply (f_image_monotone ?? (⊩) ? ((⊩)* V));
apply f_star_image_monotone;
apply oa_leq_refl; ]]
| apply hide; intros;
apply (.= (oa_overlap_sym' : ?));
- change with ((◊_t ((⊩)* V) >< (⊩)⎻* ((⊩)⎻ U)) = (U >< (◊_t ((⊩)* V))));
+ change with ((◊⎽t ((⊩)* V) >< (⊩)⎻* ((⊩)⎻ U)) = (U >< (◊⎽t ((⊩)* V))));
apply (.= (or_prop3 ?? (⊩) ((⊩)* V) ?));
apply (.= #‡(lemma_10_3_a : ?));
apply (.= (or_prop3 : ?)^-1);