Type Definition prop::path_semantics::PSemNaive

type PSemNaive<F1, F2, X1, X2> = Imply<And<Eq<F1, F2>, And<Imply<F1, X1>, Imply<F2, X2>>>, Eq<X1, X2>>;

Naive axiom of Path Semantics (without order assumption).