Function prop::path_semantics::use_pand_both

pub fn use_pand_both<A: Prop, B: Prop, C: Prop, D: Prop>(
    f: Q<And<A, B>, D>, 
    g: Imply<D, C>, 
    p_a: PAndFst<A, B, D, C>, 
    p_b: PAndSnd<A, B, D, C>
) -> And<Q<A, C>, Q<B, C>>

Use both PAndFst and PAndSnd.

This results in a stronger statement than PAnd alone.