import "set.mm";
replace { equals : = , provable : |- };

2plus2 = ( 2 + 2 ) equals 4: provable;

proof of 2plus2 {
    c2;
    c2;
    caddc;
    co;
    c2;
    c1;
    c1;
    caddc;
    co;
    caddc;
    co;
    c4;
    c2;
    c1;
    c1;
    caddc;
    co;
    c2;
    caddc;
    df-2;
    oveq2i;
    c4;
    c3;
    c1;
    caddc;
    co;
    c2;
    c1;
    caddc;
    co;
    c1;
    caddc;
    co;
    c2;
    c1;
    c1;
    caddc;
    co;
    caddc;
    co;
    df-4;
    c3;
    c2;
    c1;
    caddc;
    co;
    c1;
    caddc;
    df-3;
    oveq1i;
    c2;
    c1;
    c1;
    2cn;
    ax-1cn;
    ax-1cn;
    addassi;
    3eqtri;
    eqtr4i;
}