PrintForm Definitions assignment Sections ClassicalProps(jlc) Doc

At: restriction wf 1 1 1
1. a': Assignment
2. a: Assignment
3. x: Var
4. n:
5. a(x) = n
6. n1:
7. a'(x) = n1
8. n2:
9. a'(x) = n2

case n: 3 n1; 3 3; 3 n1;
By:
ThreeCases 4
THEN
Reduce 0
Generated subgoals:

None

About:
memberequalapply