Function prop::path_semantics::use_pand_both [−][src]
pub fn use_pand_both<A: Prop, B: Prop, C: Prop, D: Prop>(
f: Eq<And<A, B>, D>,
g: Imply<D, C>,
p_a: PAndFst<A, B, D, C>,
p_b: PAndSnd<A, B, D, C>
) -> And<Eq<A, C>, Eq<B, C>>
Use both PAndFst
and PAndSnd
.
This results in a stronger statement than PAnd
alone.