Nuprl - Pf formula_imp_falsifiable

1. a: Assignment
2. q: Formula
3. r: Formula
4. (q under a) = 3
5. (r under a) = 3
6. 3 = 3

3 = 3

By: ApFunToHypEquands `zz' case zz: 3 0; 3 1; 3 2; -1

Generated subgoals:

1 7. zz:
case zz: 3 0; 3 1; 3 2; = case zz: 3 0; 3 1; 3 2;

2 7. case 3: 3 0; 3 1; 3 2; = case 3: 3 0; 3 1; 3 2;
3 = 3

About:

1	7. `zz:` `case zz: 3 0; 3 1; 3 2; = case zz: 3 0; 3 1; 3 2;`
2	7. `case 3: 3 0; 3 1; 3 2; = case 3: 3 0; 3 1; 3 2;` `3 = 3`