Relax SetAdd typing rule analogously to ElementOfSet
Created by: gsps
Our typing rule for SetAdd
is currently more restrictive than necessary. Namely, we reject judgments of the form
xs : Set[T], x : S |- xs + x : Set[T]
where S <: T
while x \in xs
passes in the same typing environment. This PR relaxes the typing rule of SetAdd
to match the behavior on ElementOfSet
.