Step * 2 of Lemma mset_sum_bor_mon_hom


1. s : DSet@i'
2. x : |s|@i
⊢ ff = ff
BY
{ Auto }


Latex:


Latex:

1.  s  :  DSet@i'
2.  x  :  |s|@i
\mvdash{}  ff  =  ff


By


Latex:
Auto




Home Index