/*

Congruence

There are two forms of congruence: Normal congruence and tautological congruence.

Normal congruence for `f`:

    (a == b) -> f(a) == f(b)

Tautological congruence for `f`:

    (a == b)^true -> f(a) == f(b)

Most operators are normal congruent.
All normal congruent operators are tautological congruent.

In some theories, normal congruence is assumed.
This limits the theories to what they can express.

In Path Semantics, some operators are tautological congruent, but not normal congruent.
For example, path semantical quality and symbolic distinction.

Normal congruence might be thought of as a kind of dynamic invariance.
The type `a == b` might have a proof at run-time, but not necessary at compile-time.

Tautological congruence might be thought of as a akind of static invariance.
The type `(a == b)^true` might have a proof at compile-time.
However, this is a loose analogy, since `(a == b)^true` might be assumed at run-time.

If you find this hard to reason about, then you are not the only one.

It can be confusing to try understand nuances like:

    tauto_cong'(f)      vs      tauto_cong'(f)^true

E.g. in `tauto_cong_eq_left`.

Compared to normal congruence, tautological congruence harder for the human brain.
Sometimes it is best to leave it up to HOOO EP to figure out what is true.
Path Semanticists are used to things being hard to think about,
so they try not to overthink too much, but instead building an intuition over time.

HOOO EP was designed specificially to deal with foundations of Path Semantics.
The motivation of this development came from realizing that some operators
are tautological congruent but not normal congruent.

*/

sym cong;
sym tauto_cong;

fn tauto_cong_sym :
    true -> tauto_cong'(sym(f, all((a == b)^true -> f'(a) == f'(b))))
{
    axiom tauto_cong_sym :
        true -> tauto_cong'(sym(f, all((a == b)^true -> f'(a) == f'(b))));
    x : true;
    let r = tauto_cong_sym(x) :
        tauto_cong'(sym(f, all((a == b)^true -> f'(a) == f'(b))));
    return r;
}

fn cong_app : cong'(f) & (f : t1 => t2 => t3) -> cong'(f(a)) {
    axiom cong_app : cong'(f) & (f : t1 => t2 => t3) -> cong'(f(a));
    x : cong'(f) & (f : t1 => t2 => t3);
    let r = cong_app(x) : cong'(f(a));
    return x;
}

fn tauto_cong_app : tauto_cong'(f) & (f : t1 => t2 => t3) -> tauto_cong'(f(a)) {
    axiom tauto_cong_app : tauto_cong'(f) & (f : t1 => t2 => t3) -> tauto_cong'(f(a));
    x : tauto_cong'(f) & (f : t1 => t2 => t3);
    let r = tauto_cong_app(x) : tauto_cong'(f(a));
    return r;
}

fn cong_fun_eq : cong'(f) & cong'(g) & (f == g) -> f(a) == g(a) {
    axiom cong_fun_eq : cong'(f) & cong'(g) & (f == g) -> f(a) == g(a);
    x : cong'(f) & cong'(g) & (f == g);
    let r = cong_fun_eq(x) : f(a) == g(a);
    return r;
}

fn cong_fun_bin_eq :
    cong'(f) &
    cong'(g) &
    (f : t1 => t2 => t3) &
    (f == g) ->
    f(a, b) == g(a, b)
{
    use cong_app;
    use cong_fun_eq;
    use ty_in_left_arg;
    
    x : cong'(f);
    y : cong'(g);
    z : (f : t1 => t2 => t3);
    w : f == g;

    let z2 = ty_in_left_arg(z, w) : (g : t1 => t2 => t3);
    let x2 = cong_app(x, z) : cong'(f(a));
    let y2 = cong_app(y, z2) : cong'(g(a));
    let w2 = cong_fun_eq(x, y, w) : f(a) == g(a);
    let r = cong_fun_eq(x2, y2, w2) : f(a, b) == g(a, b);
    return r;
}

