Type Definition prop::path_semantics::PAndFst

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

Sends first argument of Logical AND to higher level.