Do not use SubsetEq class for logical entailment.
Now we use a specific notation (⊑) to whose arguments we interpret in uPred_scope. This makes notations much more concise.
This diff is collapsed.
Please register or sign in to comment
Now we use a specific notation (⊑) to whose arguments we interpret in uPred_scope. This makes notations much more concise.