fn tauto_cong_fun_eq : tauto_cong'(f) & tauto_cong'(g) & (f == g)^true -> f(a) == g(a) {
    axiom tauto_cong_fun_eq : tauto_cong'(f) & tauto_cong'(g) & (f == g)^true -> f(a) == g(a);
    x : tauto_cong'(f) & tauto_cong'(g) & (f == g)^true;
    let r = tauto_cong_fun_eq(x) : f(a) == g(a);
    return r;
}

fn cong_sym_def : true -> cong' == sym(f, all(a == b -> f'(a) == f'(b))) {
    axiom cong_sym_def : true -> cong' == sym(f, all(a == b -> f'(a) == f'(b)));
    x : true;
    let r = cong_sym_def(x) : cong' == sym(f, all(a == b -> f'(a) == f'(b)));
    unsafe return r;
}

fn cong_def : true -> cong'(f) == sym(f, all(a == b -> f'(a) == f'(b)))(f) {
    use cong_cong;
    use cong_fun_eq;
    use cong_sym;
    use cong_sym_def;
    use triv;

    x : true;

    let x2 = triv(cong_sym_def) : cong' == sym(f, all(a == b -> f'(a) == f'(b)));
    let x3 = triv(cong_cong) : cong'(cong');
    let x4 = triv(cong_sym) : cong'(sym(f, all(a == b -> f'(a) == f'(b))));
    let r = cong_fun_eq(x3, x4, x2) :
        cong'(f) == sym(f, all(a == b -> f'(a) == f'(b)))(f);
    unsafe return r;
}

fn cong_to : cong'(f) -> sym(f, all(a == b -> f'(a) == f'(b)))(f) {
    use cong_def;
    use eq_to_right;
    use triv;

    x : cong'(f);

    let x2 = triv(cong_def) : cong'(f) == sym(f, all(a == b -> f'(a) == f'(b)))(f);
    let r = eq_to_right(x2, x) : sym(f, all(a == b -> f'(a) == f'(b)))(f);
    unsafe return r;
}

fn cong_from : sym(f, all(a == b -> f'(a) == f'(b)))(f) -> cong'(f) {
    use cong_def;
    use eq_to_left;
    use triv;

    x : sym(f, all(a == b -> f'(a) == f'(b)))(f);

    let x2 = triv(cong_def) : cong'(f) == sym(f, all(a == b -> f'(a) == f'(b)))(f);
    let r = eq_to_left(x2, x) : cong'(f);
    return r;
}

fn tauto_cong_to : tauto_cong'(f) -> sym(f, all((a == b)^true -> f'(a) == f'(b)))(f) {
    axiom tauto_cong_to : tauto_cong'(f) -> sym(f, all((a == b)^true -> f'(a) == f'(b)))(f);
    x : tauto_cong'(f);
    let r = tauto_cong_to(x) : sym(f, all((a == b)^true -> f'(a) == f'(b)))(f);
    unsafe return r;
}

fn tauto_cong_from : sym(f, all((a == b)^true -> f'(a) == f'(b)))(f) -> tauto_cong'(f) {
    axiom tauto_cong_from : sym(f, all((a == b)^true -> f'(a) == f'(b)))(f) -> tauto_cong'(f);
    x : sym(f, all((a == b)^true -> f'(a) == f'(b)))(f);
    let r = tauto_cong_from(x) : tauto_cong'(f);
    return r;
}

fn cong_eq_to_tauto_eq : sym(f, all(a == b -> f'(a) == f'(b)))(f) ->
    sym(f, all((a == b)^true -> f'(a) == f'(b)))(f)
{
    axiom cong_eq_to_tauto_eq : sym(f, all(a == b -> f'(a) == f'(b)))(f) ->
        sym(f, all((a == b)^true -> f'(a) == f'(b)))(f);
    x : sym(f, all(a == b -> f'(a) == f'(b)))(f);
    let r = cong_eq_to_tauto_eq(x) : sym(f, all((a == b)^true -> f'(a) == f'(b)))(f);
    unsafe return r;
}

fn cong_to_tauto_cong : cong'(f) -> tauto_cong'(f) {
    use cong_to;
    use cong_eq_to_tauto_eq;
    use tauto_cong_from;

    x : cong'(f);

    let x2 = cong_to(x) : sym(f, all((a == b) -> (f'(a) == f'(b))))(f);
    let x3 = cong_eq_to_tauto_eq(x2) : sym(f, all((a == b)^true -> (f'(a) == f'(b))))(f);
    let r = tauto_cong_from(x3) : tauto_cong'(f);
    return r;
}

