Fix is_prop, is_set etc. to satisfy type checking

[bvssvni]

Currently, is_prop, is_set etc. doesn't satisfy type checking, because the following is not provable:

is_prop(x, a, b) & (a => x) & (b => c) => ((a == b) => x)

This might be thought of as:

A : Type
B : Type
--------
(A -> B, B -> A) : Type

[bvssvni]

In the case of is_prop, the definition can be changed to:

pub fn is_prop(x: u64, a: u64, b: u64) -> u64 {
    imply(
        and(imply(a, x), imply(b, x)),
        imply(eq(a, b), x)
    )
}

[bvssvni]

In the case of is_set, the definition can be changed to:

/// Defines a set relation from a set `x[0]` to potential members `a` and `b`.
///
/// `x[1]` is a propositional type storing equivalences.
pub fn is_set(x: [u64; 2], a: u64, b: u64) -> u64 {
    imply(
        and(imply(a, x[0]), imply(b, x[0])),
        imply(imply(eq(a, b), x[1]), imply(eq(qubit(a), qubit(b)), x[1]))
    )
}

[bvssvni]

An alternative is to make a language trade-off in design.