pub type PSemNaive<F1, F2, X1, X2> = Imply<And<Q<F1, F2>, And<Imply<F1, X1>, Imply<F2, X2>>>, Q<X1, X2>>;
Expand description

Naive axiom of Path Semantics (without order assumption).