fn cong_app_eq : cong'(f) & (a == b) -> f(a) == f(b) {
    use cong_to;

    x : cong'(f);
    y : a == b;

    let x2 = cong_to(x) : sym(f, (a == b) -> (f'(a) == f'(b)))(f);
    let x3 = x2() : (a == b) -> f(a) == f(b);
    let r = x3(y) : f(a) == f(b);
    return r;
}

fn tauto_cong_app_eq : tauto_cong'(f) & (a == b)^true -> f(a) == f(b) {
    use tauto_cong_to;

    x : tauto_cong'(f);
    y : (a == b)^true;

    let x2 = tauto_cong_to(x) : sym(f, (a == b)^true -> f'(a) == f'(b))(f);
    let x3 = x2() : (a == b)^true -> f(a) == f(b);
    let r = x3(y) : f(a) == f(b);
    return r;
}

fn cong_app_in_arg : cong'(f) & (f(a) == b) & (a == c) -> (f(c) == b) {
    use cong_app_eq;
    use eq_transitivity_rev_sym;

    x : cong'(f);
    y : f(a) == b;
    z : a == c;

    let x2 = cong_app_eq(x, z) : f(a) == f(c);
    let r = eq_transitivity_rev_sym(x2, y) : f(c) == b;
    return r;
}

fn tauto_cong_app_in_arg :
    tauto_cong'(f) & (f(a) == b) & (a == c)^true -> (f(c) == b)
{
    use tauto_cong_app_eq;
    use eq_transitivity_rev_sym;

    x : tauto_cong'(f);
    y : f(a) == b;
    z : (a == c)^true;

    let x2 = tauto_cong_app_eq(x, z) : f(a) == f(c);
    let r = eq_transitivity_rev_sym(x2, y) : f(c) == b;
    return r;
}

fn cong_in_arg : cong'(f) & (f == g) -> cong'(g) {
    axiom cong_in_arg : cong'(f) & (f == g) -> cong'(g);
    x : cong'(f) & (f == g);
    let r = cong_in_arg(x) : cong'(g);
    return r;
}

fn cong_eq : (f == g) -> cong'(f) == cong'(g) {
    use cong_in_arg;
    use eq_symmetry;
    use refl;

    x : f == g;

    let y = eq_symmetry(x) : g == f;
    lam x2 : cong'(f) => cong'(g) {
        y2 : cong'(f);
        let r = cong_in_arg(y2, x) : cong'(g);
        return r;
    }
    lam x3 : cong'(g) => cong'(f) {
        y2 : cong'(g);
        let r = cong_in_arg(y2, y) : cong'(f);
        return r;
    }
    let r = refl(x2, x3) : cong'(f) == cong'(g);
    return r;
}

fn tauto_cong_in_arg : tauto_cong'(f) & (f == g)^true -> tauto_cong'(g) {
    use tauto_cong_app_eq;
    use tauto_cong_from;
    use tauto_cong_sym;
    use tauto_cong_to;
    use fst;
    use triv;

    x : tauto_cong'(f);
    y : (f == g)^true;

    let x2 = tauto_cong_to(x) : sym(f, all((a == b)^true -> f'(a) == f'(b)))(f);
    let x3 = triv(tauto_cong_sym) : tauto_cong'(sym(f, all((a == b)^true -> f'(a) == f'(b))));
    let x5 = tauto_cong_app_eq(x3, y) :
        sym(f, all((a == b)^true -> f'(a) == f'(b)))(f) ==
        sym(f, all((a == b)^true -> f'(a) == f'(b)))(g);
    let x6 = fst(x5) :
        sym(f, all((a == b)^true -> f'(a) == f'(b)))(f) =>
        sym(f, all((a == b)^true -> f'(a) == f'(b)))(g);
    let x7 = x6(x2) : sym(f, all((a == b)^true -> f'(a) == f'(b)))(g);
    let x8 = x7() : sym(g, all((a == b)^true -> g'(a) == g'(b)))(g);
    let r = tauto_cong_from(x8) : tauto_cong'(g);
    return r;
}

