conj (<>(@c1 c2),@ c1 ([]p1 -> p2), @ c2 []p1, - @ c1 p2)