-conj (<>@c1 c2,  @ c1 (<>p -> p1), @ c2 <>p, - @ c1 p1)