fn cong_eq_left : cong'(f) & (f : t1 => t2 => t3) & (a == b) -> f(a, c) == f(b, c) {
    use cong_app;
    use cong_app_eq;
    use cong_fun_eq;

    x : cong'(f);
    f_ty : (f : t1 => t2 => t3);
    y : a == b;

    let x2 = cong_app(x, f_ty) : cong'(f(a));
    let x3 = cong_app(x, f_ty) : cong'(f(b));
    let x4 = cong_app_eq(x, y) : f(a) == f(b);
    let r = cong_fun_eq(x2, x3, x4) : f(a, c) == f(b, c);
    return r;
}

/// Notice that the first argument is tautological.
/// This is needed because otherwise one can not prove `(f(a) == f(b))^true`.
fn tauto_cong_eq_left :
    tauto_cong'(f)^true & (f : t1 => t2 => t3) & (a == b)^true -> f(a, c) == f(b, c)
{
    use hooo_rev_and;
    use pow_lift;
    use pow_transitivity;
    use tauto_cong_app;
    use tauto_cong_app_eq;
    use tauto_cong_fun_eq;
    use triv;

    x : tauto_cong'(f)^true;
    f_ty : (f : t1 => t2 => t3);
    y : (a == b)^true;

    let z = triv(x) : tauto_cong'(f);
    let y2 = pow_lift(y) : ((a == b)^true)^true;
    let x2 = hooo_rev_and(x, y2) : (tauto_cong'(f) & (a == b)^true)^true;
    let y3 = pow_transitivity() :
        (tauto_cong'(f) & (a == b)^true)^true &
        (f(a) == f(b))^(tauto_cong'(f) & (a == b)^true) ->
        (f(a) == f(b))^true;
    let x3 = y3(x2, tauto_cong_app_eq) : (f(a) == f(b))^true;
    let x4 = tauto_cong_app(z, f_ty) : tauto_cong'(f(a));
    let x5 = tauto_cong_app(z, f_ty) : tauto_cong'(f(b));
    let r = tauto_cong_fun_eq(x4, x5, x3) : f(a, c) == f(b, c);
    return r;
}

fn cong_eq_right : cong'(f) & (f : t1 => t2 => t3) & (a == b) -> f(c, a) == f(c, b) {
    use cong_app;
    use cong_app_eq;

    x : cong'(f);
    f_ty : (f : t1 => t2 => t3);
    y : a == b;

    let x2 = cong_app(x, f_ty) : cong'(f(c));
    let r = cong_app_eq(x2, y) : f(c, a) == f(c, b);
    return r;
}

fn tauto_cong_eq_right :
    tauto_cong'(f) & (f : t1 => t2 => t3) & (a == b)^true -> f(c, a) == f(c, b)
{
    use tauto_cong_app;
    use tauto_cong_app_eq;

    x : tauto_cong'(f);
    f_ty : (f : t1 => t2 => t3);
    y : (a == b)^true;

    let x2 = tauto_cong_app(x, f_ty) : tauto_cong'(f(c));
    let r = tauto_cong_app_eq(x2, y) : f(c, a) == f(c, b);
    return r;
}

fn cong_eq_both :
    cong'(f) & (f : t1 => t2 => t3) & (a == b) & (c == d) -> f(a, c) == f(b, d)
{
    use cong_eq_left;
    use cong_eq_right;
    use eq_transitivity;

    x : cong'(f);
    f_ty : (f : t1 => t2 => t3);
    y : a == b;
    z : c == d;

    let x2 = cong_eq_left(x, f_ty, y) : f(a, c) == f(b, c);
    let x3 = cong_eq_right(x, f_ty, z) : f(b, c) == f(b, d);
    let r = eq_transitivity(x2, x3) : f(a, c) == f(b, d);
    return r;
}

fn tauto_cong_eq_both :
    tauto_cong'(f)^true &
    (f : t1 => t2 => t3) &
    (a == b)^true &
    (c == d)^true ->
    f(a, c) == f(b, d)
{
    use eq_transitivity;
    use tauto_cong_eq_left;
    use tauto_cong_eq_right;
    use triv;

    x : tauto_cong'(f)^true;
    f_ty : (f : t1 => t2 => t3);
    y : (a == b)^true;
    z : (c == d)^true;

    let triv_x = triv(x) : tauto_cong'(f);
    let x2 = tauto_cong_eq_left(x, f_ty, y) : f(a, c) == f(b, c);
    let x3 = tauto_cong_eq_right(triv_x, f_ty, z) : f(b, c) == f(b, d);
    let r = eq_transitivity(x2, x3) : f(a, c) == f(b, d);
    return r;
}

fn cong_in_left_arg : cong'(f) & (f : t1 => t2 => t3) & f(a, b) & (a == c) -> f(c, b) {
    use cong_eq_left;
    use fst;

    x : cong'(f);
    f_ty : (f : t1 => t2 => t3);
    y : f(a, b);
    z : a == c;

    let x2 = cong_eq_left(x, f_ty, z) : f(a, b) == f(c, b);
    let x3 = fst(x2) : f(a, b) => f(c, b);
    let r = x3(y) : f(c, b);
    return r;
}

fn tauto_cong_in_left_arg :
    tauto_cong'(f)^true & (f : t1 => t2 => t3) & f(a, b) & (a == c)^true -> f(c, b)
{
    use fst;
    use tauto_cong_eq_left;

    x : tauto_cong'(f)^true;
    f_ty : (f : t1 => t2 => t3);
    y : f(a, b);
    z : (a == c)^true;

    let x2 = tauto_cong_eq_left(x, f_ty, z) : f(a, b) == f(c, b);
    let x3 = fst(x2) : f(a, b) => f(c, b);
    let r = x3(y) : f(c, b);
    return r;
}

fn cong_in_right_arg : cong'(f) & (f : t1 => t2 => t3) & f(a, b) & (b == c) -> f(a, c) {
    use cong_eq_right;
    use fst;

    x : cong'(f);
    f_ty : (f : t1 => t2 => t3);
    y : f(a, b);
    z : b == c;

    let x2 = cong_eq_right(x, f_ty, z) : f(a, b) == f(a, c);
    let x3 = fst(x2) : f(a, b) => f(a, c);
    let r = x3(y) : f(a, c);
    return r;
}

