A lean4 implementation attempt of Pijul