>mf_bind >mf_bind
>(mf_comp … T) in ⊢ (?????%?);
[2: @mf_vpush_swap // |4: @exteq_refl |3,5: skip ]
>(mf_comp … T) in ⊢ (??????%);
[2: @mf_vpush_swap // |4: @exteq_refl |3,5: skip ]
>mf_bind >mf_bind
>(mf_comp … T) in ⊢ (?????%?);
[2: @mf_vpush_swap // |4: @exteq_refl |3,5: skip ]
>(mf_comp … T) in ⊢ (??????%);
[2: @mf_vpush_swap // |4: @exteq_refl |3,5: skip ]