fn tauto_cong_in_right_arg :
    tauto_cong'(f) & (f : t1 => t2 => t3) & f(a, b) & (b == c)^true -> f(a, c)
{
    use fst;
    use tauto_cong_eq_right;

    x : tauto_cong'(f);
    f_ty : (f : t1 => t2 => t3);
    y : f(a, b);
    z : (b == c)^true;

    let x2 = tauto_cong_eq_right(x, f_ty, z) : f(a, b) == f(a, c);
    let x3 = fst(x2) : f(a, b) => f(a, c);
    let r = x3(y) : f(a, c);
    return r;
}

fn cong_in_both_args :
    cong'(f) & (f : t1 => t2 => t3) & f(a, b) & (a == c) & (b == d) -> f(c, d)
{
    use cong_in_left_arg;
    use cong_in_right_arg;

    x : cong'(f);
    f_ty : (f : t1 => t2 => t3);
    y : f(a, b);
    z : a == c;
    w : b == d;

    let x2 = cong_in_left_arg(x, f_ty, y, z) : f(c, b);
    let r = cong_in_right_arg(x, f_ty, x2, w) : f(c, d);
    return r;
}

fn tauto_cong_in_both_args :
    tauto_cong'(f)^true &
    (f : t1 => t2 => t3) &
    f(a, b) & (a == c)^true &
    (b == d)^true ->
    f(c, d)
{
    use tauto_cong_in_left_arg;
    use tauto_cong_in_right_arg;
    use triv;

    x : tauto_cong'(f)^true;
    f_ty : (f : t1 => t2 => t3);
    y : f(a, b);
    z : (a == c)^true;
    w : (b == d)^true;

    let x2 = triv(x) : tauto_cong'(f);
    let x3 = tauto_cong_in_left_arg(x, f_ty, y, z) : f(c, b);
    let r = tauto_cong_in_right_arg(x2, f_ty, x3, w) : f(c, d);
    return r;
}

