Nuprl - Pf extension_lemma 1 1 1 1 1 1 1 1

1. a: Assignment
2. a': Assignment
3. a'a = a
4. x: Var
5. a'a(x) = 3
6. a(x) = 3
7. case (a(x)): 3 (a'(x)); 3 3; 3 (a'(x)); = 3

3 = a'(x)

By: HypSubst -2 -1

Generated subgoals:

1 8. z:
case z: 3 (a'(x)); 3 3; 3 (a'(x));

2 7. case 3: 3 (a'(x)); 3 3; 3 (a'(x)); = 3
3 = a'(x)

About:

1	8. `z:` `case z: 3 (a'(x)); 3 3; 3 (a'(x));`
2	7. `case 3: 3 (a'(x)); 3 3; 3 (a'(x)); = 3` `3 = a'(x)`