Type Definition prop::path_semantics::PAnd

type PAnd<A, B, C, D> = Imply<And<Eq<And<A, B>, C>, Imply<C, D>>, Eq<And<A, B>, D>>;

Sends Logical AND to higher level.