(R(_1;_2))(a,b) is | NOTE: | (R(_1;_2))(a,b) is | alpha-equivalent | to Symmetrize(x,y.R(x;y);a;b). |
| Who Cites symmetrize? | |
| symmetrize | Def Symmetrize(x,y.R(x;y);a;b) == R(a;b) & R(b;a) |
Thm*  T:Type{j}, R:(T TProp{i}), a,b:T. Symmetrize(x,y.R(x,y);a;b)  Prop{i} |
| Syntax: | Symmetrize(x,y.R(x;y);a;b) | has structure: | symmetrize(x,y.R(x;y); a; b) |
About:
 |  |  |  |  |  |  |