At:
st app monotone
1
1.
a1: Collection(SimpleType)
2.
a2: Collection(SimpleType)
3.
b1: Collection(SimpleType)
4.
b2: Collection(SimpleType)
5.
x:SimpleType. x 
a1 
x a2
6.
x:SimpleType. x b1 x b2
7.
x: SimpleType
8.
a:SimpleType. a b1 & a
x a1
a:SimpleType. a b2 & ax a2
By:
ExRepD
THEN
InstConcl [a]
THEN
SmAuto
Generated subgoals:
None
About:
