R(b;a)
T:Type, R:(T
TProp), a,b:T. strict_part(x,y.R(x,y);a;b) 
PropA == A 
FalseA:Prop. (A) Prop| Who Cites strict part? | |
| strict_part | Def strict_part(x,y.R(x;y);a;b) == R(a;b) & R(b;a) |
| Thm* T:Type, R:(TTProp), a,b:T. strict_part(x,y.R(x,y);a;b) Prop | |
| not | Def A == A False |
| Thm* A:Prop. (A) Prop |
| Syntax: | strict_part(x,y.R(x;y);a;b) | has structure: | strict_part(x,y.R(x;y); a; b) |
About:
 |  |  |  |  |  |  |  |  |