fn cong_sym_id : true -> cong'(sym(a, a')) {
    use cong_from;
    use refl;
    
    x : true;

    let x2 = refl() : all(a == b -> a == b);
    let x3 = x2() : all(a == b -> sym(a, a')(a) == sym(a, a')(b));
    let x4 = x3() : sym(f, all(a == b -> f'(a) == f'(b)))(sym(a, a'));
    let r = cong_from(x4) : cong'(sym(a, a'));
    return r;
}

fn cong_cong : true -> cong'(cong') {
    axiom cong_cong : true -> cong'(cong');
    x : true;
    let r = cong_cong(x) : cong'(cong');
    return r;
}

fn cong_sym : true -> cong'(sym(f, all(a == b -> f'(a) == f'(b)))) {
    use cong_cong;
    use cong_in_arg;
    use cong_sym_def;

    x : true;

    let x2 = cong_cong(x) : cong'(cong');
    let x3 = cong_sym_def(x) :
        cong' == sym(f, all(a == b -> f'(a) == f'(b)));
    let r = cong_in_arg(x2, x3) :
        cong'(sym(f, all(a == b -> f'(a) == f'(b))));
    return r;
}

fn cong_bin :
    cong'(f) & cong'(g) & cong'(h) -> cong'(sym(a, h(f(a'), g(a'))))
{
    use comp_cong;
    use comp_tup_sym_def;
    use cong_in_arg;
    use tup_cong;
    use triv;

    x : cong'(f);
    y : cong'(g);
    z : cong'(h);

    let x2 = tup_cong(x, y) : cong'((f, g));
    let x3 = comp_cong(z, x2) : cong'((h . (f, g)));
    let x4 = triv(comp_tup_sym_def) : (h . (f, g)) == sym(a, h(f(a'), g(a')));
    let r = cong_in_arg(x3, x4) : cong'(sym(a, h(f(a'), g(a'))));
    return r;
}

fn cong_bin_fst : cong'(f) & cong'(h) -> cong'(sym(a, h(f(a'), a'))) {
    use comp_cong;
    use comp_tup_sym_def;
    use cong_in_arg;
    use cong_sym_id;
    use triv;
    use tup_cong;

    x : cong'(f);
    z : cong'(h);

    let x2 = triv(cong_sym_id) : cong'(sym(a, a'));
    let x3 = tup_cong(x, x2) : cong'((f, sym(a, a')));
    let x4 = comp_cong(z, x3) : cong'((h . (f, sym(a, a'))));
    let x5 = triv(comp_tup_sym_def) :
        (h . (f, sym(a, a'))) == sym(a, h(f(a'), sym(a, a')(a')));
    let x6 = x5() : (h . (f, sym(a, a'))) == sym(a, h(f(a'), a'));
    let r = cong_in_arg(x4, x6) : cong'(sym(a, h(f(a'), a')));
    return r;
}

fn cong_bin_and : cong'(f) & cong'(g) -> cong'(sym(a, f(a') & g(a'))) {
    use and_cong;
    use cong_bin;
    use cong_in_arg;
    use prop_and;
    use sym_eq;
    use triv;

    x : cong'(f);
    y : cong'(g);

    let z = triv(and_cong) : cong'(prop_and');
    let z2 = cong_bin(x, y, z) : cong'(sym(a, prop_and'(f(a'), g(a'))));
    fn x2 : sym a  ->  prop_and'(f(a'), g(a')) == (f(a') & g(a')) {
        sym a;
        use and_def;
        use triv;
        let r = triv(and_def) : prop_and'(f(a'), g(a')) == (f(a') & g(a'));
        return r;
    }
    let y2 = sym_eq(x2) : sym(a, prop_and'(f(a'), g(a'))) == sym(a, f(a') & g(a'));
    let r = cong_in_arg(z2, y2) : cong'(sym(a, f(a') & g(a')));
    return r;
}

