PrintForm Definitions assignment Sections ClassicalProps(jlc) Doc

At: extension lemma 1 1 1 1 1
1. a: Assignment
2. a': Assignment
3. a'a = a
4. x: Var
5. a'a(x) = 3
6. n:
7. a(x) = n
8. a'a(x) = n

n = a'(x)
By: ThreeInd 6
Generated subgoals:

16. a(x) = 3
7. a'a(x) = 3
3 = a'(x)
26. a(x) = 3
7. a'a(x) = 3
3 = a'(x)
36. a(x) = 3
7. a'a(x) = 3
3 = a'(x)

About:
equalapply