Nuprl - Pf formula_imp_sat_lemma 1 1 1 1 1 8

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

a | q a |= r

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

Generated subgoals:

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

2 7. case 3: 3 0; 3 1; 3 2; = case 3: 3 0; 3 1; 3 2;
a | q a |= r

About:

1	7. `z:` `case z: 3 0; 3 1; 3 2; = case z: 3 0; 3 1; 3 2;`
2	7. `case 3: 3 0; 3 1; 3 2; = case 3: 3 0; 3 1; 3 2;` `a \| q a \|= r`