Opened 3 years ago

# Set comprehensions with patterns

Reported by: Owned by: tilk major Proof Engine

### Description

Currently, one can only write set comprehensions like this: {x \in S | F}, where x is a variable. I should be able to write any pattern there, like for example {<a,b> \in S | F}. It probably should be a syntax sugar for {x \in S | \exists a \exists b (x=<a,b> /\ F)}.

Additional requirement: if a variable occuring free in the pattern is bound in the assumptions, it should NOT be bound in the pattern.