Ex4.15

excersise.4.15.als

sig A{
    S: set A
}

fun id_A : A -> A{
    A -> A & iden
}
pred Simple{
    ~S.S in id_A
}

pred Entire{
    id_A in S.~S
}

pred Ex415{
		S.~S.S = S
}

assert Ex415'{
		Simple[] implies Ex415[]
}

check Ex415'

pred show{
    not Simple[] and Ex415[]
}

run show