fn cong_bin_or : cong'(f) & cong'(g) -> cong'(sym(a, f(a') | g(a'))) {
    use or_cong;
    use cong_bin;
    use cong_in_arg;
    use prop_or;
    use sym_eq;
    use triv;

    x : cong'(f);
    y : cong'(g);

    let z = triv(or_cong) : cong'(prop_or');
    let z2 = cong_bin(x, y, z) : cong'(sym(a, prop_or'(f(a'), g(a'))));
    fn x2 : sym a  ->  prop_or'(f(a'), g(a')) == (f(a') | g(a')) {
        sym a;
        use or_def;
        use triv;
        let r = triv(or_def) : prop_or'(f(a'), g(a')) == (f(a') | g(a'));
        return r;
    }
    let y2 = sym_eq(x2) : sym(a, prop_or'(f(a'), g(a'))) == sym(a, f(a') | g(a'));
    let r = cong_in_arg(z2, y2) : cong'(sym(a, f(a') | g(a')));
    return r;
}

fn cong_bin_imply : cong'(f) & cong'(g) -> cong'(sym(a, f(a') => g(a'))) {
    use imply_cong;
    use cong_bin;
    use cong_in_arg;
    use prop_imply;
    use sym_eq;
    use triv;

    x : cong'(f);
    y : cong'(g);

    let z = triv(imply_cong) : cong'(prop_imply');
    let z2 = cong_bin(x, y, z) : cong'(sym(a, prop_imply'(f(a'), g(a'))));
    fn x2 : sym a  ->  prop_imply'(f(a'), g(a')) == (f(a') => g(a')) {
        sym a;
        use imply_def;
        use triv;
        let r = triv(imply_def) : prop_imply'(f(a'), g(a')) == (f(a') => g(a'));
        return r;
    }
    let y2 = sym_eq(x2) : sym(a, prop_imply'(f(a'), g(a'))) == sym(a, f(a') => g(a'));
    let r = cong_in_arg(z2, y2) : cong'(sym(a, f(a') => g(a')));
    return r;
}

fn cong_bin_eq : cong'(f) & cong'(g) -> cong'(sym(a, f(a') == g(a'))) {
    use eq_cong;
    use cong_bin;
    use cong_in_arg;
    use prop_eq;
    use sym_eq;
    use triv;

    x : cong'(f);
    y : cong'(g);

    let z = triv(eq_cong) : cong'(prop_eq');
    let z2 = cong_bin(x, y, z) : cong'(sym(a, prop_eq'(f(a'), g(a'))));
    fn x2 : sym a  ->  prop_eq'(f(a'), g(a')) == (f(a') == g(a')) {
        sym a;
        use eq_def;
        use triv;
        let r = triv(eq_def) : prop_eq'(f(a'), g(a')) == (f(a') == g(a'));
        return r;
    }
    let y2 = sym_eq(x2) : sym(a, prop_eq'(f(a'), g(a'))) == sym(a, f(a') == g(a'));
    let r = cong_in_arg(z2, y2) : cong'(sym(a, f(a') == g(a')));
    return r;
}

fn cong_bin_eq_fst : cong'(f) -> cong'(sym(a, f(a') == a')) {
    use cong_bin_fst;
    use cong_in_arg;
    use eq_cong;
    use prop_eq;
    use sym_eq;
    use triv;

    x : cong'(f);

    let z = triv(eq_cong) : cong'(prop_eq');
    let z2 = cong_bin_fst(x, z) : cong'(sym(a, prop_eq'(f(a'), a')));
    fn x2 : sym a  ->  prop_eq'(f(a'), a') == (f(a') == a') {
        sym a;
        use eq_def;
        use triv;
        let r = triv(eq_def) : prop_eq'(f(a'), a') == (f(a') == a');
        return r;
    }
    let y2 = sym_eq(x2) : sym(a, prop_eq'(f(a'), a')) == sym(a, f(a') == a');
    let r = cong_in_arg(z2, y2) : cong'(sym(a, f(a') == a'));
    return r;
}