/*
 * SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.
 * For more information, please refer to <https://unlicense.org/>
 * SPDX-License-Identifier: Unlicense
 */

/*
 * Attempt to write a proof showing
 *  (p -> q) -> p
 * but demonstrate that we do not allow that.
 */

#include "formula.h"
#include "proof.h"

int main(int argc, char **argv) {
    return proves(
        impl_intro(
            1,
            suppose(conj(var("p"), var("q")), 1)
        ),
        impl(impl(var("p"), var("q")), var("p"))
    );
}