At:
st app functionality
1
1.
a1: Collection(SimpleType)
2.
a2: Collection(SimpleType)
3.
b1: Collection(SimpleType)
4.
b2: Collection(SimpleType)
5.
a1 = a2
6.
b1 = b2
x:SimpleType. (
a:SimpleType. a
b1 & a
x
a1) 
(
a:SimpleType. a
b2 & a
x
a2)
By:
RW (SweepDnC (HypC -1 ORELSEC HypC -2)) 0
Generated subgoals:
None
About: