At:
tc pred monotone
1
1.
p1: Fmla
2.
p2: Fmla
3.
ds1: Collection(dec())
4.
ds2: Collection(dec())
5.
da1: Collection(SimpleType)
6.
da2: Collection(SimpleType)
7.
de: sig()
8.
p2 
p1
9.
ds1 ds2
10.
da1 da2
11.
r:rel(). r 
p1 
tc(r;ds1;da1;de)
12.
r: rel()
13.
r p2
r p1
By:
AllHyps (
i.(Unfold `col_le` i) THEN (BackThru i) THEN Trivial)
Generated subgoals:
None
About:
