p1,p2:Fmla, ds1,ds2:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(). p1 = p2 ds1 = ds2 da1 = da2 (tc_pred(p1;ds1;da1;de) tc_pred(p2;ds2;da2;de))

let T Auto THEN (Try (Fold `pred` 0)) in (((Unfold `tc_pred` 0) THEN UnivCD) THEN (RW (SweepDnC (FirstC (map HypC [-1;-2;-3]))) 0) THEN RelRST) THEN T

None

About: