At: extension lemma 1 1 1 1 1 3 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
8. z: 
case z: 3 (a'(x)); 3 3; 3 (a'(x)); 
By:
ThreeInd -1
THEN
AbReduce 0
Generated subgoals:None
About:
