At: col member functionality T:Type, c1,c2:Collection(T), t1,t2:T. t1 = t2 c1 = c2 (t1 c1 t2 c2) By: Unfold `col_equal` 0
THEN
BackThruSomeHyp
THEN
AllHyps (i.(HypSubst i -1) THEN (Complete Auto))
THEN
AllHyps (i.(RevHypSubst i -1) THEN (Complete Auto)) Generated subgoals:
T:Type, c1,c2:Collection(T), t1,t2:T. t1 = t2 
c1 = c2 
c1 
i.(HypSubst i -1) THEN (Complete Auto))