eq-refl
Theorem.
Arguments:
(coll),
Assertions:
(
)
Proof:
Hyp
Ref
Line
Expr
sub-refl
1
(
)
1
>andi
2
((
)
(
))
2
eq.sub
3
(
)
(coll), (coll), 
)
))
()))