Function cover 

pub fn cover<A: Prop, B: Prop, C: Prop, X: Prop, Y: Prop>(
    ty_a: Ty<A, B>,
    def: Pow<Or<Eq<A, X>, Eq<A, Y>>, Ty<A, B>>,
    pow_c_eq_a_x: Pow<C, Eq<A, X>>,
    pow_c_eq_a_y: Pow<C, Eq<A, Y>>,
) -> C

(a : b) ⋀ ((a == x) ⋁ (a == y))^(a : b) ⋀ c^(a == x) ⋀ c^(a == y) => c.