Function prop::queenity::in_right_arg

source · 
pub fn in_right_arg<A: Prop, B: Prop, C: Prop>(
    Sq: Sq<A, B>,
    (g0, _): Eq<B, C>
) -> Sq<A, C>
Expand description

(a ¬> b) ∧ (b == c) => (a ¬> c).

Examples found in repository?
examples/sq_uniq.rs (line 24)
17
18
19
20
21
22
23
24
25
26
27
28
29
30

pub fn dominating_queen<A: Prop, B: Prop, C: Prop>(
    sq_ac: Sq<A, C>,
    uniq_sq_ab: impl UniqSq<A, B>,
    eq_q_bc: EqQ<B, C>,
) -> False {
    let eq_cb = uniq_sq_ab.uniq_sq(sq_ac.clone());
    let eq_bc = eq::symmetry(eq_cb.clone());
    let sq_ab = queenity::in_right_arg(sq_ac, eq_cb);
    let q_bc = eq_q_bc(eq_bc);
    let q_bb = quality::left(q_bc);
    let sq_bb = queenity::sq_right(sq_ab);
    let sesh_bb = queenity::to_sesh(sq_bb);
    sesh_bb(q_bb)
}