PrintForm Definitions assignment Sections ClassicalProps(jlc) Doc

At: extension lemma 1 1 1 1 1 3

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

3 = a'(x)

By: Unfold `restriction` -1

Generated subgoal:

17. (x.case (a(x)): 3 (a'(x)); 3 3; 3 (a'(x));)(x) = 3
3 = a'(x)


About:
equalapply