use cong;

fn comp_ty : (f : a -> b) & (g : b -> c) -> ((f . g) : a -> c) {
    axiom comp_ty : (f : a -> b) & (g : b -> c) -> ((f . g) : a -> c);
    x : (f : a -> b) & (g : b -> c);
    let r = comp_ty(x) : ((f . g) : a -> c);
    return r;
}

fn comp_def : true -> (f . g)(a) == f(g(a)) {
    axiom comp_def : true -> (f . g)(a) == f(g(a));
    x : true;
    let r = comp_def(x) : (f . g)(a) == f(g(a));
    return r;
}

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

fn comp_tup_sym_def : true -> (h . (f, g)) == sym(a, h(f(a'), g(a'))) {
    axiom comp_tup_sym_def : true -> (h . (f, g)) == sym(a, h(f(a'), g(a')));
    x : true;
    let r = comp_tup_sym_def(x) : (h . (f, g)) == sym(a, h(f(a'), g(a')));
    return r;
}

fn comp_tup_def :
    cong'(f) & cong'(g) & cong'(h) -> (h . (f, g))(a) == h(f(a), g(a))
{
    use comp_cong;
    use cong_fun_eq;
    use cong_in_arg;
    use comp_tup_sym_def;
    use triv;
    use tup_cong;

    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 x5 = cong_in_arg(x3, x4) : cong'(sym(a, h(f(a'), g(a'))));
    let x6 = cong_fun_eq(x3, x5, x4) : (h . (f, g))(a) == sym(a, h(f(a'), g(a')))(a);
    let r = x6() : (h . (f, g))(a) == h(f(a), g(a));
    return r;
}

fn comp_tup_sym_eq : true -> sym(a, (h . (f, g))(a')) == (h . (f, g)) {
    use sym_fun_eq;
    x : true;
    let r = sym_fun_eq(x) : sym(a, (h . (f, g))(a')) == (h . (f, g));
    return r;
}